awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 (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_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 (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_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 (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_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 (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_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 (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_1 : a ⟶ b
X Y : SimplexCategoryGenRel
f_2 : X ⟶ Y
x y z : SimplexCategoryGenRel
f : x ⟶ y
g : y ⟶ z
hf : generators f
hg : generators.multiplicativeClosure' g
hrec : P g
of_comp :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 2)) (g : mk (n + 1) ⟶ z)
    (hg : generators.multiplicativeClosure' g) (hrec : P g), P (δ i ≫ g)
of_comp₁ :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 1)) (g : mk n ⟶ z) (hg : generators.multiplicativeClosure' g)
    (hrec : P g), P (σ i ≫ g)
⊢ P (f ≫ g)

Tactic:
rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
-- 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_1 : a ⟶ b
X_1 Y_1 : SimplexCategoryGenRel
f : X_1 ⟶ Y_1
z X Y : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 2)
g : mk (n + 1) ⟶ z
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (δ i ≫ g)

Tactic:
simpa using (δ_comp g 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_1 : a ⟶ b
X_1 Y_1 : SimplexCategoryGenRel
f : X_1 ⟶ Y_1
z X Y : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 1)
g : mk n ⟶ z
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (σ i ≫ g)

Tactic:
simpa using (σ_comp g 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_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)
of_comp :
  ∀ {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z) (hf : generators f)
    (hg : generators.multiplicativeClosure' g) (hrec : P g), 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
  | of_comp f g hf hg hrec =>
    rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (δ_comp g i hrec)
    · simpa using (σ_comp g i hrec)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
P : SimplexCategoryGenRel → Sort u_1
H : (n : ℕ) → P (mk n)
x : SimplexCategoryGenRel
⊢ P x

Tactic:
exact H x.len

Premises used: SimplexCategoryGenRel.len
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x y : SimplexCategoryGenRel
h : x.len = y.len
H : ∀ (n : ℕ) (h : (mk n).len = y.len), mk n = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
y : SimplexCategoryGenRel
n : ℕ
h : (mk n).len = y.len
H : ∀ (n_1 : ℕ) (h : (mk n).len = (mk n_1).len), mk n = mk n_1
⊢ mk n = y

Tactic:
cases y
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n n_1 : ℕ
h : n = n_1
⊢ mk n = mk n_1

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
h :
  FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ j.succ)))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc)))
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
apply CategoryTheory.Quotient.sound

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ j.succ)))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc)))

Tactic:
FreeSimplexQuiver.homRel.δ_comp_δ H

Premises used: FreeSimplexQuiver.mk, FreeSimplexQuiver.homRel.δ_comp_δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ j.succ)))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc)))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_δ H

Premises used: FreeSimplexQuiver.homRel.δ_comp_δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
h :
  FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1))
    (CategoryStruct.comp (Y := (mk (n + 1 + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.succ)))
    (CategoryStruct.comp (Y := (mk n).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1))
    (CategoryStruct.comp (Y := (mk (n + 1 + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.succ)))
    (CategoryStruct.comp (Y := (mk n).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))

Tactic:
FreeSimplexQuiver.homRel.δ_comp_σ_of_le H

Premises used: FreeSimplexQuiver.homRel.δ_comp_σ_of_le, FreeSimplexQuiver.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1))
    (CategoryStruct.comp (Y := (mk (n + 1 + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.succ)))
    (CategoryStruct.comp (Y := (mk n).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_of_le H

Premises used: FreeSimplexQuiver.homRel.δ_comp_σ_of_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
h :
  FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
    (𝟙 ((mk n).as (r := FreeSimplexQuiver.homRel)))
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk n)

Tactic:
apply CategoryTheory.Quotient.sound

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
    (𝟙 ((mk n).as (r := FreeSimplexQuiver.homRel)))

Tactic:
FreeSimplexQuiver.homRel.δ_comp_σ_self

Premises used: FreeSimplexQuiver.mk, FreeSimplexQuiver.homRel.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
    (𝟙 ((mk n).as (r := FreeSimplexQuiver.homRel)))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_self

Premises used: FreeSimplexQuiver.homRel.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
h :
  FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
    (𝟙 ((mk n).as (r := FreeSimplexQuiver.homRel)))
⊢ δ i.succ ≫ σ i = 𝟙 (mk n)

Tactic:
apply CategoryTheory.Quotient.sound

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
    (𝟙 ((mk n).as (r := FreeSimplexQuiver.homRel)))

Tactic:
FreeSimplexQuiver.homRel.δ_comp_σ_succ

Premises used: FreeSimplexQuiver.mk, FreeSimplexQuiver.homRel.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) n)
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
    (𝟙 ((mk n).as (r := FreeSimplexQuiver.homRel)))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_succ

Premises used: FreeSimplexQuiver.homRel.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
h :
  FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1))
    (CategoryStruct.comp (Y := (mk (n + 1 + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.castSucc)))
    (CategoryStruct.comp (Y := (mk n).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1))
    (CategoryStruct.comp (Y := (mk (n + 1 + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.castSucc)))
    (CategoryStruct.comp (Y := (mk n).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))

Tactic:
FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H

Premises used: FreeSimplexQuiver.mk, FreeSimplexQuiver.homRel.δ_comp_σ_of_gt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1))
    (CategoryStruct.comp (Y := (mk (n + 1 + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.castSucc)))
    (CategoryStruct.comp (Y := (mk n).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.δ i)))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H

Premises used: FreeSimplexQuiver.homRel.δ_comp_σ_of_gt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
h :
  FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1 + 1))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j)))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
apply CategoryTheory.Quotient.sound

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1 + 1))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j)))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))

Tactic:
FreeSimplexQuiver.homRel.σ_comp_σ H

Premises used: FreeSimplexQuiver.mk, FreeSimplexQuiver.homRel.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel (X := Prefunctor.obj (Paths.of FreeSimplexQuiver) (n + 1 + 1))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i.castSucc))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j)))
    (CategoryStruct.comp (Y := (mk (n + 1)).as (r := FreeSimplexQuiver.homRel))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ j.succ))
      (Prefunctor.map (Paths.of FreeSimplexQuiver) (FreeSimplexQuiver.Hom.σ i)))

Tactic:
exact FreeSimplexQuiver.homRel.σ_comp_σ H

Premises used: FreeSimplexQuiver.homRel.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ j + 1 < n + 1 + 2

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ i < n + 1 + 2

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ i < n + 2

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ j < n + 2

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ (⟨i, ⋯⟩ : Fin (n + 2)) ≤ ⟨j, ⋯⟩

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ i < n + 1 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ j + 1 < n + 1 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ i < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ j < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ (⟨i, ⋯⟩ : Fin (n + 1)) ≤ ⟨j, ⋯⟩

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
⊢ toSimplexCategory.obj (mk n) = { len := n }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 2)
⊢ toSimplexCategory.map (δ i) = SimplexCategory.δ i

Tactic:
rfl

Premises used: Fin.succAbove, SimplexCategory.mkHom, FreeSimplexQuiver.mk, SimplexCategory.δ, OrderHom.comp, SimplexCategory.Hom.comp, OrderEmbedding.toOrderHom, rfl, ite, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ toSimplexCategory.map (σ i) = SimplexCategory.σ i

Tactic:
rfl

Premises used: SimplexCategory.mkHom, FreeSimplexQuiver.mk, SimplexCategory.σ, OrderHom.comp, Fin.predAbove, dite, SimplexCategory.Hom.comp, Fin.predAboveOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Goal:
x : SimplexCategoryGenRel
⊢ (toSimplexCategory.obj x).len = x.len

Tactic:
rfl

Premises used: SimplexCategoryGenRel.len, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
⊢ mk (n + 1) ⟶ mk n

Tactic:
exact σ (Fin.last n)

Premises used: SimplexCategoryGenRel.σ, Fin.last
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
⊢ mk (n + 1) ⟶ mk n

Tactic:
exact σ i

Premises used: SimplexCategoryGenRel.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
last : mk (n + 1) ⟶ mk n
cast : (i : Fin (n + 1)) → mk (n + 1) ⟶ mk n
⊢ mk (n + 1) ⟶ mk n

Tactic:
induction i using Fin.lastCases with
    | last => exact σ (Fin.last n)
    | cast i => exact σ i

Premises used: cast, SimplexCategoryGenRel.σ, Fin.last
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
last :
  δ (Fin.last (n + 1)) ≫
      Fin.lastCases (motive := fun (i : Fin (n + 2)) ↦ mk (n + 1) ⟶ mk n) (σ (Fin.last n)) (fun (i : Fin (n + 1)) ↦ σ i)
        (Fin.last (n + 1)) =
    𝟙 (mk n)
cast :
  ∀ (i : Fin (n + 1)),
    δ i.castSucc ≫
        Fin.lastCases (motive := fun (i : Fin (n + 2)) ↦ mk (n + 1) ⟶ mk n) (σ (Fin.last n))
          (fun (i : Fin (n + 1)) ↦ σ i) i.castSucc =
      𝟙 (mk n)
⊢ δ i ≫
      Fin.lastCases (motive := fun (i : Fin (n + 2)) ↦ mk (n + 1) ⟶ mk n) (σ (Fin.last n)) (fun (i : Fin (n + 1)) ↦ σ i)
        i =
    𝟙 (mk n)

Tactic:
cases i using Fin.lastCases