awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 (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)
⊢ 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 (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
⊢ P (f ≫ g)
have 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)
Tactic: rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
Cleared hypotheses: x, y, 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 (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)
⊢ P (f ≫ g)
have of_comp₁ : ∀ ⦃X Y : SimplexCategoryGenRel⦄ {n : ℕ} (i : Fin (n + 1)) (g : mk n ⟶ z) (hg : generators.multiplicativeClosure' g)
  (hrec : P g), P (σ i ≫ g)
Tactic: rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
Cleared hypotheses: x, y, 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 (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
⊢ 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
  | of_comp f g hf hg hrec =>
    rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (δ_comp g i hrec)
    · simpa using (σ_comp g 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 (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
⊢ 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
  | of_comp f g hf hg hrec =>
    rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using (δ_comp g i hrec)
    · simpa using (σ_comp g 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 (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)
⊢ P f
have 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)
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)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
x y : SimplexCategoryGenRel
h : x.len = y.len
⊢ x = y
have H : ∀ (n : ℕ) (h : (mk n).len = y.len), mk n = y
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
y : SimplexCategoryGenRel
n : ℕ
h : (mk n).len = y.len
⊢ mk n = y
have H : ∀ (n_1 : ℕ) (h : (mk n).len = (mk n_1).len), mk n = mk n_1
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc
have 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)))
Tactic: apply CategoryTheory.Quotient.sound
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i
have 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)))
Tactic: apply CategoryTheory.Quotient.sound
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk n)
have 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)))
Tactic: apply CategoryTheory.Quotient.sound
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 (mk n)
have 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)))
Tactic: apply CategoryTheory.Quotient.sound
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i
have 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)))
Tactic: apply CategoryTheory.Quotient.sound
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i
have 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)))
Tactic: apply CategoryTheory.Quotient.sound
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
last : mk (n + 1) ⟶ mk n
⊢ mk (n + 1) ⟶ mk n
have cast : (i : Fin (n + 1)) → mk (n + 1) ⟶ mk n
Tactic: induction i using Fin.lastCases with
    | last => exact σ (Fin.last n)
    | cast i => exact σ i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ δ 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)
have 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)
Tactic: cases i using Fin.lastCases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
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)
⊢ δ 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)
have 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)
Tactic: cases i using Fin.lastCases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
⊢ δ (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)
have last : δ (Fin.last (n + 1)) ≫ σ (Fin.last n) = 𝟙 (mk n)
Tactic: simp only [Fin.lastCases_last]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
n : ℕ
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)
have cast : δ i.castSucc ≫ σ i = 𝟙 (mk n)
Tactic: simp only [Fin.lastCases_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x_1 y : SimplexCategoryGenRel
e : x_1 ⟶ y
x_2 y_1 : SimplexCategoryGenRel
x : x_2 ⟶ y_1
hx : degeneracies x
⊢ IsSplitEpi x
have of : ∀ {n : ℕ} (i : Fin (n + 1)), IsSplitEpi (σ i)
Tactic: cases hx
Cleared hypotheses: x_2, y_1, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
f : x_1 ⟶ y_1
g : y_1 ⟶ z
hf : degeneracies.multiplicativeClosure f
h : degeneracies g
hf_ih : IsSplitEpi f
⊢ IsSplitEpi (f ≫ g)
have comp_of : ∀ {n : ℕ} (i : Fin (n + 1)) (f : x_1 ⟶ mk (n + 1)),
  degeneracies.multiplicativeClosure f → IsSplitEpi f → IsSplitEpi (f ≫ σ i)
Tactic: cases h
Cleared hypotheses: y_1, z, f, g, hf, h, hf_ih
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi e
have of : ∀ {x y : SimplexCategoryGenRel} (x_1 : x ⟶ y) (hx : degeneracies x_1), IsSplitEpi x_1
Tactic: induction he with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
of : ∀ {x y : SimplexCategoryGenRel} (x_1 : x ⟶ y) (hx : degeneracies x_1), IsSplitEpi x_1
⊢ IsSplitEpi e
have id : ∀ (x : SimplexCategoryGenRel), IsSplitEpi (𝟙 x)
Tactic: induction he with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
of : ∀ {x y : SimplexCategoryGenRel} (x_1 : x ⟶ y) (hx : degeneracies x_1), IsSplitEpi x_1
id : ∀ (x : SimplexCategoryGenRel), IsSplitEpi (𝟙 x)
⊢ IsSplitEpi e
have comp_of : ∀ {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z),
  degeneracies.multiplicativeClosure f → ∀ (h : degeneracies g), IsSplitEpi f → IsSplitEpi (f ≫ g)
Tactic: induction he with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x_1 y : SimplexCategoryGenRel
m : x_1 ⟶ y
x_2 y_1 : SimplexCategoryGenRel
x : x_2 ⟶ y_1
hx : faces x
⊢ IsSplitMono x
have of : ∀ {n : ℕ} (i : Fin (n + 2)), IsSplitMono (δ i)
Tactic: cases hx
Cleared hypotheses: x_2, y_1, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
f : x_1 ⟶ y_1
g : y_1 ⟶ z
hf : faces.multiplicativeClosure f
h : faces g
hf_ih : IsSplitMono f
⊢ IsSplitMono (f ≫ g)
have comp_of : ∀ {n : ℕ} (i : Fin (n + 2)) (f : x_1 ⟶ mk n), faces.multiplicativeClosure f → IsSplitMono f → IsSplitMono (f ≫ δ i)
Tactic: cases h
Cleared hypotheses: y_1, z, f, g, hf, h, hf_ih
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono m
have of : ∀ {x y : SimplexCategoryGenRel} (x_1 : x ⟶ y) (hx : faces x_1), IsSplitMono x_1
Tactic: induction hm with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
of : ∀ {x y : SimplexCategoryGenRel} (x_1 : x ⟶ y) (hx : faces x_1), IsSplitMono x_1
⊢ IsSplitMono m
have id : ∀ (x : SimplexCategoryGenRel), IsSplitMono (𝟙 x)
Tactic: induction hm with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
of : ∀ {x y : SimplexCategoryGenRel} (x_1 : x ⟶ y) (hx : faces x_1), IsSplitMono x_1
id : ∀ (x : SimplexCategoryGenRel), IsSplitMono (𝟙 x)
⊢ IsSplitMono m
have comp_of : ∀ {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z),
  faces.multiplicativeClosure f → ∀ (h : faces g), IsSplitMono f → IsSplitMono (f ≫ g)
Tactic: induction hm with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi (toSimplexCategory.map e)
have exists_splitEpi : Nonempty (SplitEpi (toSimplexCategory.map e))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ Nonempty (SplitEpi (toSimplexCategory.map e))
have exists_splitEpi : SplitEpi (toSimplexCategory.map e)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi (toSimplexCategory.map e)
have exists_splitEpi : SplitEpi e
Tactic: apply SplitEpi.map
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono (toSimplexCategory.map m)
have exists_splitMono : Nonempty (SplitMono (toSimplexCategory.map m))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ Nonempty (SplitMono (toSimplexCategory.map m))
have exists_splitMono : SplitMono (toSimplexCategory.map m)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono (toSimplexCategory.map m)
have exists_splitMono : SplitMono m
Tactic: apply SplitMono.map
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 : SimplexCategoryGenRel
f_1 : x_1 ⟶ y_1
hx : faces f_1
⊢ (∃ (h : x_1 = y_1), f_1 = eqToHom h) ∨ x_1.len < y_1.len
have of : ∀ {n : ℕ} (i : Fin (n + 2)), (∃ (h : mk n = mk (n + 1)), δ i = eqToHom h) ∨ (mk n).len < (mk (n + 1)).len
Tactic: cases hx
Cleared hypotheses: x_1, y_1, f_1, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
n : ℕ
i : Fin (n + 2)
⊢ (∃ (h : mk n = mk (n + 1)), δ i = eqToHom h) ∨ (mk n).len < (mk (n + 1)).len
have of : (mk n).len < (mk (n + 1)).len
Tactic: right
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
⊢ (∃ (h : x_1 = x_1), 𝟙 x_1 = eqToHom h) ∨ x_1.len < x_1.len
have id : ∃ (h : x_1 = x_1), 𝟙 x_1 = eqToHom h
Tactic: left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
⊢ ∃ (h : x_1 = x_1), 𝟙 x_1 = eqToHom h
have h : 𝟙 x_1 = eqToHom sorry
Tactic: use rfl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
i : x_1 ⟶ y_1
u : y_1 ⟶ z
hf : faces.multiplicativeClosure i
hg : faces u
h' : (∃ (h : x_1 = y_1), i = eqToHom h) ∨ x_1.len < y_1.len
⊢ (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
have comp_of : ∀ (e : x_1 = y_1), i = eqToHom e → (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
Tactic: rcases h' with ⟨e, _⟩ | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
i : x_1 ⟶ y_1
u : y_1 ⟶ z
hf : faces.multiplicativeClosure i
hg : faces u
h' : (∃ (h : x_1 = y_1), i = eqToHom h) ∨ x_1.len < y_1.len
comp_of : ∀ (e : x_1 = y_1), i = eqToHom e → (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
⊢ (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
have comp_of₁ : ∀ (h' : x_1.len < y_1.len), (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
Tactic: rcases h' with ⟨e, _⟩ | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
i : x_1 ⟶ y_1
u : y_1 ⟶ z
hf : faces.multiplicativeClosure i
hg : faces u
e : x_1 = y_1
h : i = eqToHom e
⊢ (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
have comp_of : x_1.len < z.len
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
i : x_1 ⟶ y_1
u : y_1 ⟶ z
hf : faces.multiplicativeClosure i
hg : faces u
h' : x_1.len < y_1.len
⊢ (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len
have comp_of : x_1.len < z.len
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
i : x_1 ⟶ y_1
u : y_1 ⟶ z
hf : faces.multiplicativeClosure i
hg : faces u
e : x_1 = y_1
h : i = eqToHom e
⊢ x_1.len < z.len
have comp_of : ∀ {n : ℕ} (i : Fin (n + 2)) (i : x_1 ⟶ mk n),
  faces.multiplicativeClosure i → ∀ (e : x_1 = mk n), i = eqToHom e → x_1.len < (mk (n + 1)).len
Tactic: cases hg
Cleared hypotheses: y_1, z, i, u, hf, hg, e, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 z : SimplexCategoryGenRel
i : x_1 ⟶ y_1
u : y_1 ⟶ z
hf : faces.multiplicativeClosure i
hg : faces u
h' : x_1.len < y_1.len
⊢ x_1.len < z.len
have comp_of : ∀ {n : ℕ} (i : Fin (n + 2)) (i : x_1 ⟶ mk n),
  faces.multiplicativeClosure i → ∀ (h' : x_1.len < (mk n).len), x_1.len < (mk (n + 1)).len
Tactic: cases hg
Cleared hypotheses: y_1, z, i, u, hf, hg, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
n : ℕ
i_1 : Fin (n + 2)
i : x_1 ⟶ mk n
hf : faces.multiplicativeClosure i
e : x_1 = mk n
h : i = eqToHom e
⊢ x_1.len < (mk (n + 1)).len
have comp_of : (mk n).len < (mk (n + 1)).len
Tactic: rw [e]