awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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)) : ℝ)
⊢ (↑(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:
rw [Unique.eq_default i]

Premises used: Unique.eq_default
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)) default) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ) - 1)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
neg : ∀ (h : ¬i = j), Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)

Tactic:
by_cases h : i = j
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i = j
pos pos₁ : Eq (α := Group (HomotopyGroup N X x)) (auxGroup j) (auxGroup j)
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)

Tactic:
rw [h]
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)

Tactic:
Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)

Premises used: HomotopyGroup.isUnital_auxGroup, EckmannHilton.mul, Group.ext
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : ¬i = j
neg : ∀ (a b c d : HomotopyGroup N X x), a * b * (c * d) = a * c * (b * d)
⊢ Eq (α := Group (HomotopyGroup N X x)) (auxGroup i) (auxGroup j)

Tactic:
refine Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)

Premises used: EckmannHilton.mul, Group.ext
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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))⟧
⊢ Eq (α := Quotient (α := (↑(Ω^ N X x) : Type (max u_2 u_1))) (Homotopic.setoid N x)) ⟦transAt i f g⟧ ⟦transAt j f g⟧

Tactic:
simp_rw [← fromLoop_trans_toLoop]

Premises used: GenLoop.fromLoop_trans_toLoop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
m : (G : Type (max u_2 u_1)) → Group G → G → G → G := fun (G : Type (max u_2 u_1)) (x : Group G) (x1 x2 : G) ↦ x1 * x2
⊢ 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:
congr_fun₂ (congr_arg (m <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦g⟧ ⟦f⟧

Premises used: GenLoop.toLoop, HomotopyGroup.auxGroup_indep, congr_fun₂, Quotient.mk, congr_arg, HomotopyGroup, Quot.map, GenLoop.fromLoop, GenLoop.const
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
m : (G : Type (max u_2 u_1)) → Group G → G → G → G := fun (G : Type (max u_2 u_1)) (x : Group G) (x1 x2 : G) ↦ x1 * x2
⊢ 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:
exact congr_fun₂ (congr_arg (m <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦g⟧ ⟦f⟧

Premises used: HomotopyGroup.auxGroup_indep, congr_fun₂, Quotient.mk, congr_arg, HomotopyGroup
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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))⟧
⊢ Eq (α := Quotient (α := (↑(Ω^ N X x) : Type (max u_2 u_1))) (Homotopic.setoid N x)) ⟦symmAt i f⟧ ⟦symmAt j f⟧

Tactic:
simp_rw [← fromLoop_symm_toLoop]

Premises used: GenLoop.fromLoop_symm_toLoop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
inv : (G : Type (max u_2 u_1)) → Group G → G → G := fun (G : Type (max u_2 u_1)) (x : Group G) (x_1 : G) ↦ x_1⁻¹
⊢ 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:
congr_fun (congr_arg (inv <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦f⟧

Premises used: GenLoop.toLoop, HomotopyGroup.auxGroup_indep, Quotient.mk, congr_arg, HomotopyGroup, Quot.map, congr_fun, GenLoop.fromLoop, GenLoop.const
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
inv : (G : Type (max u_2 u_1)) → Group G → G → G := fun (G : Type (max u_2 u_1)) (x : Group G) (x_1 : G) ↦ x_1⁻¹
⊢ 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:
exact congr_fun (congr_arg (inv <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦f⟧

Premises used: HomotopyGroup.auxGroup_indep, Quotient.mk, congr_arg, HomotopyGroup, congr_fun
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
inst_2 : Nonempty N
⊢ Eq (α := HomotopyGroup N X x) 1 ⟦const⟧

Tactic:
rfl

Premises used: ContinuousMap.comp, Quot.map, ContinuousMap.const, GenLoop.fromLoop, GenLoop.const, rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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))⟧
⊢ Eq (α := HomotopyGroup N X x) ((fun (x1 x2 : HomotopyGroup N X x) ↦ x1 * x2) ⟦p⟧ ⟦q⟧) ⟦transAt i q p⟧

Tactic:
rw [transAt_indep (Classical.arbitrary N) q, ← fromLoop_trans_toLoop]

Premises used: HomotopyGroup.transAt_indep, Classical.arbitrary, GenLoop.fromLoop_trans_toLoop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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)))
⊢ 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:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
⊢ (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:
rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
rw :
  Eq (α := HomotopyGroup N X x) (⟦p⟧)⁻¹
    ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧
⊢ Eq (α := HomotopyGroup N X x) (⟦p⟧)⁻¹ ⟦symmAt i p⟧

Tactic:
rw [symmAt_indep (Classical.arbitrary N) p, ← fromLoop_symm_toLoop]

Premises used: HomotopyGroup.symmAt_indep, GenLoop.fromLoop_symm_toLoop, Classical.arbitrary
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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)))
⊢ Eq (α := HomotopyGroup N X x) (⟦p⟧)⁻¹
    ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
⊢ (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:
rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
simp :
  Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦transAt default q p⟧ =
    Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦p⟧ *
      Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦q⟧
⊢ Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) (HMul.hMul (α := HomotopyGroup N X x) ⟦p⟧ ⟦q⟧) =
    Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦p⟧ *
      Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦q⟧

Tactic:
simp only [HomotopyGroup.mul_spec (i := default)]

Premises used: HomotopyGroup.mul_spec
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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)
⊢ Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦transAt default q p⟧ =
    Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦p⟧ *
      Equiv.toFun (homotopyGroupEquivFundamentalGroupOfUnique N) ⟦q⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
⊢ 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:
simp [genLoopEquivOfUnique_transAt]

Premises used: HomotopyGroup.genLoopEquivOfUnique_transAt
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
simp :
  Equiv.toFun pi1EquivFundamentalGroup ⟦transAt 0 q p⟧ =
    Equiv.toFun pi1EquivFundamentalGroup ⟦p⟧ * Equiv.toFun pi1EquivFundamentalGroup ⟦q⟧
⊢ Equiv.toFun pi1EquivFundamentalGroup (HMul.hMul (α := π_ 1 X x) ⟦p⟧ ⟦q⟧) =
    Equiv.toFun pi1EquivFundamentalGroup ⟦p⟧ * Equiv.toFun pi1EquivFundamentalGroup ⟦q⟧

Tactic:
simp only [HomotopyGroup.mul_spec (i := (0 : Fin 1))]

Premises used: HomotopyGroup.mul_spec
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
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)
⊢ Equiv.toFun pi1EquivFundamentalGroup ⟦transAt 0 q p⟧ =
    Equiv.toFun pi1EquivFundamentalGroup ⟦p⟧ * Equiv.toFun pi1EquivFundamentalGroup ⟦q⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
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)
a₂ a₃ :
  (Path.Homotopic.setoid { as := x }.as { as := x }.as :
      Path { as := x }.as { as := x }.as → Path { as := x }.as { as := x }.as → Prop)
    (Path.trans (y := x) ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) q)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) p) :
      Path x x)
    (Path.trans (y := x) ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) q)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) p) :
      Path x x)
⊢ 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:
rw [Unique.eq_default 0, genLoopEquivOfUnique_transAt]

Premises used: HomotopyGroup.genLoopEquivOfUnique_transAt, Unique.eq_default, OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
homeo : IsLocalHomeomorph p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
a : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
choose :
  ∀ (q : (x : E) → OpenPartialHomeomorph E X) (mem_source : ∀ (x : E), x ∈ (q x).source)
    (hpq : ∀ (x : E), p = (↑(q x) : E → X)),
    ∃ N ∈ 𝓝 a,
      ∃ (g' : (↑I : Type) × A → E),
        ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
          p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
            (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)
⊢ ∃ N ∈ 𝓝 a,
    ∃ (g' : (↑I : Type) × A → E),
      ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
        p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
          (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)

Tactic:
choose q mem_source hpq using homeo
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
a : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
q : (x : E) → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = (↑(q x) : E → X)
obtain :
  ∀ (t : ℕ → (↑I : Type)) (t_0 : t 0 = 0) (t_mono : Monotone t)
    (t_sub : ∀ (n : ℕ), ∃ (i : E), Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q i).source)
    (n_max : ℕ) (h_max : ∀ m ≥ n_max, t m = 1),
    ∃ N ∈ 𝓝 a,
      ∃ (g' : (↑I : Type) × A → E),
        ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
          p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
            (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)
⊢ ∃ N ∈ 𝓝 a,
    ∃ (g' : (↑I : Type) × A → E),
      ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
        p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
          (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)

Tactic:
obtain ⟨t, t_0, t_mono, ⟨n_max, h_max⟩, t_sub⟩ :=
    exists_monotone_Icc_subset_open_cover_unitInterval
      (fun e ↦ (q e).open_source.preimage cont_a)
      fun t _ ↦ Set.mem_iUnion.mpr ⟨g (t, a), mem_source _⟩

Premises used: Iff.mpr, OpenPartialHomeomorph.open_source, Set.mem_iUnion, Prod.mk, Exists.intro, exists_monotone_Icc_subset_open_cover_unitInterval, IsOpen.preimage