case hb
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i => (b i).carrier)

case hb'
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), ↑(b i)
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
case h.e'_3
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i => (b i).carrier) = SetLike.coe '' range b
case hb
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i => (b i).carrier)
convert (config := {transparency := .default}) hb
case h.e'_3.h
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i => (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b
case h.e'_3
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i => (b i).carrier) = SetLike.coe '' range b
ext
no goals
case h.e'_3.h
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i => (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b
simp
no goals
case hb'
ι✝ : Type ?u.35576
α : Type u_2
β : Type ?u.35582
γ : Type ?u.35585
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier
exact hb'