awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
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'
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 ⋯ ≫ σ 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'
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ 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]

Premises used: SimplexCategory.σ₀Iter_succ, Fin.castSucc_zero, SimplexCategory.σ₀Iter_succ_assoc, SimplexCategory.σ_comp_σ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
hi : n + 0 = m
⊢ n = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
hi : n + 0 = m
zero : ∀ (hi : n + 0 = n), δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌

Tactic:
obtain rfl : n = m := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
hi : n + 0 = n
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n m : ℕ
hi : n + (i + 1) = m
⊢ m = n + i + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n m : ℕ
hi : n + (i + 1) = m
succ : ∀ (hi : n + (i + 1) = n + i + 1), δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌

Tactic:
obtain rfl : m = (n + i) + 1 := by lia

Premises used: HAdd.hAdd, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
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⦌
succ₃ succ₄ : 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌

Tactic:
rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']

Premises used: SimplexCategory.δ₀Iter_succ_assoc, SimplexCategory.σ₀Iter_succ', SimplexCategory.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
zero : ∀ {n m : ℕ} (hi : n + 0 = m), δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
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⦌
⊢ δ₀Iter i hi ≫ σ₀Iter i 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']

Premises used: SimplexCategory.δ₀Iter_succ_assoc, SimplexCategory.σ₀Iter_succ', HAdd.hAdd, SimplexCategory.δ_comp_σ_self, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
⊢ Mono (δ₀Iter i hi)

Tactic:
mono_of_mono_fac (δ₀Iter_σ₀Iter i hi)

Premises used: SimplexCategory.δ₀Iter_σ₀Iter, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
⊢ Epi (σ₀Iter i hi)

Tactic:
epi_of_epi_fac (δ₀Iter_σ₀Iter i hi)

Premises used: CategoryTheory.epi_of_epi_fac, SimplexCategory.δ₀Iter_σ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x : SimplexCategoryGenRel
rcases : (n : Paths FreeSimplexQuiver) → ℕ
⊢ ℕ

Tactic:
rcases x with ⟨n⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : Paths FreeSimplexQuiver
⊢ ℕ

Tactic:
exact n
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
⊢ (mk n).len = n

Tactic:
rfl

Premises used: SimplexCategoryGenRel.len, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
⊢ generators (SimplexCategoryGenRel.δ i)

Tactic:
le_sup_left (a := faces) _ (.δ i)

Premises used: le_sup_left, SimplexCategoryGenRel.faces.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ generators (SimplexCategoryGenRel.σ i)

Tactic:
le_sup_right (a := faces) _ (.σ i)

Premises used: le_sup_right, SimplexCategoryGenRel.degeneracies.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
⊢ generators.multiplicativeClosure ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
apply : ⊤ ≤ generators.multiplicativeClosure
⊢ generators.multiplicativeClosure = ⊤

Tactic:
apply le_antisymm (by simp)

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
h :
  ∀ {x y : Paths FreeSimplexQuiver} (f : x ⟶ y),
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)
⊢ generators.multiplicativeClosure f

Tactic:
induction f using CategoryTheory.Quotient.induction with | _ f

Premises used: CategoryTheory.Quotient.induction
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
v : FreeSimplexQuiver
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 (Prefunctor.obj (Paths.of FreeSimplexQuiver) v)))

Tactic:
generators.multiplicativeClosure.id_mem _

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
v : FreeSimplexQuiver
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 (Prefunctor.obj (Paths.of FreeSimplexQuiver) v)))

Tactic:
exact generators.multiplicativeClosure.id_mem _

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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)))
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)))
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p ≫ Prefunctor.map (Paths.of FreeSimplexQuiver) k))

Tactic:
cases k
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
u : FreeSimplexQuiver
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:
generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, SimplexCategoryGenRel.mk, FreeSimplexQuiver.mk, CategoryTheory.MorphismProperty.multiplicativeClosure.of, CategoryTheory.MorphismProperty.comp_mem, SimplexCategoryGenRel.generators.δ, CategoryTheory.Quotient.comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
u : FreeSimplexQuiver
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:
exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
u : FreeSimplexQuiver
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:
generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, SimplexCategoryGenRel.mk, FreeSimplexQuiver.mk, CategoryTheory.MorphismProperty.multiplicativeClosure.of, SimplexCategoryGenRel.generators.σ, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.Quotient.comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
x_1 y_1 : Paths FreeSimplexQuiver
u : FreeSimplexQuiver
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:
exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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)))
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))
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)

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 _ <| .σ _

Premises used: CategoryTheory.Paths.induction, CategoryTheory.MorphismProperty.multiplicativeClosure, SimplexCategoryGenRel.generators, id, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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 = ⊤

Tactic:
rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this

Premises used: SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, top_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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 = ⊤
rw : ⊤ f
⊢ P f

Tactic:
rw [this]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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 = ⊤
⊢ ⊤ f

Tactic:
apply MorphismProperty.top_apply

Premises used: CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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
suffices : generators.multiplicativeClosure ≤ P
⊢ P f

Tactic:
suffices generators.multiplicativeClosure ≤ P by
    rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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
X : SimplexCategoryGenRel
_ : ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X ⟶ Y), generators.multiplicativeClosure f → P f
⊢ ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X ⟶ Y), generators.multiplicativeClosure f → P f

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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)
of₁ : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 1)), P (σ i)
⊢ P f

Tactic:
rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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_1 Y_1 : SimplexCategoryGenRel
f : X_1 ⟶ Y_1
X Y : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 2)
⊢ P (δ i)

Tactic:
simpa using (comp_δ (𝟙 _) i id)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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_1 Y_1 : SimplexCategoryGenRel
f : X_1 ⟶ Y_1
X Y : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 1)
⊢ P (σ i)

Tactic:
simpa using (comp_σ (𝟙 _) i id)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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
n : SimplexCategoryGenRel
⊢ P (𝟙 n)

Tactic:
id

Premises used: SimplexCategoryGenRel.mk, SimplexCategoryGenRel
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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
n : SimplexCategoryGenRel
⊢ P (𝟙 n)

Tactic:
exact id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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)
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)
⊢ P (f ≫ g)

Tactic:
rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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_1 Y_1 : SimplexCategoryGenRel
f_2 : X_1 ⟶ Y_1
x X Y : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 2)
f : x ⟶ mk n
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ δ i)

Tactic:
simpa using (comp_δ f i hrec)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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_1 Y_1 : SimplexCategoryGenRel
f_2 : X_1 ⟶ Y_1
x X Y : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 1)
f : x ⟶ mk (n + 1)
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ σ i)

Tactic:
simpa using (comp_σ f i hrec)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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)
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)
⊢ 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)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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 = ⊤

Tactic:
rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
      multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this

Premises used: SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, CategoryTheory.MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure', top_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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 = ⊤
rw : ⊤ f
⊢ P f

Tactic:
rw [this]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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 = ⊤
⊢ ⊤ f

Tactic:
apply MorphismProperty.top_apply

Premises used: CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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
suffices : generators.multiplicativeClosure' ≤ P
⊢ P f

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
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
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
X : SimplexCategoryGenRel
_ : ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X ⟶ Y), generators.multiplicativeClosure' f → P f
⊢ ∀ ⦃Y : SimplexCategoryGenRel⦄ (f : X ⟶ Y), generators.multiplicativeClosure' f → P f

Tactic:
_