awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ a₂ : (↑(Ω^ N X x) : Type (max u_2 u_3))
H : (↑a₁ : C(N → (↑I : Type), X)).HomotopyRel (↑a₂ : C(N → (↑I : Type), X)) (Cube.boundary N)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as :
      Path { as := x }.as { as := x }.as → Path { as := x }.as { as := x }.as → Prop)
    ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as) a₁ :
      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) a₂ :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)

Tactic:
⟨{  toFun := fun tx ↦ H (tx.fst, fun _ ↦ tx.snd)
            map_zero_left := fun _ ↦ H.apply_zero _
            map_one_left := fun _ ↦ H.apply_one _
            prop' := fun t y iH ↦ H.prop' _ _ ⟨default, iH⟩ }⟩

Premises used: Inhabited.default, ContinuousMap.HomotopyWith.prop', ContinuousMap.HomotopyWith.apply_one, ContinuousMap.mk, ContinuousMap.HomotopyWith.mk, Prod.mk, Nonempty.intro, Prod.fst, Exists.intro, Path.Homotopic, ContinuousMap.HomotopyWith.apply_zero, OfNat.ofNat, ContinuousMap.Homotopy.mk, Prod.snd, DFunLike.coe
-- 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₁ a₂ : (↑(Ω^ N X x) : Type (max u_2 u_3))
H : (↑a₁ : C(N → (↑I : Type), X)).HomotopyRel (↑a₂ : C(N → (↑I : Type), X)) (Cube.boundary N)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as :
      Path { as := x }.as { as := x }.as → Path { as := x }.as { as := x }.as → Prop)
    ((genLoopEquivOfUnique N : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → Path { as := x }.as { as := x }.as) a₁ :
      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) a₂ :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)

Tactic:
exact
        ⟨{  toFun := fun tx ↦ H (tx.fst, fun _ ↦ tx.snd)
            map_zero_left := fun _ ↦ H.apply_zero _
            map_one_left := fun _ ↦ H.apply_one _
            prop' := fun t y iH ↦ H.prop' _ _ ⟨default, iH⟩ }⟩
-- 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₁ 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₂)
⊢ (Homotopic.setoid N x : (↑(Ω^ N X x) : Type (max u_2 u_3)) → (↑(Ω^ N X x) : Type (max u_2 u_3)) → Prop) a₁ a₂

Tactic:
⟨⟨⟨⟨fun tx ↦ H (tx.fst, tx.snd default), H.continuous.comp ?_⟩, fun y ↦ ?_, fun y ↦ ?_⟩, ?_⟩⟩

Premises used: Inhabited.default, GenLoop.Homotopic, ContinuousMap.mk, Continuous.comp, ContinuousMap.HomotopicRel, ContinuousMap.HomotopyWith.mk, Prod.mk, Nonempty.intro, Prod.fst, ContinuousMap.HomotopyWith.continuous, ContinuousMap.Homotopy.mk, Prod.snd, DFunLike.coe
-- 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₁ 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₂)
mpr : Continuous (Y := (↑I : Type) × (↑I : Type)) fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦ (tx.1, tx.2 default)
mpr₁ :
  ∀ (y : N → (↑I : Type)),
    {
            toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
              (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
            continuous_toFun := ⋯ : ContinuousMap.{u_3, u_2} ((↑I : Type) × (N → (↑I : Type))) X }.toFun
        (0, y) =
      ((↑a₁ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y
mpr₂ :
  ∀ (y : N → (↑I : Type)),
    {
            toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
              (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
            continuous_toFun := ⋯ : ContinuousMap.{u_3, u_2} ((↑I : Type) × (N → (↑I : Type))) X }.toFun
        (1, y) =
      ((↑a₂ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y
mpr₃ :
  ∀ (t : (↑I : Type)),
    ∀ x_1 ∈ Cube.boundary N,
      Eq.{u_2 + 1} (α := X)
        ((({
                  toFun := fun (x_2 : 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_2),
                  continuous_toFun := ⋯ } :
                ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) :
              (a : N → (↑I : Type)) → X)
            x_1 :
          X)
        (((↑a₁ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ (Homotopic.setoid N x : (↑(Ω^ N X x) : Type (max u_2 u_3)) → (↑(Ω^ N X x) : Type (max u_2 u_3)) → Prop) a₁ a₂

Tactic:
refine
      ⟨⟨⟨⟨fun tx ↦ H (tx.fst, tx.snd default), H.continuous.comp ?_⟩, fun y ↦ ?_, fun y ↦ ?_⟩, ?_⟩⟩
-- 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₁ 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₂)
⊢ Continuous (Y := (↑I : Type) × (↑I : Type)) fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦ (tx.1, tx.2 default)

Tactic:
fun_prop
-- 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₁ 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₂)
y : N → (↑I : Type)
⊢ {
          toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
            (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
          continuous_toFun := ⋯ : ContinuousMap.{u_3, u_2} ((↑I : Type) × (N → (↑I : Type))) X }.toFun
      (0, y) =
    ((↑a₁ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y

Tactic:
(H.apply_zero _).trans (congr_arg a₁ (eq_const_of_unique y).symm)

Premises used: congr_arg, ContinuousMap.HomotopyWith.apply_zero, Eq.symm, DFunLike.coe, Eq.trans, eq_const_of_unique
-- 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₁ 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₂)
y : N → (↑I : Type)
⊢ {
          toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
            (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
          continuous_toFun := ⋯ : ContinuousMap.{u_3, u_2} ((↑I : Type) × (N → (↑I : Type))) X }.toFun
      (0, y) =
    ((↑a₁ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y

Tactic:
exact (H.apply_zero _).trans (congr_arg a₁ (eq_const_of_unique y).symm)

Premises used: congr_arg, ContinuousMap.HomotopyWith.apply_zero, Eq.symm, DFunLike.coe, Eq.trans, eq_const_of_unique
-- 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₁ 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₂)
y : N → (↑I : Type)
⊢ {
          toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
            (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
          continuous_toFun := ⋯ : ContinuousMap.{u_3, u_2} ((↑I : Type) × (N → (↑I : Type))) X }.toFun
      (1, y) =
    ((↑a₂ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y

Tactic:
(H.apply_one _).trans (congr_arg a₂ (eq_const_of_unique y).symm)

Premises used: ContinuousMap.HomotopyWith.apply_one, congr_arg, Eq.symm, DFunLike.coe, Eq.trans, eq_const_of_unique
-- 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₁ 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₂)
y : N → (↑I : Type)
⊢ {
          toFun := fun (tx : (↑I : Type) × (N → (↑I : Type))) ↦
            (H : (a : (↑I : Type) × (↑I : Type)) → X) (tx.1, tx.2 default),
          continuous_toFun := ⋯ : ContinuousMap.{u_3, u_2} ((↑I : Type) × (N → (↑I : Type))) X }.toFun
      (1, y) =
    ((↑a₂ : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y

Tactic:
exact (H.apply_one _).trans (congr_arg a₂ (eq_const_of_unique y).symm)

Premises used: ContinuousMap.HomotopyWith.apply_one, congr_arg, Eq.symm, DFunLike.coe, Eq.trans, eq_const_of_unique
-- 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₁ 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
⊢ y default = 0 ∨ y default = 1

Tactic:
cases Unique.eq_default i

Premises used: Unique.eq_default
-- 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₁ 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)
iH : y default = 0 ∨ y default = 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)

Tactic:
(H.eq_fst _ iH).trans (congr_arg a₁ (eq_const_of_unique y).symm)

Premises used: congr_arg, ContinuousMap.HomotopyRel.eq_fst, Eq.symm, DFunLike.coe, Eq.trans, eq_const_of_unique
-- 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₁ 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)
iH : y default = 0 ∨ y default = 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)

Tactic:
exact (H.eq_fst _ iH).trans (congr_arg a₁ (eq_const_of_unique y).symm)

Premises used: congr_arg, ContinuousMap.HomotopyRel.eq_fst, Eq.symm, DFunLike.coe, Eq.trans, eq_const_of_unique
-- 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))
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)
⊢ 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)

Tactic:
ext t
-- 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)
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 := ⋯,
                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)
⊢ 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:
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]

Premises used: Path.trans, GenLoop.mk_apply, genLoopEquivOfUnique, GenLoop.transAt, GenLoop.copy, ContinuousMap.coe_mk, one_div, Equiv.coe_fn_mk, Function.comp_apply, Path.coe_mk'
-- 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)
⊢ 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)

Tactic:
ite_congr rfl (fun _ ↦ congrArg q ?_)
    fun _ ↦ congrArg p ?_

Premises used: congrArg, ite_congr, DFunLike.coe, rfl
-- 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)
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 : ℝ))
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)
⊢ 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)

Tactic:
refine ite_congr rfl (fun _ ↦ congrArg q ?_)
    fun _ ↦ congrArg p ?_

Premises used: congrArg, ite_congr, DFunLike.coe, rfl
-- 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⁻¹
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 : ℝ))) : ℝ)
⊢ 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:
ext i
-- 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 : ℝ))) default) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))) : ℝ)
⊢ (↑(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:
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 : ℝ))) default) :
      ℝ) =
    (↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑t : ℝ))) : ℝ)

Tactic:
simp
-- 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⁻¹
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)) : ℝ)
⊢ 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:
ext i