awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) ⋯ ≫ σ j'
have succ : σ j ≫ σ₀Iter i sorry ≫ σ 0 = σ₀Iter (i + 1) sorry ≫ σ j'
Tactic: rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter (i + 1) ⋯ ≫ σ j'
⊢ σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) ⋯ ≫ σ j'
have succ₁ : σ j ≫ σ₀Iter i sorry ≫ σ 0 = σ₀Iter i sorry ≫ σ 0 ≫ σ j'
Tactic: rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter (i + 1) ⋯ ≫ σ j'
succ₁ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
⊢ σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) ⋯ ≫ σ j'
have succ₂ : σ₀Iter i sorry ≫ σ j'.succ ≫ σ 0 = σ₀Iter i sorry ≫ σ 0 ≫ σ j'
Tactic: rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter (i + 1) ⋯ ≫ σ j'
succ₁ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
succ₂ : σ₀Iter i ⋯ ≫ σ j'.succ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
⊢ σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) ⋯ ≫ σ j'
have succ₃ : σ₀Iter i sorry ≫ σ (Fin.castSucc 0) ≫ σ j' = σ₀Iter i sorry ≫ σ 0 ≫ σ j'
Tactic: rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter (i + 1) ⋯ ≫ σ j'
succ₁ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
succ₂ : σ₀Iter i ⋯ ≫ σ j'.succ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
succ₃ : σ₀Iter i ⋯ ≫ σ (Fin.castSucc 0) ≫ σ j' = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
⊢ σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) ⋯ ≫ σ j'
have succ₄ : σ₀Iter i sorry ≫ σ 0 ≫ σ j' = σ₀Iter i sorry ≫ σ 0 ≫ σ j'
Tactic: rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + i = m
hj : (↑j : ℕ) = (↑j' : ℕ) + i
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
have zero : ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + 0 = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + 0),
  σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 sorry ≫ σ j'
Tactic: induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : j = j' := by lia
    simp
  | succ i hi' =>
    rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
Cleared hypotheses: i, n, m, j, j', hi, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + i = m
hj : (↑j : ℕ) = (↑j' : ℕ) + i
zero :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + 0 = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + 0),
    σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
have succ : ∀ (i : ℕ)
  (hi' :
    ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
      σ j ≫ σ₀Iter i hi = σ₀Iter i sorry ≫ σ j')
  {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + (i + 1) = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
  σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) sorry ≫ σ j'
Tactic: induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : j = j' := by lia
    simp
  | succ i hi' =>
    rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]
Cleared hypotheses: i, n, m, j, j', hi, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n m : ℕ
hi : n + 0 = m
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
have zero : ∀ (hi : n + 0 = n), δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
Tactic: obtain rfl : n = m := by lia
Cleared hypotheses: m, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n m : ℕ
hi : n + (i + 1) = m
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
have succ : ∀ (hi : n + (i + 1) = n + i + 1), δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
Tactic: obtain rfl : m = (n + i) + 1 := by lia
Cleared hypotheses: m, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
have succ : δ₀Iter i sorry ≫ δ 0 ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
Tactic: rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
succ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
have succ₁ : δ₀Iter i sorry ≫ δ 0 ≫ σ 0 ≫ σ₀Iter i sorry = 𝟙 ⦋n⦌
Tactic: rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
succ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
succ₁ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ 0 ≫ σ₀Iter i ⋯ = 𝟙 ⦋n⦌
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
have succ₂ : δ₀Iter i sorry ≫ σ₀Iter i sorry = 𝟙 ⦋n⦌
Tactic: rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
succ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
succ₁ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ 0 ≫ σ₀Iter i ⋯ = 𝟙 ⦋n⦌
succ₂ : δ₀Iter i ⋯ ≫ σ₀Iter i ⋯ = 𝟙 ⦋n⦌
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
have succ₃ : 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
Tactic: rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
hi : n + i = m
⊢ δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
have zero : ∀ {n m : ℕ} (hi : n + 0 = m), δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
Tactic: induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    simp
  | succ i hi' =>
    obtain rfl : m = (n + i) + 1 := by lia
    rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']
Cleared hypotheses: i, n, m, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
hi : n + i = m
zero : ∀ {n m : ℕ} (hi : n + 0 = m), δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
⊢ δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
have succ : ∀ (i : ℕ) (hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌) {n m : ℕ} (hi : n + (i + 1) = m),
  δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
Tactic: induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    simp
  | succ i hi' =>
    obtain rfl : m = (n + i) + 1 := by lia
    rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']
Cleared hypotheses: i, n, m, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x : SimplexCategoryGenRel
⊢ ℕ
have rcases : (n : Paths FreeSimplexQuiver) → ℕ
Tactic: rcases x with ⟨n⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
⊢ generators.multiplicativeClosure = ⊤
have apply : ⊤ ≤ generators.multiplicativeClosure
Tactic: apply le_antisymm (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
⊢ generators.multiplicativeClosure f
have h : ∀ {x y : Paths FreeSimplexQuiver} (f : x ⟶ y),
  generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)
Tactic: induction f using CategoryTheory.Quotient.induction with | _ f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
u v w : FreeSimplexQuiver
p : Prefunctor.obj (Paths.of FreeSimplexQuiver) u ⟶ Prefunctor.obj (Paths.of FreeSimplexQuiver) v
k : v ⟶ w
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) k))
have h₁ : ∀ {n : ℕ} (i : Fin (n + 2))
  (p :
    Prefunctor.obj (Paths.of FreeSimplexQuiver) u ⟶
      Prefunctor.obj (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.mk n))
  (h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p)),
  generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))
Tactic: cases k
Cleared hypotheses: v, w, p, k, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
u v w : FreeSimplexQuiver
p : Prefunctor.obj (Paths.of FreeSimplexQuiver) u ⟶ Prefunctor.obj (Paths.of FreeSimplexQuiver) v
k : v ⟶ w
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p)
h₁ :
  ∀ {n : ℕ} (i : Fin (n + 2))
    (p :
      Prefunctor.obj (Paths.of FreeSimplexQuiver) u ⟶
        Prefunctor.obj (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.mk n))
    (h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p)),
    generators.multiplicativeClosure
      ((Quotient.functor FreeSimplexQuiver.homRel).map
        (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) k))
have h₂ : ∀ {n : ℕ} (i : Fin (n + 1))
  (p :
    Prefunctor.obj (Paths.of FreeSimplexQuiver) u ⟶
      Prefunctor.obj (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.mk (n + 1)))
  (h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p)),
  generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
Tactic: cases k
Cleared hypotheses: v, w, p, k, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
f : x_1 ⟶ y_1
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)
have h : ∀ {v : FreeSimplexQuiver},
  generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 (Prefunctor.obj (Paths.of FreeSimplexQuiver) v)))
Tactic: induction f using Paths.induction with
  | id => exact generators.multiplicativeClosure.id_mem _
  | comp _ k h =>
    cases k
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
f : x_1 ⟶ y_1
h :
  ∀ {v : FreeSimplexQuiver},
    generators.multiplicativeClosure
      ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 (Prefunctor.obj (Paths.of FreeSimplexQuiver) v)))
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)
have h₁ : ∀ {u v w : FreeSimplexQuiver}
  (p : Prefunctor.obj (Paths.of FreeSimplexQuiver) u ⟶ Prefunctor.obj (Paths.of FreeSimplexQuiver) v) (k : v ⟶ w)
  (h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p)),
  generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) k))
Tactic: induction f using Paths.induction with
  | id => exact generators.multiplicativeClosure.id_mem _
  | comp _ k h =>
    cases k
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (hypothesis)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure ≤ P
⊢ P f
have this₁ : P = ⊤
Tactic: rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f
have rw : ⊤ f
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ P f
have suffices : generators.multiplicativeClosure ≤ P
Tactic: suffices generators.multiplicativeClosure ≤ P by
    rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f_2 : X ⟶ Y
x y : SimplexCategoryGenRel
f : x ⟶ y
h : generators f
⊢ P f
have of : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 2)), P (δ i)
Tactic: rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
Cleared hypotheses: x, y, f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f_2 : X ⟶ Y
x y : SimplexCategoryGenRel
f : x ⟶ y
h : generators f
of : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 2)), P (δ i)
⊢ P f
have of₁ : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 1)), P (σ i)
Tactic: rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
Cleared hypotheses: x, y, f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f_2 : X ⟶ Y
x y z : SimplexCategoryGenRel
f : x ⟶ y
g : y ⟶ z
hf : generators.multiplicativeClosure f
hg : generators g
hrec : P f
⊢ P (f ≫ g)
have comp_of : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 2)) (f : x ⟶ mk n) (hf : generators.multiplicativeClosure f)
  (hrec : P f), P (f ≫ δ i)
Tactic: rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
Cleared hypotheses: y, z, f, g, hf, hg, hrec
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f_2 : X ⟶ Y
x y z : SimplexCategoryGenRel
f : x ⟶ y
g : y ⟶ z
hf : generators.multiplicativeClosure f
hg : generators g
hrec : P f
comp_of :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 2)) (f : x ⟶ mk n) (hf : generators.multiplicativeClosure f)
    (hrec : P f), P (f ≫ δ i)
⊢ P (f ≫ g)
have comp_of₁ : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 1)) (f : x ⟶ mk (n + 1)) (hf : generators.multiplicativeClosure f)
  (hrec : P f), P (f ≫ σ i)
Tactic: rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
Cleared hypotheses: y, z, f, g, hf, hg, hrec
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f : X ⟶ Y
hf : generators.multiplicativeClosure f
⊢ P f
have of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (h : generators f), P f
Tactic: induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (comp_δ (𝟙 _) i id)
    · simpa using (comp_σ (𝟙 _) i id)
  | id n => exact id
  | comp_of f g hf hg hrec =>
    rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (comp_δ f i hrec)
    · simpa using (comp_σ f i hrec)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f : X ⟶ Y
hf : generators.multiplicativeClosure f
of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (h : generators f), P f
⊢ P f
have id₁ : ∀ (n : SimplexCategoryGenRel), P (𝟙 n)
Tactic: induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (comp_δ (𝟙 _) i id)
    · simpa using (comp_σ (𝟙 _) i id)
  | id n => exact id
  | comp_of f g hf hg hrec =>
    rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (comp_δ f i hrec)
    · simpa using (comp_σ f i hrec)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f : X ⟶ Y
hf : generators.multiplicativeClosure f
of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (h : generators f), P f
id₁ : ∀ (n : SimplexCategoryGenRel), P (𝟙 n)
⊢ P f
have comp_of : ∀ {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z) (hf : generators.multiplicativeClosure f) (hg : generators g)
  (hrec : P f), P (f ≫ g)
Tactic: induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (comp_δ (𝟙 _) i id)
    · simpa using (comp_σ (𝟙 _) i id)
  | id n => exact id
  | comp_of f g hf hg hrec =>
    rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (comp_δ f i hrec)
    · simpa using (comp_σ f i hrec)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (hypothesis)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure' ≤ P
⊢ P f
have this₁ : P = ⊤
Tactic: rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
      multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f
have rw : ⊤ f
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ P f
have suffices : generators.multiplicativeClosure' ≤ P
Tactic: suffices generators.multiplicativeClosure' ≤ P by
    rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
      multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply