[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Closeds α
h : s.carrier = t.carrier
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Closeds α
carrier✝ : Set α
closed'✝ : IsClosed carrier✝
h : { carrier := carrier✝, closed' := closed'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, closed' := closed'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
closed'✝¹ : IsClosed carrier✝¹
carrier✝ : Set α
closed'✝ : IsClosed carrier✝
h : { carrier := carrier✝¹, closed' := closed'✝¹ }.carrier = { carrier := carrier✝, closed' := closed'✝ }.carrier
⊢ { carrier := carrier✝¹, closed' := closed'✝¹ } = { carrier := carrier✝, closed' := closed'✝ }
[PROOFSTEP]
congr
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_4
x : α
s : ι → Closeds α
⊢ x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i
[PROOFSTEP]
simp [iInf]
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)
[PROOFSTEP]
ext
[GOAL]
case h
ι✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ (i : ι), s i) ↔ x✝ ∈ ⋂ (i : ι), ↑(s i)
[PROOFSTEP]
simp
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_4
s : ι → Closeds α
⊢ ⨅ (i : ι), s i = { carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }
[PROOFSTEP]
ext1
[GOAL]
case h
ι✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ (i : ι), s i) = ↑{ carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
src✝ : CompleteLattice (Closeds α) := inferInstanceAs (CompleteLattice (Closeds α))
a : Closeds α
s : Set (Closeds α)
⊢ ↑(⨅ (b : Closeds α) (_ : b ∈ s), a ⊔ b) = ↑(a ⊔ sInf s)
[PROOFSTEP]
simp only [coe_sup, coe_iInf, coe_sInf, Set.union_iInter₂]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Closeds α
⊢ (Opens.compl ∘ ↑ofDual) ((↑toDual ∘ compl) s) = s
[PROOFSTEP]
simp [Closeds.compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : (Opens α)ᵒᵈ
⊢ (↑toDual ∘ compl) ((Opens.compl ∘ ↑ofDual) s) = s
[PROOFSTEP]
simp [Opens.compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Opens α
⊢ (Closeds.compl ∘ ↑ofDual) ((↑toDual ∘ compl) s) = s
[PROOFSTEP]
simp [Opens.compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : (Closeds α)ᵒᵈ
⊢ (↑toDual ∘ compl) ((Closeds.compl ∘ ↑ofDual) s) = s
[PROOFSTEP]
simp [Closeds.compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom s ↔ ∃ x, s = singleton x
[PROOFSTEP]
have : IsAtom (s : Set α) ↔ IsAtom s :=
  by
  refine' Closeds.gi.isAtom_iff' rfl (fun t ht => _) s
  obtain ⟨x, rfl⟩ := t.isAtom_iff.mp ht
  exact closure_singleton
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom ↑s ↔ IsAtom s
[PROOFSTEP]
refine' Closeds.gi.isAtom_iff' rfl (fun t ht => _) s
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ ↑(Closeds.closure t) = t
[PROOFSTEP]
obtain ⟨x, rfl⟩ := t.isAtom_iff.mp ht
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}
[PROOFSTEP]
exact closure_singleton
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
this : IsAtom ↑s ↔ IsAtom s
⊢ IsAtom s ↔ ∃ x, s = singleton x
[PROOFSTEP]
simp only [← this, (s : Set α).isAtom_iff, SetLike.ext'_iff, Closeds.singleton_coe]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ x, s = Closeds.compl (Closeds.singleton x)
[PROOFSTEP]
rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (↑toDual (Closeds.compl (compl s))) ↔ ∃ x, Closeds.compl (compl s) = Closeds.compl (Closeds.singleton x)
[PROOFSTEP]
change IsAtom (Closeds.complOrderIso α s.compl) ↔ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (↑(Closeds.complOrderIso α) (compl s)) ↔ ∃ x, Closeds.compl (compl s) = Closeds.compl (Closeds.singleton x)
[PROOFSTEP]
simp only [(Closeds.complOrderIso α).isAtom_iff, Closeds.isAtom_iff, Closeds.compl_bijective.injective.eq_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Clopens α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Clopens α
carrier✝ : Set α
clopen'✝ : IsClopen carrier✝
h : (fun s => s.carrier) { carrier := carrier✝, clopen' := clopen'✝ } = (fun s => s.carrier) t
⊢ { carrier := carrier✝, clopen' := clopen'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
clopen'✝¹ : IsClopen carrier✝¹
carrier✝ : Set α
clopen'✝ : IsClopen carrier✝
h :
  (fun s => s.carrier) { carrier := carrier✝¹, clopen' := clopen'✝¹ } =
    (fun s => s.carrier) { carrier := carrier✝, clopen' := clopen'✝ }
⊢ { carrier := carrier✝¹, clopen' := clopen'✝¹ } = { carrier := carrier✝, clopen' := clopen'✝ }
[PROOFSTEP]
congr


[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : NonAssocRing α
inst✝ : ContinuousMul α
⊢ Continuous fun a => -a
[PROOFSTEP]
simpa using (continuous_const.mul continuous_id : Continuous fun x : α => -1 * x)
[GOAL]
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_
[GOAL]
case refine_1
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x => ↑(↑AddMonoidHom.mul x.fst) x.snd) (0, 0)
[PROOFSTEP]
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]
[GOAL]
case refine_2
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (↑(↑AddMonoidHom.mul x)) 0
[PROOFSTEP]
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]
[GOAL]
case refine_3
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R), ContinuousAt (fun x => ↑(↑AddMonoidHom.mul x) y) 0
[PROOFSTEP]
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]
[GOAL]
α : Type u_1
inst✝ : Ring α
⊢ Injective toTopologicalSpace
[PROOFSTEP]
intro f g _
[GOAL]
α : Type u_1
inst✝ : Ring α
f g : RingTopology α
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
inst✝ : Ring α
g : RingTopology α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalRing✝ : TopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
toTopologicalSpace✝¹ : TopologicalSpace α
toTopologicalRing✝¹ : TopologicalRing α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalRing✝ : TopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalRing := toTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalRing := toTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }
[PROOFSTEP]
congr


[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
⊢ IsOpenMap ↑(mk N)
[PROOFSTEP]
intro s s_op
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) '' s)
[PROOFSTEP]
change IsOpen (mk N ⁻¹' (mk N '' s))
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) ⁻¹' (↑(mk N) '' s))
[PROOFSTEP]
rw [quotient_ring_saturate]
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun y => ↑x + y) '' s)
[PROOFSTEP]
exact isOpen_iUnion fun ⟨n, _⟩ => isOpenMap_add_left n s s_op
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
⊢ Function.Surjective fun p => (↑(mk N) p.fst, ↑(mk N) p.snd)
[PROOFSTEP]
rintro ⟨⟨x⟩, ⟨y⟩⟩
[GOAL]
case mk.mk.mk
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
fst✝ snd✝ : R ⧸ N
x y : R
⊢ ∃ a, (fun p => (↑(mk N) p.fst, ↑(mk N) p.snd)) a = (Quot.mk Setoid.r x, Quot.mk Setoid.r y)
[PROOFSTEP]
exact ⟨(x, y), rfl⟩