-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem isTopologicalBasis : IsTopologicalBasis (lowerBasis α)

Proof state:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩

Result:
no goals

Proof state:
case h.e'_3.h.mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}} → s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
rintro ⟨F, ⟨hF, hs⟩, rfl⟩

Result:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Proof state:
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
ext s

Result:
case h.e'_3.h
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} ↔ s ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Proof state:
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lowerBasis α = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]

Result:
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Proof state:
case h.e'_3.h.mp
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} → s ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
rintro ⟨F, hF, rfl⟩

Result:
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set α
hF : F.Finite
⊢ ⋂ i ∈ F, (Ici i)ᶜ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Proof state:
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set α
hF : F.Finite
⊢ ⋂ i ∈ F, (Ici i)ᶜ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
refine ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, ?_⟩

Result:
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set α
hF : F.Finite
⊢ (fun f => ⋂₀ f) ((fun a => (Ici a)ᶜ) '' F) = ⋂ i ∈ F, (Ici i)ᶜ

Proof state:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
haveI := hF.to_subtype

Result:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Proof state:
case h.e'_3.h
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} ↔ s ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
constructor

Result:
case h.e'_3.h.mp
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} → s ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

case h.e'_3.h.mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}} → s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Proof state:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : ∀ (x : { a // a ∈ F }), ↑x ∈ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
choose f hf using hs

Result:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ ⋂ i ∈ range f, (Ici i)ᶜ = (fun f => ⋂₀ f) F

Tactic:
simp_rw [biInter_range, hf, sInter_eq_iInter]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ IsTopologicalBasis (lowerBasis α)

Tactic:
convert isTopologicalBasis_of_subbasis (topology_eq α)

Result:
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lowerBasis α = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Proof state:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
rw [subset_def, Subtype.forall'] at hs

Result:
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : ∀ (x : { a // a ∈ F }), ↑x ∈ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Proof state:
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set α
hF : F.Finite
⊢ (fun f => ⋂₀ f) ((fun a => (Ici a)ᶜ) '' F) = ⋂ i ∈ F, (Ici i)ᶜ

Tactic:
simp only [sInter_image]

Result:
no goals