awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (hypothesis)
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N_1
N : Type u_3
inst_2 : Unique N
a₁ a₂ : (↑(Ω^ N X x) : Type (max u_2 u_3))
H :
  Path.Homotopy (X := X) (x₀ := { as := x }.as) (x₁ := { as := x }.as)
    ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as) a₁)
    ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as) a₂)
t : (↑I : Type)
y : N → (↑I : Type)
i : N
iH : y i = 0 ∨ y i = 1
⊢ Eq.{u_2 + 1} (α := X)
    ((({
              toFun := fun (x_1 : N → (↑I : Type)) ↦
                (ContinuousMap.Homotopy.toContinuousMap (f₀ := (↑a₁ : C(N → (↑I : Type), X))) (f₁ :=
                      (↑a₂ : C(N → (↑I : Type), X)))
                      {
                        toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
                          (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
                        continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ :
                        (↑a₁ : C(N → (↑I : Type), X)).Homotopy (↑a₂ : C(N → (↑I : Type), X)) }).toFun
                  (t, x_1),
              continuous_toFun := ⋯ } :
            ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    (((↑a₁ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)
have iH₁ : y default = 0 ∨ y default = 1
Tactic: cases Unique.eq_default i
Cleared hypotheses: i, iH
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
⊢ Eq.{u_2 + 1} (α := Ω X x)
    ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) (transAt default q p) : Ω X x)
    (Path.trans (y := x) ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) q)
        ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) p) :
      Path x x)
have a : ∀ (t : (↑I : Type)),
  Eq (α := X)
    ((((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) (transAt default q p) : Ω X x) :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((Path.trans (y := x) ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) q)
              ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) p) :
            Path x x) :
          (a : (↑I : Type)) → X)
        t :
      X)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
⊢ Eq (α := X)
    ((((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) (transAt default q p) : Ω X x) :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((Path.trans (y := x) ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) q)
              ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Ω X x) p) :
            Path x x) :
          (a : (↑I : Type)) → X)
        t :
      X)
have a : Eq (α := X)
  (if (↑t : ℝ) ≤ 2⁻¹ then
      (q : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))))
    else
      (p : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1))) :
    X)
  (if (↑t : ℝ) ≤ 2⁻¹ then
      ({ toFun := fun (t : (↑I : Type)) ↦ (q : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := sorry,
              source' := sorry, target' := sorry : Path x x }.extend :
          (a : ℝ) → X)
        (2 * (↑t : ℝ))
    else
      ({ toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := sorry,
              source' := sorry, target' := sorry : Path x x }.extend :
          (a : ℝ) → X)
        (2 * (↑t : ℝ) - 1) :
    X)
Tactic: simp only [genLoopEquivOfUnique, GenLoop.transAt, GenLoop.copy,
    one_div, Equiv.coe_fn_mk, GenLoop.mk_apply, ContinuousMap.coe_mk, Path.coe_mk', Path.trans,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
⊢ Eq (α := X)
    (if (↑t : ℝ) ≤ 2⁻¹ then
        (q : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))))
      else
        (p : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1))) :
      X)
    (if (↑t : ℝ) ≤ 2⁻¹ then
        ({ toFun := fun (t : (↑I : Type)) ↦ (q : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := ⋯,
                source' := ⋯, target' := ⋯ : Path x x }.extend :
            (a : ℝ) → X)
          (2 * (↑t : ℝ))
      else
        ({ toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := ⋯,
                source' := ⋯, target' := ⋯ : Path x x }.extend :
            (a : ℝ) → X)
          (2 * (↑t : ℝ) - 1) :
      X)
have a : (↑t : ℝ) ≤ 2⁻¹ →
  Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))) =
    fun (x : N) ↦ Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))
Tactic: refine ite_congr rfl (fun _ ↦ congrArg q ?_)
    fun _ ↦ congrArg p ?_
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
a :
  (↑t : ℝ) ≤ 2⁻¹ →
    Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))) =
      fun (x : N) ↦ Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))
⊢ Eq (α := X)
    (if (↑t : ℝ) ≤ 2⁻¹ then
        (q : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))))
      else
        (p : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1))) :
      X)
    (if (↑t : ℝ) ≤ 2⁻¹ then
        ({ toFun := fun (t : (↑I : Type)) ↦ (q : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := ⋯,
                source' := ⋯, target' := ⋯ : Path x x }.extend :
            (a : ℝ) → X)
          (2 * (↑t : ℝ))
      else
        ({ toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := ⋯,
                source' := ⋯, target' := ⋯ : Path x x }.extend :
            (a : ℝ) → X)
          (2 * (↑t : ℝ) - 1) :
      X)
have a₁ : ¬(↑t : ℝ) ≤ 2⁻¹ →
  Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1)) =
    fun (x : N) ↦ Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ) - 1)
Tactic: refine ite_congr rfl (fun _ ↦ congrArg q ?_)
    fun _ ↦ congrArg p ?_
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
h : (↑t : ℝ) ≤ 2⁻¹
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))) =
    fun (x : N) ↦ Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))
have a : ∀ (i : N),
  (↑(Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))) i) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))) : ℝ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
h : (↑t : ℝ) ≤ 2⁻¹
i : N
⊢ (↑(Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))) i) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))) : ℝ)
have a : (↑(Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ))) default) :
    ℝ) =
  (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))) : ℝ)
Tactic: rw [Unique.eq_default i]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 2⁻¹
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1)) =
    fun (x : N) ↦ Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ) - 1)
have a : ∀ (i : N),
  (↑(Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1)) i) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ) - 1)) : ℝ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
N : Type u_3
inst_1 : DecidableEq N
inst_2 : Unique N
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 2⁻¹
i : N
⊢ (↑(Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1)) i) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ) - 1)) : ℝ)
have a : (↑(Function.update (β := fun (a : N) ↦ (↑I : Type)) (fun (x : N) ↦ t) default
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑t : ℝ) - 1)) default) :
    ℝ) =
  (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ) - 1)) : ℝ)
Tactic: rw [Unique.eq_default i]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
have pos : ∀ (h : i = j), Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
pos : ∀ (h : i = j), Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
have neg : ∀ (h : ¬i = j), Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i = j
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
have pos : Eq (α := Group (HomotopyGroup N X x)) (auxGroup j) (auxGroup j)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : ¬i = j
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
have neg : ∀ (a b c d : HomotopyGroup N X x), a * b * (c * d) = a * c * (b * d)
Tactic: refine Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := Quotient (α := (↑(Ω^ N X x) : Type (max u_2 u_1))) (Homotopic.setoid N x)) ⟦transAt i f g⟧ ⟦transAt j f g⟧
have simp_rw : Eq (α := Quotient (α := (↑(Ω^ N X x) : Type (max u_2 u_1))) (Homotopic.setoid N x))
  ⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧
Tactic: simp_rw [← fromLoop_trans_toLoop]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := Quotient (α := (↑(Ω^ N X x) : Type (max u_2 u_1))) (Homotopic.setoid N x)) ⟦symmAt i f⟧ ⟦symmAt j f⟧
have simp_rw : Eq (α := Quotient (α := (↑(Ω^ N X x) : Type (max u_2 u_1))) (Homotopic.setoid N x))
  ⟦fromLoop i (Path.symm (toLoop i f))⟧ ⟦fromLoop j (Path.symm (toLoop j f))⟧
Tactic: simp_rw [← fromLoop_symm_toLoop]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
inst_2 : Nonempty N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := HomotopyGroup N X x) ((fun (x1 x2 : HomotopyGroup N X x) ↦ x1 * x2) ⟦p⟧ ⟦q⟧) ⟦transAt i q p⟧
have rw : Eq (α := HomotopyGroup N X x) ((fun (x1 x2 : HomotopyGroup N X x) ↦ x1 * x2) ⟦p⟧ ⟦q⟧)
  ⟦fromLoop (Classical.arbitrary N) (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧
Tactic: rw [transAt_indep (Classical.arbitrary N) q, ← fromLoop_trans_toLoop]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
inst_2 : Nonempty N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := HomotopyGroup N X x) ((fun (x1 x2 : HomotopyGroup N X x) ↦ x1 * x2) ⟦p⟧ ⟦q⟧)
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧
have a : (Homotopic.setoid N x : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop)
  ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
        (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
      (Path.trans (y := FundamentalGroupoid.as { as := const })
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          q)
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          p)) :
    (↑(Ω^ N X x) : Type (max u_2 u_1)))
  ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
        (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
      (Path.trans (y := FundamentalGroupoid.as { as := const })
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          q)
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          p)) :
    (↑(Ω^ N X x) : Type (max u_2 u_1)))
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
inst_2 : Nonempty N
i : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := HomotopyGroup N X x) (⟦p⟧)⁻¹ ⟦symmAt i p⟧
have rw : Eq (α := HomotopyGroup N X x) (⟦p⟧)⁻¹ ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧
Tactic: rw [symmAt_indep (Classical.arbitrary N) p, ← fromLoop_symm_toLoop]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
inst_2 : Nonempty N
i : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := HomotopyGroup N X x) (⟦p⟧)⁻¹
    ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧
have a : (Homotopic.setoid N x : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop)
  ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
        (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
      (Path.symm
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          p)) :
    (↑(Ω^ N X x) : Type (max u_2 u_1)))
  ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
        (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
      (Path.symm
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          p)) :
    (↑(Ω^ N X x) : Type (max u_2 u_1)))
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N_1
N : Type u_3
inst_2 : Unique N
a b : HomotopyGroup N X x
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
⊢ Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) (HMul.hMul (α := HomotopyGroup N X x) ⟦p⟧ ⟦q⟧) =
    Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦p⟧ *
      Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦q⟧
have simp : Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦transAt default q p⟧ =
  Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦p⟧ *
    Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦q⟧
Tactic: simp only [HomotopyGroup.mul_spec (i := default)]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N_1
N : Type u_3
inst_2 : Unique N
a b : HomotopyGroup N X x
p q : (↑(Ω^ N X x) : Type (max u_2 u_3))
⊢ Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦transAt default q p⟧ =
    Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦p⟧ *
      Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦q⟧
have a₁ : HasEquiv.Equiv.{u_2 + 1, 0} (α := Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
  ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as)
      (transAt default q p) :
    Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
  (Path.trans (y := { as := x }.as)
      ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as) q)
      ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as) p) :
    Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
a b : π_ 1 X x
p q : (↑(Ω^ (Fin 1) X x) : Type u_2)
⊢ Equiv.toFun pi1EquivFundamentalGroup (HMul.hMul (α := π_ 1 X x) ⟦p⟧ ⟦q⟧) =
    Equiv.toFun pi1EquivFundamentalGroup ⟦p⟧ * Equiv.toFun pi1EquivFundamentalGroup ⟦q⟧
have simp : Equiv.toFun pi1EquivFundamentalGroup ⟦transAt 0 q p⟧ =
  Equiv.toFun pi1EquivFundamentalGroup ⟦p⟧ * Equiv.toFun pi1EquivFundamentalGroup ⟦q⟧
Tactic: simp only [HomotopyGroup.mul_spec (i := (0 : Fin 1))]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
a b : π_ 1 X x
p q : (↑(Ω^ (Fin 1) X x) : Type u_2)
⊢ Equiv.toFun pi1EquivFundamentalGroup ⟦transAt 0 q p⟧ =
    Equiv.toFun pi1EquivFundamentalGroup ⟦p⟧ * Equiv.toFun pi1EquivFundamentalGroup ⟦q⟧
have a₁ : HasEquiv.Equiv (α := Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
  ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as)
      (transAt 0 q p) :
    Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
  (Path.trans (y := { as := x }.as)
      ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) q)
      ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) p) :
    Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
a b : π_ 1 X x
p q : (↑(Ω^ (Fin 1) X x) : Type u_2)
⊢ HasEquiv.Equiv (α := Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
    ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as)
        (transAt 0 q p) :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
    (Path.trans (y := { as := x }.as)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) q)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) p) :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
have a₁ : HasEquiv.Equiv (α := Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
  ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as)
      (transAt default q p) :
    Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
  (Path.trans (y := { as := x }.as)
      ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) q)
      ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) p) :
    Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
Tactic: rw [Unique.eq_default 0, genLoopEquivOfUnique_transAt]