α : Type u_2
β : Type ?u.34252
γ : Type ?u.34255
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : ¬a ∈ s
h : ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
⊢ ↑(Finset.sup (Finset.cons a s x✝) f) = Finset.sup (Finset.cons a s x✝) fun i => ↑(f i)
α : Type u_2
β : Type ?u.34252
γ : Type ?u.34255
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
s : Finset ι
f : ι → Compacts α
⊢ ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
refine Finset.cons_induction_on s rfl fun a s _ h => ?_
α : Type u_2
β : Type ?u.34252
γ : Type ?u.34255
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : ¬a ∈ s
h : ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
⊢ ↑(f a) ∪ ↑(Finset.sup s f) = ↑(f a) ∪ Finset.sup s fun i => ↑(f i)
α : Type u_2
β : Type ?u.34252
γ : Type ?u.34255
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : ¬a ∈ s
h : ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
⊢ ↑(Finset.sup (Finset.cons a s x✝) f) = Finset.sup (Finset.cons a s x✝) fun i => ↑(f i)
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]
no goals
α : Type u_2
β : Type ?u.34252
γ : Type ?u.34255
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : ¬a ∈ s
h : ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
⊢ ↑(f a) ∪ ↑(Finset.sup s f) = ↑(f a) ∪ Finset.sup s fun i => ↑(f i)
congr