awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith : 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2 / 2 = 1
linarith₅ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₆ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2 / 2 = 1
linarith₅ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : GT.gt (α := ℝ) 2 0
linarith₇ : 2 / 2 = 1
linarith₈ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 2 / 2 = 1
linarith₁₀ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₂ : GT.gt (α := ℝ) 2 0
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₁₃ : 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2 / 2 = 1
linarith₅ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : GT.gt (α := ℝ) 2 0
linarith₇ : 2 / 2 = 1
linarith₈ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 2 / 2 = 1
linarith₁₀ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₂ : GT.gt (α := ℝ) 2 0
linarith₁₃ : 4 / 4 = 1
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₁₄ : HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2 / 2 = 1
linarith₅ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : GT.gt (α := ℝ) 2 0
linarith₇ : 2 / 2 = 1
linarith₈ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 2 / 2 = 1
linarith₁₀ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₂ : GT.gt (α := ℝ) 2 0
linarith₁₃ : 4 / 4 = 1
linarith₁₄ : HMul.hMul (α := ℝ) 1 4 = 4
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₁₅ : GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2 / 2 = 1
linarith₅ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : GT.gt (α := ℝ) 2 0
linarith₇ : 2 / 2 = 1
linarith₈ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 2 / 2 = 1
linarith₁₀ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₂ : GT.gt (α := ℝ) 2 0
linarith₁₃ : 4 / 4 = 1
linarith₁₄ : HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₅ : GT.gt (α := ℝ) 4 0
linarith₁₆ : 2 / 2 = 1
linarith₁₇ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₈ : GT.gt (α := ℝ) 2 0
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)
have linarith₁₉ : HMul.hMul (α := ℝ) 1 1 - 2 * (↑x : ℝ) +
    (HMul.hMul (α := ℝ) 1 2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (↑x : ℝ) + HMul.hMul (α := ℝ) 1 1)) -
        HMul.hMul (α := ℝ) 2 1 -
      HMul.hMul (α := ℝ) 1 1) =
  0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ trans (refl x₀) γ = γ
have mk : ∀ (γ : Path x₀ x₁), trans (refl x₀) (mk γ) = mk γ
Tactic: induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.refl_trans γ
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ γ.trans (refl x₁) = γ
have mk : ∀ (γ : Path x₀ x₁), (mk γ).trans (refl x₁) = mk γ
Tactic: induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.trans_refl γ
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ γ.trans γ.symm = refl x₀
have mk : ∀ (γ : Path x₀ x₁), (mk γ).trans (mk γ).symm = refl x₀
Tactic: induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.trans_symm γ
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
⊢ γ.symm.trans γ = refl x₁
have mk : ∀ (γ : Path x₀ x₁), (mk γ).symm.trans (mk γ) = refl x₁
Tactic: induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.symm_trans γ
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
γ₁ : Path x₁ x₂
⊢ ((mk γ₀).trans (mk γ₁)).trans γ₂ = (mk γ₀).trans ((mk γ₁).trans γ₂)
have mk : ∀ (γ₂ : Path x₂ x₃), ((mk γ₀).trans (mk γ₁)).trans (mk γ₂) = (mk γ₀).trans ((mk γ₁).trans (mk γ₂))
Tactic: induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂
Cleared hypotheses: γ₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
⊢ ((mk γ₀).trans γ₁).trans γ₂ = (mk γ₀).trans (γ₁.trans γ₂)
have mk : ∀ (γ₁ : Path x₁ x₂), ((mk γ₀).trans (mk γ₁)).trans γ₂ = (mk γ₀).trans ((mk γ₁).trans γ₂)
Tactic: induction γ₁ using Quotient.ind with | mk γ₁ =>
  induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂
Cleared hypotheses: γ₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₀ : Homotopic.Quotient x₀ x₁
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
⊢ (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)
have mk : ∀ (γ₀ : Path x₀ x₁), ((mk γ₀).trans γ₁).trans γ₂ = (mk γ₀).trans (γ₁.trans γ₂)
Tactic: induction γ₀ using Quotient.ind with | mk γ₀ =>
  induction γ₁ using Quotient.ind with | mk γ₁ =>
  induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂
Cleared hypotheses: γ₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α := FundamentalGroupoid X ⥤ FundamentalGroupoid X)
    { obj := fun (x : FundamentalGroupoid X) ↦ { as := (ContinuousMap.id X : (a : X) → X) x.as },
      map := fun {X_1 Y : FundamentalGroupoid X} (p : X_1 ⟶ Y) ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X),
      map_id := ⋯, map_comp := ⋯ }
    (𝟭 (FundamentalGroupoid X))
have e_map : Eq.{u_1 + 1} (α :=
  {X_1 Y : FundamentalGroupoid X} →
    (X_1 ⟶ Y) →
      Quiver.Hom (V := FundamentalGroupoid X)
        ({ as := (ContinuousMap.id X : (a : X) → X) X_1.as } : FundamentalGroupoid X)
        ({ as := (ContinuousMap.id X : (a : X) → X) Y.as } : FundamentalGroupoid X))
  (fun {X_1 Y : FundamentalGroupoid X} (p : X_1 ⟶ Y) ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X))
  fun {X_1 Y : FundamentalGroupoid X} (f : X_1 ⟶ Y) ↦ f
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α :=
    {X_1 Y : FundamentalGroupoid X} →
      (X_1 ⟶ Y) →
        Quiver.Hom (V := FundamentalGroupoid X)
          ({ as := (ContinuousMap.id X : (a : X) → X) X_1.as } : FundamentalGroupoid X)
          ({ as := (ContinuousMap.id X : (a : X) → X) Y.as } : FundamentalGroupoid X))
    (fun {X_1 Y : FundamentalGroupoid X} (p : X_1 ⟶ Y) ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X))
    fun {X_1 Y : FundamentalGroupoid X} (f : X_1 ⟶ Y) ↦ f
have e_map : ∀ (x y : FundamentalGroupoid X) (x_1 : x ⟶ y) (p : Path x.as y.as),
  Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p)
      (ContinuousMap.id X) =
    Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p
Tactic: ext x y ⟨p⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
Z : Type u_3
inst_2 : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ Eq (α := CategoryTheory.Functor.{u_1, u_3, u_1, u_3} (FundamentalGroupoid X) (FundamentalGroupoid Z))
    { obj := fun (x : FundamentalGroupoid X) ↦ { as := (g.comp f : (a : X) → Z) x.as },
      map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p (g.comp f),
      map_id := ⋯, map_comp := ⋯ }
    (Functor.comp.{u_1, u_2, u_3, u_1, u_2, u_3} (D := FundamentalGroupoid Y)
      { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
        map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_1 : FundamentalGroupoid Y} (p : X ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ })
have e_map : Eq (α :=
  {X_1 Y_1 : FundamentalGroupoid X} →
    (X_1 ⟶ Y_1) →
      Quiver.Hom (V := FundamentalGroupoid Z) ({ as := (g.comp f : (a : X) → Z) X_1.as } : FundamentalGroupoid Z)
        ({ as := (g.comp f : (a : X) → Z) Y_1.as } : FundamentalGroupoid Z))
  (fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p (g.comp f))
  fun {X_1 Y_1 : FundamentalGroupoid X} (f_1 : X_1 ⟶ Y_1) ↦
  CategoryTheory.Functor.map
    { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
      map := fun {X Y_2 : FundamentalGroupoid Y} (p : X ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p g, map_id := sorry,
      map_comp := sorry }
    (CategoryTheory.Functor.map
      { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
        map := fun {X_2 Y_2 : FundamentalGroupoid X} (p : X_2 ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p f, map_id := sorry,
        map_comp := sorry }
      f_1)
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
Z : Type u_3
inst_2 : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ Eq (α :=
    {X_1 Y_1 : FundamentalGroupoid X} →
      (X_1 ⟶ Y_1) →
        Quiver.Hom (V := FundamentalGroupoid Z) ({ as := (g.comp f : (a : X) → Z) X_1.as } : FundamentalGroupoid Z)
          ({ as := (g.comp f : (a : X) → Z) Y_1.as } : FundamentalGroupoid Z))
    (fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p (g.comp f))
    fun {X_1 Y_1 : FundamentalGroupoid X} (f_1 : X_1 ⟶ Y_1) ↦
    CategoryTheory.Functor.map
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_2 : FundamentalGroupoid Y} (p : X ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }
      (CategoryTheory.Functor.map
        { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
          map := fun {X_2 Y_2 : FundamentalGroupoid X} (p : X_2 ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
          map_comp := ⋯ }
        f_1)
have e_map : ∀ (x y : FundamentalGroupoid X) (x_1 : x ⟶ y) (p : Path x.as y.as),
  Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p)
      (g.comp f) =
    CategoryTheory.Functor.map
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_1 : FundamentalGroupoid Y} (p : X ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p g, map_id := sorry,
        map_comp := sorry }
      (CategoryTheory.Functor.map
        { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
          map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p f, map_id := sorry,
          map_comp := sorry }
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p))
Tactic: ext x y ⟨p⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
h : x₀ = x₁
⊢ Eq (α := { as := x₀ : FundamentalGroupoid X } ⟶ { as := x₁ }) (eqToHom ⋯) ⟦Path.cast (Path.refl x₁) h ⋯⟧
have subst : Eq (α := { as := x₀ : FundamentalGroupoid X } ⟶ { as := x₀ }) (eqToHom sorry) ⟦Path.cast (Path.refl x₀) sorry sorry⟧
Tactic: subst h
Cleared hypotheses: x₁, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y x' y' : X
p : Path x y
hx : x' = x
hy : y' = y
⊢ eqToHom ⋯ ≫ Path.Homotopic.Quotient.mk p ≫ eqToHom ⋯ = Path.Homotopic.Quotient.mk (p.cast hx hy)
have subst : ∀ {p : Path x' y'}, eqToHom sorry ≫ Path.Homotopic.Quotient.mk p ≫ eqToHom sorry = Path.Homotopic.Quotient.mk (p.cast sorry sorry)
Tactic: subst hx hy
Cleared hypotheses: x, y, p, hx, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ (Path.trans (p.map ⋯) (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
have H0 : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x₁ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (0, 0) : Y)
Tactic: refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
H0 : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x₁ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (0, 0) : Y)
⊢ (Path.trans (p.map ⋯) (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
have H1 : Eq.{u_2 + 1} (α := Y) ((g : (a : X) → Y) x₂ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (1, 1) : Y)
Tactic: refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
H0 : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x₁ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (0, 0) : Y)
H1 : Eq.{u_2 + 1} (α := Y) ((g : (a : X) → Y) x₂ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (1, 1) : Y)
⊢ (Path.trans (p.map ⋯) (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
have hp : (p₁.map sorry).cast sorry sorry = Path.trans (p.map sorry) (F.evalAt x₂)
Tactic: refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
H0 : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x₁ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (0, 0) : Y)
H1 : Eq.{u_2 + 1} (α := Y) ((g : (a : X) → Y) x₂ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (1, 1) : Y)
hp : (p₁.map ⋯).cast ⋯ ⋯ = Path.trans (p.map ⋯) (F.evalAt x₂)
⊢ (Path.trans (p.map ⋯) (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
have hq : (p₂.map sorry).cast sorry sorry = (F.evalAt x₁).trans (p.map sorry)
Tactic: refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : { as := x : FundamentalGroupoid X } ⟶ { as := y }
⊢ (map f).map p ≫ ⟦H.evalAt { as := y : FundamentalGroupoid X }.as⟧ = ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map p
have rcases : ∀ (p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as),
  (map f).map (Path.Homotopic.Quotient.mk p) ≫ ⟦H.evalAt { as := y : FundamentalGroupoid X }.as⟧ =
    ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map (Path.Homotopic.Quotient.mk p)
Tactic: rcases Path.Homotopic.Quotient.mk_surjective p with ⟨p, rfl⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as
⊢ (map f).map (Path.Homotopic.Quotient.mk p) ≫ ⟦H.evalAt { as := y : FundamentalGroupoid X }.as⟧ =
    ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map (Path.Homotopic.Quotient.mk p)
have simp : Path.Homotopic.Quotient.mk
    ((p.map (sorry : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y))).trans (H.evalAt y)) =
  Path.Homotopic.Quotient.mk
    ((H.evalAt x).trans (p.map (sorry : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑g : (a : X) → Y))))
Tactic: simp only [map_map, map_obj_as, Path.Homotopic.Quotient.mk''_eq_mk, comp_eq,
      ← Path.Homotopic.Quotient.mk_map, ← Path.Homotopic.Quotient.mk_trans]