awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : (↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
exact h.symm

Premises used: Ne.symm
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
neg :
  Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))
⊢ Eq.{u_2 + 1} (α := X)
    ((d : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
          j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) :
      X)
    ((d : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
          i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) :
      X)

Tactic:
congr 1
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
neg :
  ∀ (x : N),
    Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
        j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) x =
      Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
        i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)) x
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))

Tactic:
ext1
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
neg :
  (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1) else y x_1
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) x_1 =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)) x_1

Tactic:
simp only [Function.update, eq_rec_constant, dite_eq_ite]

Premises used: Function.update, eq_rec_constant, dite_eq_ite
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
neg : x_1 = j → ¬x_1 = i
⊢ (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1) else y x_1

Tactic:
apply ite_ite_comm

Premises used: ite_ite_comm
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : ¬(↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
h.symm

Premises used: Ne.symm
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : ¬(↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
exact h.symm

Premises used: Ne.symm
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ fromLoop i (Path.trans (toLoop i p) (toLoop i q)) = transAt i p q

Tactic:
(copy_eq _ _).symm

Premises used: GenLoop.transAt, Eq.symm, GenLoop.copy_eq
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ fromLoop i (Path.symm (toLoop i p)) = symmAt i p

Tactic:
(copy_eq _ _).symm

Premises used: GenLoop.symmAt, Eq.symm, GenLoop.copy_eq
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty N
f : (↑(Ω^ N X x) : Type (max u_2 u_3))
H :
  ∀ (y : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      (((fun (y : X) ↦
                (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
                    Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                    (ContinuousMap.const (N → (↑I : Type)) y) ⋯ :
                  { x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X //
                    Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
              ((fun (f : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦ ((f : (a : N → (↑I : Type)) → X) 0 : X)) f) :
            (a : N → (↑I : Type)) → X)
          y :
        X)
      ((f : (a : N → (↑I : Type)) → X) y : X)
⊢ (fun (y : X) ↦
        (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
            Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
            (ContinuousMap.const (N → (↑I : Type)) y) ⋯ :
          { x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X //
            Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
      ((fun (f : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦ ((f : (a : N → (↑I : Type)) → X) 0 : X)) f) =
    f

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty N
f : (↑(Ω^ N X x) : Type (max u_2 u_3))
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    (((fun (y : X) ↦
              (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                  (ContinuousMap.const (N → (↑I : Type)) y) ⋯ :
                { x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X //
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
            ((fun (f : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦ ((f : (a : N → (↑I : Type)) → X) 0 : X)) f) :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    ((f : (a : N → (↑I : Type)) → X) y : X)

Tactic:
congr_arg f (Subsingleton.elim _ _)

Premises used: congr_arg, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty N
f : (↑(Ω^ N X x) : Type (max u_2 u_3))
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    (((fun (y : X) ↦
              (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                  (ContinuousMap.const (N → (↑I : Type)) y) ⋯ :
                { x_2 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X //
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
            ((fun (f : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦ ((f : (a : N → (↑I : Type)) → X) 0 : X)) f) :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    ((f : (a : N → (↑I : Type)) → X) y : X)

Tactic:
exact congr_arg f (Subsingleton.elim _ _)

Premises used: congr_arg, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty N
a₁ a₂ : (↑(Ω^ N X x) : Type (max u_2 u_3))
mp :
  (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₂ →
    (pathSetoid X : X → X → Prop)
      ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₁ : X)
      ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₂ : X)
mpr :
  (pathSetoid X : X → X → Prop)
      ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₁ : X)
      ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₂ : 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₂
⊢ (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₂ ↔
    (pathSetoid X : X → X → Prop)
      ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₁ : X)
      ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₂ : X)

Tactic:
constructor
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty 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)
⊢ (pathSetoid X : X → X → Prop)
    ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₁ : X)
    ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₂ : X)

Tactic:
⟨{ toFun := fun t ↦ H ⟨t, isEmptyElim⟩
            source' := (H.apply_zero _).trans (congr_arg a₁ <| Subsingleton.elim _ _)
            target' := (H.apply_one _).trans (congr_arg a₂ <| Subsingleton.elim _ _) }⟩

Premises used: isEmptyElim, ContinuousMap.HomotopyWith.apply_one, ContinuousMap.mk, Prod.mk, Nonempty.intro, congr_arg, Path.mk, ContinuousMap.HomotopyWith.apply_zero, Subsingleton.elim, OfNat.ofNat, Joined, DFunLike.coe, Eq.trans
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty N
a₁ a₂ : (↑(Ω^ N X x) : Type (max u_2 u_3))
H :
  Path (X := X) ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₁ : X)
    ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₂ : 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:
⟨{  toFun := fun t0 ↦ H t0.fst
            map_zero_left := fun _ ↦ H.source.trans (congr_arg a₁ <| Subsingleton.elim _ _)
            map_one_left := fun _ ↦ H.target.trans (congr_arg a₂ <| Subsingleton.elim _ _)
            prop' := fun _ _ ⟨i, _⟩ ↦ isEmptyElim i }⟩

Premises used: GenLoop.Homotopic, isEmptyElim, ContinuousMap.mk, Continuous.comp, ContinuousMap.HomotopicRel, ContinuousMap.HomotopyWith.mk, Prod.mk, GenLoop.congr.match_1, Nonempty.intro, Prod.fst, congr_arg, Path.source, ContinuousMap.HomotopyWith._proof_1, Path.target, Subsingleton.elim, OfNat.ofNat, Subtype.val, ContinuousMap.Homotopy.mk, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N_1 : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
inst_1 : DecidableEq N_1
N : Type u_3
x : X
inst_2 : IsEmpty 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)
⊢ (pathSetoid X : X → X → Prop)
    ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₁ : X)
    ((toEquiv (genLoopHomeoOfIsEmpty N x) : (a : (↑(Ω^ N X x) : Type (max u_2 u_3))) → X) a₂ : X)

Tactic:
exacts
        [⟨{ toFun := fun t ↦ H ⟨t, isEmptyElim⟩
            source' := (H.apply_zero _).trans (congr_arg a₁ <| Subsingleton.elim _ _)
            target' := (H.apply_one _).trans (congr_arg a₂ <| Subsingleton.elim _ _) }⟩,
        ⟨{  toFun := fun t0 ↦ H t0.fst
            map_zero_left := fun _ ↦ H.source.trans (congr_arg a₁ <| Subsingleton.elim _ _)
            map_one_left := fun _ ↦ H.target.trans (congr_arg a₂ <| Subsingleton.elim _ _)
            prop' := fun _ _ ⟨i, _⟩ ↦ isEmptyElim i }⟩]
-- 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
p : (↑(Ω^ N X x) : Type (max u_2 u_3))
⊢ Continuous[_, inst] fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t

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
p : Ω X x
⊢ Continuous[_, inst] fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c 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
p : Ω X x
y : N → (↑I : Type)
i : N
iH : y i = 0
⊢ y default = 0

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
p : Ω X x
y : N → (↑I : Type)
i : N
iH : y i = 1
⊢ 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
p : Ω X x
y : N → (↑I : Type)
iH : y default = 0
inl : (p : (a : (↑I : Type)) → X) 0 = x
⊢ ({ toFun := fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c default), continuous_toFun := ⋯ :
          ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X } :
        (a : N → (↑I : Type)) → X)
      y =
    x

Tactic:
apply (congr_arg p iH).trans

Premises used: congr_arg, DFunLike.coe, Eq.trans
-- 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
p : Ω X x
y : N → (↑I : Type)
iH : y default = 1
inr : (p : (a : (↑I : Type)) → X) 1 = x
⊢ ({ toFun := fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c default), continuous_toFun := ⋯ :
          ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X } :
        (a : N → (↑I : Type)) → X)
      y =
    x

Tactic:
apply (congr_arg p iH).trans

Premises used: congr_arg, DFunLike.coe, Eq.trans
-- 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
p : Ω X x
y : N → (↑I : Type)
iH : y default = 0
⊢ (p : (a : (↑I : Type)) → X) 0 = x

Tactic:
p.source

Premises used: Path.source
-- 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
p : Ω X x
y : N → (↑I : Type)
iH : y default = 1
⊢ (p : (a : (↑I : Type)) → X) 1 = x

Tactic:
p.target

Premises used: Path.target
-- 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
p : Ω X x
y : N → (↑I : Type)
iH : y default = 0
⊢ (p : (a : (↑I : Type)) → X) 0 = x

Tactic:
exacts [p.source, p.target]

Premises used: Path.source, Path.target
-- 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
p : (↑(Ω^ N X x) : Type (max u_2 u_3))
H :
  ∀ (y : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      (((fun (p : Ω X x) ↦
                Subtype.mk (p := fun (x_1 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_1)
                  { toFun := fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c default),
                    continuous_toFun := ⋯ }
                  ⋯)
              ((fun (p : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦
                  { toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t,
                    continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path x x })
                p) :
            (a : N → (↑I : Type)) → X)
          y :
        X)
      ((p : (a : N → (↑I : Type)) → X) y : X)
⊢ (fun (p : Ω X x) ↦
        Subtype.mk (p := fun (x_1 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
          Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_1)
          { toFun := fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c default), continuous_toFun := ⋯ } ⋯)
      ((fun (p : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦
          { toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t, continuous_toFun := ⋯,
            source' := ⋯, target' := ⋯ : Path x x })
        p) =
    p

Tactic:
ext 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
p : (↑(Ω^ N X x) : Type (max u_2 u_3))
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    (((fun (p : Ω X x) ↦
              Subtype.mk (p := fun (x_1 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
                Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_1)
                { toFun := fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c default), continuous_toFun := ⋯ }
                ⋯)
            ((fun (p : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦
                { toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t,
                  continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path x x })
              p) :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    ((p : (a : N → (↑I : Type)) → X) y : X)

Tactic:
congr_arg p (eq_const_of_unique y).symm

Premises used: congr_arg, Eq.symm, DFunLike.coe, 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
p : (↑(Ω^ N X x) : Type (max u_2 u_3))
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    (((fun (p : Ω X x) ↦
              Subtype.mk (p := fun (x_1 : ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X) ↦
                Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_1)
                { toFun := fun (c : N → (↑I : Type)) ↦ (p : (a : (↑I : Type)) → X) (c default), continuous_toFun := ⋯ }
                ⋯)
            ((fun (p : (↑(Ω^ N X x) : Type (max u_2 u_3))) ↦
                { toFun := fun (t : (↑I : Type)) ↦ (p : (a : N → (↑I : Type)) → X) fun (x : N) ↦ t,
                  continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path x x })
              p) :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    ((p : (a : N → (↑I : Type)) → X) y : X)

Tactic:
exact congr_arg p (eq_const_of_unique y).symm

Premises used: congr_arg, Eq.symm, DFunLike.coe, 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))
mp :
  (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₂ →
    (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)
mpr :
  (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) →
    (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₂
⊢ (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₂ ↔
    (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:
constructor