awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(ofOpenSubsets U).glued : Type u)
h :
  ∀ (i : (ofOpenSubsets U).J) (x : (↑(of α) : Type u)) (hx' : x ∈ U i),
    Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                  (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
                (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
              (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
            (↑(ofOpenSubsets U).glued : Type u)) :
        (↑(of α) : Type u))
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))

Tactic:
obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x

Premises used: TopCat.GlueData.ofOpenSubsets, TopCat.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
h :
  Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
      α)
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))

Tactic:
rw [ι_fromOpenSubsetsGlue_apply]

Premises used: TopCat.GlueData.ι_fromOpenSubsetsGlue_apply
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
      α)

Tactic:
Set.subset_iUnion _ i hx'

Premises used: Set.Mem, Set.subset_iUnion
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
      α)

Tactic:
exact Set.subset_iUnion _ i hx'

Premises used: Set.subset_iUnion
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(of α) : Type u)
i : J
hx : Membership.mem (γ := Set α) ((fun (i : J) ↦ (↑(U i) : Set α)) i) x
⊢ Membership.mem (γ := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U)) :
        (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
    x

Tactic:
⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

Premises used: TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, TopCat.GlueData.toGlueData, TopCat.GlueData.ofOpenSubsets, Subtype.mk, CategoryTheory.GlueData.ι, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(of α) : Type u)
i : J
hx : Membership.mem (γ := Set α) ((fun (i : J) ↦ (↑(U i) : Set α)) i) x
⊢ Membership.mem (γ := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U)) :
        (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
    x

Tactic:
exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩
-- Module: Mathlib.Topology.Hom.ContinuousEval
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : FunLike F X Y
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : ContinuousEval F X Y
inst_5 : TopologicalSpace Z
f : Z → F
g : Z → X
hf : Continuous[inst_5, inst_1] f
hg : Continuous[inst_5, inst_2] g
⊢ Continuous[inst_5, inst_3] fun (z : Z) ↦ (f z : (a : X) → Y) (g z)

Tactic:
continuous_eval.comp (hf.prodMk hg)

Premises used: Continuous.comp, ContinuousEval.continuous_eval, Continuous.prodMk
-- Module: Mathlib.Topology.Hom.ContinuousEval
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
inst : FunLike F X Y
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : ContinuousEval F X Y
F' : Type u_5
inst_5 : FunLike F' X Y
inst_6 : TopologicalSpace F'
f : F' → F
hc : Continuous[inst_6, inst_1] f
hf : ∀ (g : F'), Eq (α := (a : X) → Y) (⇑(f g) : (a : X) → Y) (⇑g : (a : X) → Y)
⊢ Continuous[instTopologicalSpaceProd, inst_3] fun (fx : F' × X) ↦ (fx.1 : (a : X) → Y) fx.2

Tactic:
simpa only [← hf] using hc.fst'.eval continuous_snd

Premises used: Continuous.fst', continuous_snd, Continuous.eval
-- Module: Mathlib.Topology.Hom.ContinuousEval
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
inst : FunLike F X Y
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : ContinuousEval F X Y
α : Type u_5
l : Filter α
f : α → F
f₀ : F
g : α → X
x₀ : X
hf : Tendsto f l (𝓝 f₀)
hg : Tendsto g l (𝓝 x₀)
⊢ Tendsto.{u_5, u_3} (β := Y) (fun (a : α) ↦ ((f a : (a : X) → Y) (g a) : Y)) l (𝓝 ((f₀ : (a : X) → Y) x₀) : Filter Y)

Tactic:
(ContinuousEval.continuous_eval.tendsto _).comp (hf.prodMk_nhds hg)

Premises used: Continuous.tendsto, ContinuousEval.continuous_eval, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Hom.ContinuousEval
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : FunLike F X Y
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : ContinuousEval F X Y
inst_5 : TopologicalSpace Z
f : Z → F
g : Z → X
z : Z
hf : ContinuousAt f z
hg : ContinuousAt g z
⊢ ContinuousAt.{u_4, u_3} (Y := Y) (fun (z : Z) ↦ (f z : (a : X) → Y) (g z)) z

Tactic:
hf.eval hg

Premises used: ContinuousAt, Filter.Tendsto.eval
-- Module: Mathlib.Topology.Hom.ContinuousEval
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : FunLike F X Y
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : ContinuousEval F X Y
inst_5 : TopologicalSpace Z
f : Z → F
g : Z → X
s : Set Z
z : Z
hf : ContinuousWithinAt f s z
hg : ContinuousWithinAt g s z
⊢ ContinuousWithinAt.{u_4, u_3} (Y := Y) (fun (z : Z) ↦ (f z : (a : X) → Y) (g z)) s z

Tactic:
hf.eval hg

Premises used: ContinuousWithinAt, Filter.Tendsto.eval
-- Module: Mathlib.Topology.Hom.ContinuousEval
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : FunLike F X Y
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : ContinuousEval F X Y
inst_5 : TopologicalSpace Z
f : Z → F
g : Z → X
s : Set Z
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_4, u_3} (Y := Y) (fun (z : Z) ↦ (f z : (a : X) → Y) (g z)) s

Tactic:
fun z hz ↦ (hf z hz).eval (hg z hz)

Premises used: ContinuousWithinAt.eval, ContinuousOn
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
F' : Type u_5
inst_4 : FunLike F' α X
inst_5 : TopologicalSpace F'
f : F' → F
hc : Continuous[inst_5, inst_1] f
hf : ∀ (g : F'), Eq (α := (a : α) → X) (⇑(f g) : (a : α) → X) (⇑g : (a : α) → X)
x : α
⊢ Continuous[inst_5, inst_2] fun (f : F') ↦ (f : (a : α) → X) x

Tactic:
simpa only [← hf] using (continuous_eval_const x).comp hc

Premises used: Continuous.comp, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
hf : Continuous[inst_4, inst_1] f
x : α
⊢ Continuous[inst_4, inst_2] fun (x_1 : Z) ↦ (f x_1 : (a : α) → X) x

Tactic:
(continuous_eval_const x).comp hf

Premises used: Continuous.comp, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
⊢ Continuous[inst_1, Pi.topologicalSpace] (DFunLike.coe (β := fun (a : α) ↦ X))

Tactic:
continuous_pi continuous_eval_const

Premises used: continuous_pi, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
hf : Continuous[inst_4, inst_1] f
⊢ Continuous[inst_4, Pi.topologicalSpace] fun (z : Z) ↦ (⇑(f z) : (a : α) → X)

Tactic:
continuous_pi hf.eval_const

Premises used: continuous_pi, Continuous.eval_const
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
ι : Type u_5
l : Filter ι
f : ι → F
g : F
hf : Tendsto f l (𝓝 g)
a : α
⊢ Tendsto.{u_5, u_3} (β := X) (fun (x : ι) ↦ ((f x : (a : α) → X) a : X)) l (𝓝 ((g : (a : α) → X) a) : Filter X)

Tactic:
((continuous_id.eval_const a).tendsto _).comp hf

Premises used: Continuous.eval_const, Continuous.tendsto, continuous_id, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
ι : Type u_5
l : Filter ι
f : ι → F
g : F
hf : Tendsto f l (𝓝 g)
⊢ Tendsto (β := (a : α) → X) (fun (i : ι) ↦ (⇑(f i) : (a : α) → X)) l (𝓝 (⇑g : (a : α) → X))

Tactic:
(continuous_id.coeFun.tendsto _).comp hf

Premises used: Continuous.coeFun, Continuous.tendsto, continuous_id, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
z : Z
hf : ContinuousAt f z
x : α
⊢ ContinuousAt.{u_4, u_3} (Y := X) (fun (x_1 : Z) ↦ (f x_1 : (a : α) → X) x) z

Tactic:
hf.eval_const x

Premises used: ContinuousAt, Filter.Tendsto.eval_const
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
z : Z
hf : ContinuousAt f z
⊢ ContinuousAt (Y := (a : α) → X) (fun (z : Z) ↦ (⇑(f z) : (a : α) → X)) z

Tactic:
hf.coeFun

Premises used: ContinuousAt, Filter.Tendsto.coeFun
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
s : Set Z
z : Z
hf : ContinuousWithinAt f s z
x : α
⊢ ContinuousWithinAt.{u_4, u_3} (Y := X) (fun (x_1 : Z) ↦ (f x_1 : (a : α) → X) x) s z

Tactic:
hf.eval_const x

Premises used: ContinuousWithinAt, Filter.Tendsto.eval_const
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
s : Set Z
z : Z
hf : ContinuousWithinAt f s z
⊢ ContinuousWithinAt (Y := (a : α) → X) (fun (z : Z) ↦ (⇑(f z) : (a : α) → X)) s z

Tactic:
hf.coeFun

Premises used: ContinuousWithinAt, Filter.Tendsto.coeFun
-- Module: Mathlib.Topology.Hom.ContinuousEvalConst
Goal:
F : Type u_1
α : Type u_2
X : Type u_3
Z : Type u_4
inst : FunLike F α X
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace X
inst_3 : ContinuousEvalConst F α X
inst_4 : TopologicalSpace Z
f : Z → F
s : Set Z
hf : ContinuousOn f s
x : α
⊢ ContinuousOn.{u_4, u_3} (Y := X) (fun (x_1 : Z) ↦ (f x_1 : (a : α) → X) x) s

Tactic:
fun z hz ↦ (hf z hz).eval_const x

Premises used: ContinuousWithinAt.eval_const, ContinuousOn
-- Module: Mathlib.Topology.Hom.Open
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : α →CO β
h : Eq (α := (a : α) → β) ((fun (f : α →CO β) ↦ f.toFun) f) ((fun (f : α →CO β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (continuous_toFun : Continuous toFun)
    (map_open' : IsOpenMap { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
        ((fun (f : α →CO β) ↦ f.toFun) g)),
    { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.Hom.Open
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
g : α →CO β
toFun : α → β
continuous_toFun : Continuous toFun
map_open' : IsOpenMap { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
    ((fun (f : α →CO β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous toFun_1)
    (map_open'_1 : IsOpenMap { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
        ((fun (f : α →CO β) ↦ f.toFun)
          { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_open' := map_open'_1 })),
    { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_open' := map_open'_1 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.Hom.Open
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
toFun : α → β
continuous_toFun : Continuous toFun
map_open' : IsOpenMap { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun
toFun_1 : α → β
continuous_toFun_1 : Continuous toFun_1
map_open'_1 : IsOpenMap { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
    ((fun (f : α →CO β) ↦ f.toFun)
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_open' := map_open'_1 })
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_open' := map_open'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α →CO β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α →CO β
⊢ Eq (α := (a : α) → β) (⇑f.toContinuousMap : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α →CO β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α →CO β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α →CO β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Eq (α := (a : α) → α) (⇑(ContinuousOpenMap.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
inst : TopologicalSpace α
a : α
⊢ (ContinuousOpenMap.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β →CO γ
g : α →CO β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β →CO γ
g : α →CO β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : γ →CO δ
g : β →CO γ
h : α →CO β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: ContinuousOpenMap.comp, ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α →CO β
⊢ f.comp (ContinuousOpenMap.id α) = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousOpenMap.ext, rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α →CO β
⊢ comp (ContinuousOpenMap.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousOpenMap.ext, rfl
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g₁ g₂ : β →CO γ
f : α →CO β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun h => congr_arg₂ _ h rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, ContinuousOpenMap.comp, DFunLike.ext_iff, ContinuousOpenMap.ext, Iff.intro, Iff.mp, rfl, congr_arg₂
-- Module: Mathlib.Topology.Hom.Open
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: ContinuousOpenMap.comp_apply
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : X ≃ Y
b : Continuous[inst, inst_1] a.toFun
c : Continuous[inst_1, inst] a.invFun
⊢ Eq (α := (a : X) → Y) (⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c : X ≃ₜ Y } : (a : X) → Y)
    (⇑a : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.symm.symm = h

Tactic:
rfl

Premises used: Homeomorph.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Function.Bijective (α := X ≃ₜ Y) Homeomorph.symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, Homeomorph.symm_symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq (α := (a : X) → Y) (⇑h.toEquiv : (a : X) → Y) (⇑h : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq (α := (a : Y) → X) (⇑h.symm : (a : Y) → X) (⇑h.symm : (a : Y) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h h' : X ≃ₜ Y
H : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((h : (a : X) → Y) x : Y) ((h' : (a : X) → Y) x : Y)
⊢ h = h'

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h₁ : X ≃ₜ Y
h₂ : Y ≃ₜ Z
x : X
⊢ Eq.{u_4 + 1} (α := Z) ((h₁.trans h₂ : (a : X) → Z) x : Z) ((h₂ : (a : Y) → Z) ((h₁ : (a : X) → Y) x : Y) : Z)

Tactic:
rfl

Premises used: rfl