awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
rcases : ∀ (h : X ≃ₕ Unit), Nonempty (X ≃ₕ Y)
⊢ Nonempty (X ≃ₕ Y)

Tactic:
rcases ContractibleSpace.hequiv_unit' (X := X) with ⟨h⟩

Premises used: ContractibleSpace.hequiv_unit'
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
h : X ≃ₕ Unit
rcases : ∀ (h' : Y ≃ₕ Unit), Nonempty (X ≃ₕ Y)
⊢ Nonempty (X ≃ₕ Y)

Tactic:
rcases ContractibleSpace.hequiv_unit' (X := Y) with ⟨h'⟩

Premises used: ContractibleSpace.hequiv_unit'
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
h : X ≃ₕ Unit
h' : Y ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Tactic:
⟨h.trans h'.symm⟩

Premises used: ContinuousMap.HomotopyEquiv.trans, Nonempty.intro, ContinuousMap.HomotopyEquiv.symm
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
h : X ≃ₕ Unit
h' : Y ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Tactic:
exact ⟨h.trans h'.symm⟩
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
obtain : ∀ (p : X) (h : Homotopy (ContinuousMap.id X) (const X p)), PathConnectedSpace X
⊢ PathConnectedSpace X

Tactic:
obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X

Premises used: id_nullhomotopic
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
⊢ ∀ (x : X), Joined p x

Tactic:
have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
rw : ∃ (x : X), pathComponent x = Set.univ
⊢ PathConnectedSpace X

Tactic:
rw [pathConnectedSpace_iff_eq]

Premises used: pathConnectedSpace_iff_eq
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
h₁ : pathComponent p = Set.univ
⊢ ∃ (x : X), pathComponent x = Set.univ

Tactic:
use p
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
h₁ : ∀ (x : X), x ∈ pathComponent p ↔ Membership.mem (γ := Set X) Set.univ x
⊢ pathComponent p = Set.univ

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
x : X
h₁ : x ∈ pathComponent p → Membership.mem (γ := Set X) Set.univ x
h₂ : Membership.mem (γ := Set X) Set.univ x → x ∈ pathComponent p
h₃ h₄ h₅ : x ∈ pathComponent p → Membership.mem (γ := Set X) Set.univ x
h₆ h₇ h₈ : Membership.mem (γ := Set X) Set.univ x → x ∈ pathComponent p
h₉ h₁₀ h₁₁ : x ∈ pathComponent p → Membership.mem (γ := Set X) Set.univ x
h₁₂ h₁₃ h₁₄ : Membership.mem (γ := Set X) Set.univ x → x ∈ pathComponent p
h₁₅ h₁₆ : x ∈ pathComponent p → Membership.mem (γ := Set X) Set.univ x
h₁₇ h₁₈ : Membership.mem (γ := Set X) Set.univ x → x ∈ pathComponent p
⊢ x ∈ pathComponent p ↔ Membership.mem (γ := Set X) Set.univ x

Tactic:
tauto
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
obtain : ∀ (hX : X ≃ₕ Unit), ContractibleSpace (X × Y)
⊢ ContractibleSpace (X × Y)

Tactic:
obtain ⟨hX⟩ := hequiv_unit' (X := X)

Premises used: ContractibleSpace.hequiv_unit'
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
hX : X ≃ₕ Unit
obtain : ∀ (hY : Y ≃ₕ Unit), ContractibleSpace (X × Y)
⊢ ContractibleSpace (X × Y)

Tactic:
obtain ⟨hY⟩ := hequiv_unit' (X := Y)

Premises used: ContractibleSpace.hequiv_unit'
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
hX : X ≃ₕ Unit
hY : Y ≃ₕ Unit
⊢ ContractibleSpace (X × Y)

Tactic:
⟨⟨(hX.prodCongr hY).trans ?_⟩⟩

Premises used: ContractibleSpace.mk, ContinuousMap.HomotopyEquiv.trans, ContinuousMap.HomotopyEquiv.prodCongr, Nonempty.intro
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
hX : X ≃ₕ Unit
hY : Y ≃ₕ Unit
refine : Unit × Unit ≃ₕ Unit
⊢ ContractibleSpace (X × Y)

Tactic:
refine ⟨⟨(hX.prodCongr hY).trans ?_⟩⟩
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
hX : X ≃ₕ Unit
hY : Y ≃ₕ Unit
⊢ Unit × Unit ≃ₕ Unit

Tactic:
exact (Homeomorph.prodUnique Unit Unit).toHomotopyEquiv

Premises used: Homeomorph.prodUnique, Homeomorph.toHomotopyEquiv, Unit
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₕ Y
⊢ Continuous.{u, v} (X := X) (Y := Y) (⇑h.toFun : (a : X) → Y)

Tactic:
h.toFun.continuous

Premises used: ContinuousMap.continuous, ContinuousMap.HomotopyEquiv.toFun
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h : X ≃ₜ Y
rw rw₁ : Homotopic (ContinuousMap.id X) (ContinuousMap.id X)
⊢ Homotopic (comp (↑h.symm : C(Y, X)) (↑h : C(X, Y))) (ContinuousMap.id X)

Tactic:
rw [symm_comp_toContinuousMap]

Premises used: Homeomorph.symm_comp_toContinuousMap
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h : X ≃ₜ Y
rw rw₁ : Homotopic (ContinuousMap.id Y) (ContinuousMap.id Y)
⊢ Homotopic (comp (↑h : C(X, Y)) (↑h.symm : C(Y, X))) (ContinuousMap.id Y)

Tactic:
rw [toContinuousMap_comp_symm]

Premises used: Homeomorph.toContinuousMap_comp_symm
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq (α := (a : X) → Y) (⇑h.toHomotopyEquiv.toFun : (a : X) → Y) (⇑h : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₕ Y
⊢ Eq (α := (a : Y) → X) (⇑h.invFun : (a : Y) → X) (⇑h.symm.toFun : (a : Y) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (ContinuousMap.id X)

Tactic:
Homotopic.trans ?_ h₁.left_inv

Premises used: ContinuousMap.HomotopyEquiv.left_inv, ContinuousMap.Homotopic.trans
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
refine : ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (h₁.invFun.comp h₁.toFun)
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (ContinuousMap.id X)

Tactic:
refine Homotopic.trans ?_ h₁.left_inv

Premises used: ContinuousMap.HomotopyEquiv.left_inv, ContinuousMap.Homotopic.trans
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (h₁.invFun.comp h₁.toFun)

Tactic:
.comp (.refl _) (.comp h₂.left_inv (.refl _))

Premises used: ContinuousMap.Homotopic.comp, ContinuousMap.comp, ContinuousMap.HomotopyEquiv.left_inv, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (h₁.invFun.comp h₁.toFun)

Tactic:
exact .comp (.refl _) (.comp h₂.left_inv (.refl _))
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (ContinuousMap.id Z)

Tactic:
Homotopic.trans ?_ h₂.right_inv

Premises used: ContinuousMap.HomotopyEquiv.right_inv, ContinuousMap.Homotopic.trans
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
refine : ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (h₂.toFun.comp h₂.invFun)
⊢ ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (ContinuousMap.id Z)

Tactic:
refine Homotopic.trans ?_ h₂.right_inv

Premises used: ContinuousMap.HomotopyEquiv.right_inv, ContinuousMap.Homotopic.trans
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (h₂.toFun.comp h₂.invFun)

Tactic:
.comp (.refl _) <| .comp h₁.right_inv (.refl _)

Premises used: ContinuousMap.Homotopic.comp, ContinuousMap.HomotopyEquiv.right_inv, ContinuousMap.comp, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (h₂.toFun.comp h₂.invFun)

Tactic:
exact .comp (.refl _) <| .comp h₁.right_inv (.refl _)
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ (h₁.trans h₂).symm = h₂.symm.trans h₁.symm

Tactic:
rfl

Premises used: ContinuousMap.HomotopyEquiv.trans, ContinuousMap.comp, ContinuousMap.HomotopyEquiv.symm, rfl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq (α := X ≃ₕ X) (toHomotopyEquiv (Homeomorph.refl X)) (HomotopyEquiv.refl X)

Tactic:
rfl

Premises used: ContinuousMap.HomotopyEquiv.refl, rfl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm

Tactic:
rfl

Premises used: Homeomorph.toHomotopyEquiv, toContinuousMap, ContinuousMap.HomotopyEquiv.symm, rfl
-- Module: Mathlib.Topology.Homotopy.Equiv
Goal:
X : Type u
Y : Type v
Z : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h₀ : X ≃ₜ Y
h₁ : Y ≃ₜ Z
⊢ (h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv

Tactic:
rfl

Premises used: ContinuousMap.HomotopyEquiv.trans, ContinuousMap.comp, toContinuousMap, rfl
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
⊢ Continuous (Y := X × Y) fun (p : (X × Y) × X × Y) ↦
    ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
simp :
  Eq.{u + 1} (α := X) ((hmul : (a : X × X) → X) (@e _ inst _, @e _ inst _) : X) (@e _ inst _ : X) ∧
    Eq.{v + 1} (α := Y) ((hmul : (a : Y × Y) → Y) (@e _ inst_1 _, @e _ inst_1 _) : Y) (@e _ inst_1 _ : Y)
⊢ Eq (α := X × Y)
    (({
            toFun := fun (p : (X × Y) × X × Y) ↦
              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
            continuous_toFun := ⋯ } :
          (a : (X × Y) × X × Y) → X × Y)
        ((@e _ inst _, @e _ inst_1 _), @e _ inst _, @e _ inst_1 _) :
      X × Y)
    ((@e _ inst _, @e _ inst_1 _) : X × Y)

Tactic:
simp only [ContinuousMap.coe_mk, Prod.mk_inj]

Premises used: Prod.mk_inj, ContinuousMap.coe_mk
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
⊢ Eq.{u + 1} (α := X) ((hmul : (a : X × X) → X) (@e _ inst _, @e _ inst _) : X) (@e _ inst _ : X) ∧
    Eq.{v + 1} (α := Y) ((hmul : (a : Y × Y) → Y) (@e _ inst_1 _, @e _ inst_1 _) : Y) (@e _ inst_1 _ : Y)

Tactic:
⟨HSpace.hmul_e_e, HSpace.hmul_e_e⟩

Premises used: HSpace.hmul_e_e, And.intro
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
⊢ Eq.{u + 1} (α := X) ((hmul : (a : X × X) → X) (@e _ inst _, @e _ inst _) : X) (@e _ inst _ : X) ∧
    Eq.{v + 1} (α := Y) ((hmul : (a : Y × Y) → Y) (@e _ inst_1 _, @e _ inst_1 _) : Y) (@e _ inst_1 _ : Y)

Tactic:
exact ⟨HSpace.hmul_e_e, HSpace.hmul_e_e⟩
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
⊢ Continuous G

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
⊢ Continuous G

Tactic:
have hG : Continuous G := by fun_prop
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x, y) =
    (comp
          {
            toFun := fun (p : (X × Y) × X × Y) ↦
              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
          (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))) :
        (a : X × Y) → X × Y)
      (x, y)

Tactic:
Prod.ext (HSpace.eHmul.1.2 x) (HSpace.eHmul.1.2 y)

Premises used: HSpace.eHmul, Prod.ext, ContinuousMap.HomotopyWith.toHomotopy, ContinuousMap.Homotopy.map_zero_left
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x, y) =
    (comp
          {
            toFun := fun (p : (X × Y) × X × Y) ↦
              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
          (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))) :
        (a : X × Y) → X × Y)
      (x, y)

Tactic:
exact Prod.ext (HSpace.eHmul.1.2 x) (HSpace.eHmul.1.2 y)

Premises used: Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x, y) =
    (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) (x, y)

Tactic:
Prod.ext (HSpace.eHmul.1.3 x) (HSpace.eHmul.1.3 y)

Premises used: HSpace.eHmul, Prod.ext, ContinuousMap.HomotopyWith.toHomotopy, ContinuousMap.Homotopy.map_one_left
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x, y) =
    (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) (x, y)

Tactic:
exact Prod.ext (HSpace.eHmul.1.3 x) (HSpace.eHmul.1.3 y)

Premises used: Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
t : (↑I : Type)
x : X
y : Y
h : Membership.mem (γ := Set (X × Y)) {(@e _ inst _, @e _ inst_1 _)} (x, y)
⊢ x = @e _ inst _ ∧ y = @e _ inst_1 _

Tactic:
replace h := Prod.mk_inj.mp h
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
t : (↑I : Type)
x : X
y : Y
h : x = @e _ inst _ ∧ y = @e _ inst_1 _
⊢ Eq (α := X × Y)
    (({
            toFun := fun (x : X × Y) ↦
              (Homotopy.toContinuousMap (f₀ :=
                    comp
                      {
                        toFun := fun (p : (X × Y) × X × Y) ↦
                          ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                        continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                      (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
                    (f₁ := ContinuousMap.id (X × Y))
                    { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ :
                      Homotopy
                        (comp
                          {
                            toFun := fun (p : (X × Y) × X × Y) ↦
                              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                          (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
                        (ContinuousMap.id (X × Y)) }).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X × Y, X × Y) } :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)
    ((comp
            {
              toFun := fun (p : (X × Y) × X × Y) ↦
                ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
              continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
            (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))) :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)

Tactic:
Prod.ext (HSpace.eHmul.2 t x h.1) (HSpace.eHmul.2 t y h.2)

Premises used: ContinuousMap.HomotopyWith.prop', HSpace.eHmul, And.right, And.left, Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
t : (↑I : Type)
x : X
y : Y
h : x = @e _ inst _ ∧ y = @e _ inst_1 _
⊢ Eq (α := X × Y)
    (({
            toFun := fun (x : X × Y) ↦
              (Homotopy.toContinuousMap (f₀ :=
                    comp
                      {
                        toFun := fun (p : (X × Y) × X × Y) ↦
                          ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                        continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                      (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
                    (f₁ := ContinuousMap.id (X × Y))
                    { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ :
                      Homotopy
                        (comp
                          {
                            toFun := fun (p : (X × Y) × X × Y) ↦
                              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                          (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
                        (ContinuousMap.id (X × Y)) }).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X × Y, X × Y) } :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)
    ((comp
            {
              toFun := fun (p : (X × Y) × X × Y) ↦
                ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
              continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
            (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))) :
          (a : X × Y) → X × Y)
        (x, y) :
      X × Y)

Tactic:
exact Prod.ext (HSpace.eHmul.2 t x h.1) (HSpace.eHmul.2 t y h.2)

Premises used: Prod.ext
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((hmulE : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (hmulE : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
⊢ Continuous G

Tactic:
fun_prop