awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
pos :
  ∀ (h : (↑t : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y)
      (({
              toFun := fun (x : X) ↦
                (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ)) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
              continuous_toFun := ⋯ : C(X, Y) } :
            (a : X) → Y)
          x :
        Y)
      ((f₀ : (a : X) → Y) x : Y)
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              if (↑t : ℝ) ≤ 1 / 2 then
                (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ)) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x
              else
                (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ) - 1) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)
have neg : ∀ (h : ¬(↑t : ℝ) ≤ 1 / 2),
  Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                            ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                        (a : ℝ) → C(X, Y))
                      (2 * (↑t : ℝ) - 1) :
                    C(X, Y)) :
                  (a : X) → Y)
                x,
            continuous_toFun := sorry : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : f.Nullhomotopic
g : C(Y, Z)
⊢ (g.comp f).Nullhomotopic
have obtain : ∀ (y : Y) (hy : f.Homotopic (const X y)), (g.comp f).Nullhomotopic
Tactic: obtain ⟨y, hy⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Nullhomotopic
have h : (g.comp f).Homotopic (const X ((g : (a : Y) → Z) y))
Tactic: use g y
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(Y, Z)
hf : f.Nullhomotopic
g : C(X, Y)
⊢ (f.comp g).Nullhomotopic
have obtain : ∀ (y : Z) (hy : f.Homotopic (const Y y)), (f.comp g).Nullhomotopic
Tactic: obtain ⟨y, hy⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Nullhomotopic
have h : (f.comp g).Homotopic (const X y)
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
⊢ Nullhomotopic (ContinuousMap.id X)
have obtain : ∀ (hv : X ≃ₕ Unit), Nullhomotopic (ContinuousMap.id X)
Tactic: obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Nullhomotopic (ContinuousMap.id X)
have h : Homotopic (ContinuousMap.id X) (const X ((hv.invFun : (a : Unit) → X) ()))
Tactic: use hv.invFun ()
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
Y : Type u_1
inst : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ Nullhomotopic (ContinuousMap.id Y)
have mp : ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
Y : Type u_1
inst : TopologicalSpace Y
mp : ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)
⊢ ContractibleSpace Y ↔ Nullhomotopic (ContinuousMap.id Y)
have mpr : Nullhomotopic (ContinuousMap.id Y) → ContractibleSpace Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ ContractibleSpace Y
have mpr : Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)
Tactic: refine
    { hequiv_unit' :=
        ⟨{  toFun := ContinuousMap.const _ ()
            invFun := ContinuousMap.const _ p
            left_inv := ?_
            right_inv := ?_ }⟩ }
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
mpr : Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)
⊢ ContractibleSpace Y
have mpr₁ : Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)
Tactic: refine
    { hequiv_unit' :=
        ⟨{  toFun := ContinuousMap.const _ ()
            invFun := ContinuousMap.const _ p
            left_inv := ?_
            right_inv := ?_ }⟩ }
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
f : C(X, Y)
⊢ f.Nullhomotopic
have inhabit : ∀ (inhabited_h : Inhabited Y), f.Nullhomotopic
Tactic: inhabit Y
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
⊢ f.Nullhomotopic
have h : f.Homotopic (const X default)
Tactic: use default
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
⊢ Nonempty (X ≃ₕ Y)
have rcases : ∀ (h : X ≃ₕ Unit), Nonempty (X ≃ₕ Y)
Tactic: rcases ContractibleSpace.hequiv_unit' (X := X) with ⟨h⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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
⊢ Nonempty (X ≃ₕ Y)
have rcases : ∀ (h' : Y ≃ₕ Unit), Nonempty (X ≃ₕ Y)
Tactic: rcases ContractibleSpace.hequiv_unit' (X := Y) with ⟨h'⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
⊢ PathConnectedSpace X
have obtain : ∀ (p : X) (h : Homotopy (ContinuousMap.id X) (const X p)), PathConnectedSpace X
Tactic: obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (hypothesis)
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)
⊢ PathConnectedSpace X
have this : ∀ (x : X), Joined p x
Tactic: have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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
⊢ PathConnectedSpace X
have rw : ∃ (x : X), pathComponent x = Set.univ
Tactic: rw [pathConnectedSpace_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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), pathComponent x = Set.univ
have h₁ : pathComponent p = Set.univ
Tactic: use p
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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
⊢ pathComponent p = Set.univ
have h₁ : ∀ (x : X), x ∈ pathComponent p ↔ Membership.mem (γ := Set X) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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
⊢ x ∈ pathComponent p ↔ Membership.mem (γ := Set X) Set.univ x
have h₁ : x ∈ pathComponent p → Membership.mem (γ := Set X) Set.univ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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
⊢ x ∈ pathComponent p ↔ Membership.mem (γ := Set X) Set.univ x
have h₂ : Membership.mem (γ := Set X) Set.univ x → x ∈ pathComponent p
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace X
inst_3 : ContractibleSpace Y
⊢ ContractibleSpace (X × Y)
have obtain : ∀ (hX : X ≃ₕ Unit), ContractibleSpace (X × Y)
Tactic: obtain ⟨hX⟩ := hequiv_unit' (X := X)
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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
⊢ ContractibleSpace (X × Y)
have obtain : ∀ (hY : Y ≃ₕ Unit), ContractibleSpace (X × Y)
Tactic: obtain ⟨hY⟩ := hequiv_unit' (X := Y)
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Contractible (goal)
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)
have refine : Unit × Unit ≃ₕ Unit
Tactic: refine ⟨⟨(hX.prodCongr hY).trans ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Equiv (goal)
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
⊢ Homotopic (comp (↑h.symm : C(Y, X)) (↑h : C(X, Y))) (ContinuousMap.id X)
have rw : Homotopic (ContinuousMap.id X) (ContinuousMap.id X)
Tactic: rw [symm_comp_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Equiv (goal)
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
⊢ Homotopic (comp (↑h : C(X, Y)) (↑h.symm : C(Y, X))) (ContinuousMap.id Y)
have rw : Homotopic (ContinuousMap.id Y) (ContinuousMap.id Y)
Tactic: rw [toContinuousMap_comp_symm]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Equiv (goal)
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)
have refine : ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (h₁.invFun.comp h₁.toFun)
Tactic: refine Homotopic.trans ?_ h₁.left_inv
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Equiv (goal)
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)
have refine : ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (h₂.toFun.comp h₂.invFun)
Tactic: refine Homotopic.trans ?_ h₂.right_inv
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace 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)
have 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)
Tactic: simp only [ContinuousMap.coe_mk, Prod.mk_inj]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (hypothesis)
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))
⊢ HomotopyRel
    (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)) {(@e _ inst _, @e _ inst_1 _)}
have hG : Continuous G
Tactic: have hG : Continuous G := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
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
⊢ HomotopyRel
    (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)) {(@e _ inst _, @e _ inst_1 _)}
have map_zero_left : ∀ (x : X × Y),
  { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x) =
    (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 := sorry : 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
Tactic: use! ⟨G, hG⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
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
map_zero_left :
  ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x) =
      (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
⊢ HomotopyRel
    (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)) {(@e _ inst _, @e _ inst_1 _)}
have map_one_left : ∀ (x : X × Y),
  { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x) =
    (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) x
Tactic: use! ⟨G, hG⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (hypothesis)
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)
⊢ 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)
have h₁ : x = @e _ inst _ ∧ y = @e _ inst_1 _
Tactic: replace h := Prod.mk_inj.mp h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (hypothesis)
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))
⊢ HomotopyRel
    (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 (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
    (ContinuousMap.id (X × Y)) {(@e _ inst _, @e _ inst_1 _)}
have hG : Continuous G
Tactic: have hG : Continuous G := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
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))
hG : Continuous G
⊢ HomotopyRel
    (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 (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
    (ContinuousMap.id (X × Y)) {(@e _ inst _, @e _ inst_1 _)}
have map_zero_left : ∀ (x : X × Y),
  { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x) =
    (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 := sorry : C((X × Y) × X × Y, X × Y) }
          (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))) :
        (a : X × Y) → X × Y)
      x
Tactic: use! ⟨G, hG⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HSpaces (goal)
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))
hG : Continuous G
map_zero_left :
  ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x) =
      (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 (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))) :
          (a : X × Y) → X × Y)
        x
⊢ HomotopyRel
    (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 (ContinuousMap.id (X × Y)) (const (X × Y) (@e _ inst _, @e _ inst_1 _))))
    (ContinuousMap.id (X × Y)) {(@e _ inst _, @e _ inst_1 _)}
have map_one_left : ∀ (x : X × Y),
  { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x) =
    (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) x
Tactic: use! ⟨G, hG⟩