[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : C(α, β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : (mk toFun✝).toFun = g.toFun
⊢ mk toFun✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : (mk toFun✝¹).toFun = (mk toFun✝).toFun
⊢ mk toFun✝¹ = mk toFun✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f✝ g✝ f g : C(α, β)
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g✝ g : C(α, β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : ↑(mk toFun✝) = ↑g
⊢ mk toFun✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : ↑(mk toFun✝¹) = ↑(mk toFun✝)
⊢ mk toFun✝¹ = mk toFun✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
⊢ (fun f => mk f) ((fun f => ↑f) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
a✝ : α
⊢ ↑((fun f => mk f) ((fun f => ↑f) x✝)) a✝ = ↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : α → β
⊢ (fun f => ↑f) ((fun f => mk f) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝¹ : α → β
x✝ : α
⊢ (fun f => ↑f) ((fun f => mk f) x✝¹) x✝ = x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f✝ g : C(α, β)
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective ↑f
h : comp f g₁ = comp f g₂
a : α
⊢ ↑f (↑g₁ a) = ↑f (↑g₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
H : ⋃ (i : ι), S i = Set.univ
i : ι
⊢ ContinuousOn (Set.liftCover S (fun i => ↑(φ i)) hφ H) (S i)
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
H : ⋃ (i : ι), S i = Set.univ
i : ι
⊢ Continuous (Set.restrict (S i) (Set.liftCover S (fun i => ↑(φ i)) hφ H))
[PROOFSTEP]
simpa only [Set.restrict, Set.liftCover_coe] using (φ i).continuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
i : ι
x : ↑(S i)
⊢ ↑(liftCover S φ hφ hS) ↑x = ↑(φ i) x
[PROOFSTEP]
rw [liftCover, coe_mk, Set.liftCover_coe _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
i : ι
⊢ restrict (S i) (liftCover S φ hφ hS) = φ i
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
i : ι
a✝ : ↑(S i)
⊢ ↑(restrict (S i) (liftCover S φ hφ hS)) a✝ = ↑(φ i) a✝
[PROOFSTEP]
simp only [coe_restrict, Function.comp_apply, liftCover_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
⊢ C(α, β)
[PROOFSTEP]
let S : A → Set α := (↑)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S✝ : ι → Set α
φ : (i : ι) → C(↑(S✝ i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S✝ i) (hxj : x ∈ S✝ j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S✝ i ∈ nhds x
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
S : ↑A → Set α := Subtype.val
⊢ C(α, β)
[PROOFSTEP]
let F : ∀ i : A, C(i, β) := fun i => F i i.prop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S✝ : ι → Set α
φ : (i : ι) → C(↑(S✝ i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S✝ i) (hxj : x ∈ S✝ j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S✝ i ∈ nhds x
A : Set (Set α)
F✝ : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F✝ s hs) { val := x, property := hxi } = ↑(F✝ t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
S : ↑A → Set α := Subtype.val
F : (i : ↑A) → C(↑↑i, β) := fun i => F✝ ↑i (_ : ↑i ∈ A)
⊢ C(α, β)
[PROOFSTEP]
refine' liftCover S F (fun i j => hF i i.prop j j.prop) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S✝ : ι → Set α
φ : (i : ι) → C(↑(S✝ i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S✝ i) (hxj : x ∈ S✝ j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S✝ i ∈ nhds x
A : Set (Set α)
F✝ : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F✝ s hs) { val := x, property := hxi } = ↑(F✝ t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
S : ↑A → Set α := Subtype.val
F : (i : ↑A) → C(↑↑i, β) := fun i => F✝ ↑i (_ : ↑i ∈ A)
⊢ ∀ (x : α), ∃ i, S i ∈ nhds x
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S✝ : ι → Set α
φ : (i : ι) → C(↑(S✝ i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S✝ i) (hxj : x ∈ S✝ j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S✝ i ∈ nhds x
A : Set (Set α)
F✝ : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F✝ s hs) { val := x, property := hxi } = ↑(F✝ t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
S : ↑A → Set α := Subtype.val
F : (i : ↑A) → C(↑↑i, β) := fun i => F✝ ↑i (_ : ↑i ∈ A)
x : α
⊢ ∃ i, S i ∈ nhds x
[PROOFSTEP]
obtain ⟨s, hs, hsx⟩ := hA x
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S✝ : ι → Set α
φ : (i : ι) → C(↑(S✝ i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S✝ i) (hxj : x ∈ S✝ j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S✝ i ∈ nhds x
A : Set (Set α)
F✝ : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F✝ s hs) { val := x, property := hxi } = ↑(F✝ t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
S : ↑A → Set α := Subtype.val
F : (i : ↑A) → C(↑↑i, β) := fun i => F✝ ↑i (_ : ↑i ∈ A)
x : α
s : Set α
hs : s ∈ A
hsx : s ∈ nhds x
⊢ ∃ i, S i ∈ nhds x
[PROOFSTEP]
exact ⟨⟨s, hs⟩, hsx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑{ val := s, property := hs } := x
⊢ ↑(liftCover' A F hF hA) ↑x = ↑(F s hs) x
[PROOFSTEP]
delta liftCover'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑{ val := s, property := hs } := x
⊢ ↑(let S := Subtype.val;
        let F_1 := fun i => F ↑i (_ : ↑i ∈ A);
        liftCover S F_1
          (_ :
            ∀ (i j : ↑A) (x : α) (hxi : x ∈ ↑i) (hxj : x ∈ ↑j),
              ↑(F ↑i (_ : ↑i ∈ A)) { val := x, property := hxi } = ↑(F ↑j (_ : ↑j ∈ A)) { val := x, property := hxj })
          (_ : ∀ (x : α), ∃ i, ↑i ∈ nhds x))
      ↑x =
    ↑(F s hs) x
[PROOFSTEP]
exact liftCover_coe x'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
g : β ≃ₜ γ
⊢ ContinuousMap.comp (toContinuousMap (Homeomorph.symm f)) (toContinuousMap f) = ContinuousMap.id α
[PROOFSTEP]
rw [← coe_trans, self_trans_symm, coe_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
g : β ≃ₜ γ
⊢ ContinuousMap.comp (toContinuousMap f) (toContinuousMap (Homeomorph.symm f)) = ContinuousMap.id β
[PROOFSTEP]
rw [← coe_trans, symm_trans_self, coe_refl]
