[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : Compacts α
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 β
inst✝ : TopologicalSpace γ
t : Compacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isCompact' := isCompact'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h :
  { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier =
    { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹ } = { carrier := carrier✝, isCompact' := isCompact'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
[PROOFSTEP]
refine Finset.cons_induction_on s rfl fun a s _ h => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
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)
[PROOFSTEP]
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
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)
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) (Compacts.map ↑f (_ : Continuous ↑f) s) = s
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ ↑(Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) (Compacts.map ↑f (_ : Continuous ↑f) s)) =
    ↑s
[PROOFSTEP]
simp only [coe_map, ← image_comp, f.symm_comp_self, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
⊢ Compacts.map ↑f (_ : Continuous ↑f) (Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) s) = s
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
⊢ ↑(Compacts.map ↑f (_ : Continuous ↑f) (Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) s)) =
    ↑s
[PROOFSTEP]
simp only [coe_map, ← image_comp, f.self_comp_symm, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : NonemptyCompacts α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : NonemptyCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : Set.Nonempty { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ } =
    (fun s => s.carrier) t
⊢ { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
nonempty'✝¹ : Set.Nonempty { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : Set.Nonempty { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, nonempty' := nonempty'✝¹ } =
    (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ }
⊢ { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, nonempty' := nonempty'✝¹ } =
    { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : PositiveCompacts α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : PositiveCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : Set.Nonempty (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier)
h :
  (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ } =
    (fun s => s.carrier) t
⊢ { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
interior_nonempty'✝¹ : Set.Nonempty (interior { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier)
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : Set.Nonempty (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier)
h :
  (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ },
        interior_nonempty' := interior_nonempty'✝¹ } =
    (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ }
⊢ { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, interior_nonempty' := interior_nonempty'✝¹ } =
    { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ Set.Nonempty (interior (Compacts.prod K.toCompacts L.toCompacts).carrier)
[PROOFSTEP]
simp only [Compacts.carrier_eq_coe, Compacts.coe_prod, interior_prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ Set.Nonempty (interior ↑K.toCompacts ×ˢ interior ↑L.toCompacts)
[PROOFSTEP]
exact K.interior_nonempty.prod L.interior_nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : CompactOpens α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : CompactOpens α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ } =
    (fun s => s.carrier) t
⊢ { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
isOpen'✝¹ : IsOpen { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier) { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, isOpen' := isOpen'✝¹ } =
    (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ }
⊢ { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, isOpen' := isOpen'✝¹ } =
    { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ }
[PROOFSTEP]
congr
