awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
last : δ (Fin.last (n + 1)) ≫ σ (Fin.last n) = 𝟙 (mk 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)

Tactic:
simp only [Fin.lastCases_last]

Premises used: Fin.lastCases_last
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ σ (Fin.last n) = 𝟙 (mk n)

Tactic:
δ_comp_σ_succ

Premises used: SimplexCategoryGenRel.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ σ (Fin.last n) = 𝟙 (mk n)

Tactic:
exact δ_comp_σ_succ

Premises used: SimplexCategoryGenRel.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
cast : δ i.castSucc ≫ σ i = 𝟙 (mk n)
⊢ δ 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:
simp only [Fin.lastCases_castSucc]

Premises used: Fin.lastCases_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk n)

Tactic:
δ_comp_σ_self

Premises used: SimplexCategoryGenRel.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk n)

Tactic:
exact δ_comp_σ_self

Premises used: SimplexCategoryGenRel.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
⊢ IsSplitMono (δ i)

Tactic:
.mk' <| splitMonoδ i

Premises used: SimplexCategoryGenRel.splitMonoδ, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
⊢ IsSplitEpi (σ i)

Tactic:
.mk' <| splitEpiσ i

Premises used: SimplexCategoryGenRel.splitEpiσ, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 1)
⊢ P_σ (SimplexCategoryGenRel.σ i)

Tactic:
.of _ (.σ i)

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.of, SimplexCategoryGenRel.degeneracies.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
⊢ P_δ (SimplexCategoryGenRel.δ i)

Tactic:
.of _ (.δ i)

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.of, SimplexCategoryGenRel.faces.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x_1 y : SimplexCategoryGenRel
e : x_1 ⟶ y
x_2 y_1 : SimplexCategoryGenRel
x : x_2 ⟶ y_1
hx : degeneracies x
of : ∀ {n : ℕ} (i : Fin (n + 1)), IsSplitEpi (σ i)
⊢ IsSplitEpi x

Tactic:
cases hx
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
n : ℕ
i : Fin (n + 1)
⊢ IsSplitEpi (σ i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
x_1 : SimplexCategoryGenRel
⊢ IsSplitEpi (𝟙 x_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
comp_of :
  ∀ {n : ℕ} (i : Fin (n + 1)) (f : x_1 ⟶ mk (n + 1)),
    degeneracies.multiplicativeClosure f → IsSplitEpi f → IsSplitEpi (f ≫ σ i)
⊢ IsSplitEpi (f ≫ g)

Tactic:
cases h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
x_1 : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 1)
f : x_1 ⟶ mk (n + 1)
hf : degeneracies.multiplicativeClosure f
hf_ih : IsSplitEpi f
⊢ IsSplitEpi (f ≫ σ i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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)
comp_of :
  ∀ {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z),
    degeneracies.multiplicativeClosure f → ∀ (h : degeneracies g), IsSplitEpi f → IsSplitEpi (f ≫ g)
⊢ IsSplitEpi e

Tactic:
induction he with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance

Premises used: id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x_1 y : SimplexCategoryGenRel
m : x_1 ⟶ y
x_2 y_1 : SimplexCategoryGenRel
x : x_2 ⟶ y_1
hx : faces x
of : ∀ {n : ℕ} (i : Fin (n + 2)), IsSplitMono (δ i)
⊢ IsSplitMono x

Tactic:
cases hx
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
n : ℕ
i : Fin (n + 2)
⊢ IsSplitMono (δ i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
x_1 : SimplexCategoryGenRel
⊢ IsSplitMono (𝟙 x_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
comp_of :
  ∀ {n : ℕ} (i : Fin (n + 2)) (f : x_1 ⟶ mk n), faces.multiplicativeClosure f → IsSplitMono f → IsSplitMono (f ≫ δ i)
⊢ IsSplitMono (f ≫ g)

Tactic:
cases h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
x_1 : SimplexCategoryGenRel
n : ℕ
i : Fin (n + 2)
f : x_1 ⟶ mk n
hf : faces.multiplicativeClosure f
hf_ih : IsSplitMono f
⊢ IsSplitMono (f ≫ δ i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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)
comp_of :
  ∀ {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z),
    faces.multiplicativeClosure f → ∀ (h : faces g), IsSplitMono f → IsSplitMono (f ≫ g)
⊢ IsSplitMono m

Tactic:
induction hm with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance

Premises used: id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
exists_splitEpi : Nonempty (SplitEpi (toSimplexCategory.map e))
⊢ IsSplitEpi (toSimplexCategory.map e)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
exists_splitEpi : SplitEpi (toSimplexCategory.map e)
⊢ Nonempty (SplitEpi (toSimplexCategory.map e))

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
exists_splitEpi : SplitEpi e
⊢ SplitEpi (toSimplexCategory.map e)

Tactic:
apply SplitEpi.map

Premises used: CategoryTheory.SplitEpi.map
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi e

Tactic:
exact isSplitEpi_P_σ he |>.exists_splitEpi.some

Premises used: Nonempty.some, CategoryTheory.IsSplitEpi.exists_splitEpi
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
exists_splitMono : Nonempty (SplitMono (toSimplexCategory.map m))
⊢ IsSplitMono (toSimplexCategory.map m)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
exists_splitMono : SplitMono (toSimplexCategory.map m)
⊢ Nonempty (SplitMono (toSimplexCategory.map m))

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
exists_splitMono : SplitMono m
⊢ SplitMono (toSimplexCategory.map m)

Tactic:
apply SplitMono.map

Premises used: CategoryTheory.SplitMono.map
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono m

Tactic:
exact isSplitMono_P_δ hm |>.exists_splitMono.some

Premises used: Nonempty.some, CategoryTheory.IsSplitMono.exists_splitMono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 y_1 : SimplexCategoryGenRel
f_1 : x_1 ⟶ y_1
hx : faces f_1
of : ∀ {n : ℕ} (i : Fin (n + 2)), (∃ (h : mk n = mk (n + 1)), δ i = eqToHom h) ∨ (mk n).len < (mk (n + 1)).len
⊢ (∃ (h : x_1 = y_1), f_1 = eqToHom h) ∨ x_1.len < y_1.len

Tactic:
cases hx
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
n : ℕ
i : Fin (n + 2)
of : (mk n).len < (mk (n + 1)).len
⊢ (∃ (h : mk n = mk (n + 1)), δ i = eqToHom h) ∨ (mk n).len < (mk (n + 1)).len

Tactic:
right
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
n : ℕ
i : Fin (n + 2)
⊢ (mk n).len < (mk (n + 1)).len

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
id : ∃ (h : x_1 = x_1), 𝟙 x_1 = eqToHom h
⊢ (∃ (h : x_1 = x_1), 𝟙 x_1 = eqToHom h) ∨ x_1.len < x_1.len

Tactic:
left
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
h : 𝟙 x_1 = eqToHom ⋯
⊢ ∃ (h : x_1 = x_1), 𝟙 x_1 = eqToHom h

Tactic:
use rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
⊢ 𝟙 x_1 = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
comp_of₁ : ∀ (h' : x_1.len < y_1.len), (∃ (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

Tactic:
rcases h' with ⟨e, _⟩ | h'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
comp_of : x_1.len < z.len
⊢ (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
comp_of : x_1.len < z.len
⊢ (∃ (h : x_1 = z), i ≫ u = eqToHom h) ∨ x_1.len < z.len

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
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
⊢ x_1.len < z.len

Tactic:
cases hg
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
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
⊢ x_1.len < z.len

Tactic:
cases hg
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
comp_of : (mk n).len < (mk (n + 1)).len
⊢ x_1.len < (mk (n + 1)).len

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
⊢ (mk n).len < (mk (n + 1)).len

Tactic:
Nat.lt_add_one _

Premises used: Nat.lt_add_one, SimplexCategoryGenRel.len
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
⊢ (mk n).len < (mk (n + 1)).len

Tactic:
exact Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
h' : x_1.len < (mk n).len
⊢ x_1.len < (mk (n + 1)).len

Tactic:
Nat.lt_succ_of_lt h'

Premises used: Nat.lt_succ_of_lt, SimplexCategoryGenRel.len
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
h' : x_1.len < (mk n).len
⊢ x_1.len < (mk (n + 1)).len

Tactic:
exact Nat.lt_succ_of_lt h'

Premises used: Nat.lt_succ_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
h_δ : P_δ f
of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hx : faces f), (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len
id : ∀ (x : SimplexCategoryGenRel), (∃ (h : x = x), 𝟙 x = eqToHom h) ∨ x.len < x.len
comp_of :
  ∀ {x y z : SimplexCategoryGenRel} (i : x ⟶ y) (u : y ⟶ z),
    faces.multiplicativeClosure i →
      ∀ (hg : faces u) (h' : (∃ (h : x = y), i = eqToHom h) ∨ x.len < y.len),
        (∃ (h : x = z), i ≫ u = eqToHom h) ∨ x.len < z.len
⊢ (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len

Tactic:
induction h_δ with
  | of _ hx => cases hx; right; simp
  | id => left; use rfl; simp
  | comp_of i u _ hg h' =>
    rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr <;>
    cases hg
    · rw [e]
      exact Nat.lt_add_one _
    · exact Nat.lt_succ_of_lt h'

Premises used: id, Nat.lt_add_one, Or.inr, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
inl :
  ∀ (h : i.castSucc < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
inr : δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.castSucc ≫ σ i = σ j ≫ δ j'
inr₁ :
  ∀ (h : i' < i.castSucc), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain h | rfl | h := lt_trichotomy i.castSucc i'

Premises used: Fin.castSucc, rfl, lt_trichotomy
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.castSucc < i'
⊢ i.succ ≤ i'

Tactic:
rw [Fin.castSucc_lt_iff_succ_le] at h

Premises used: Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
inl : ∀ (h : i.succ < i'), δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'
inl₁ :
  ∀ (h : i.succ ≤ i.succ),
    δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.succ ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain h | rfl := h.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h_1 : i.succ ≤ i'
h : i.succ < i'
inl :
  ∀ (i' : Fin (n + 2)) (h : i.succ ≤ i'.succ) (h : i.succ < i'.succ),
    δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i i' : Fin (n + 2)
h_1 : i.succ ≤ i'.succ
h : i.succ < i'.succ
⊢ i < i'

Tactic:
rw [Fin.succ_lt_succ_iff] at h

Premises used: Fin.succ_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i i' : Fin (n + 2)
h_1 : i.succ ≤ i'.succ
h : i < i'
inl :
  ∀ (i : Fin (n + 1)) (h : i.castSucc.succ ≤ i'.succ) (h : i.castSucc < i'),
    δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨
      ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Premises used: Fin.eq_castSucc_of_ne_last, Fin.ne_last_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h_1 : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
rw rw₁ : σ i ≫ δ i' = σ i ≫ δ i'
⊢ δ i'.succ ≫ σ i.castSucc = σ i ≫ δ i'

Tactic:
rw [δ_comp_σ_of_gt h]

Premises used: SimplexCategoryGenRel.δ_comp_σ_of_gt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h_1 : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨
    ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'

Tactic:
exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_gt h]⟩

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.succ ≫ σ i = σ j ≫ δ j'

Tactic:
Or.inl δ_comp_σ_succ

Premises used: SimplexCategoryGenRel.δ_comp_σ_succ, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.succ ≫ σ i = σ j ≫ δ j'

Tactic:
exact Or.inl δ_comp_σ_succ

Premises used: SimplexCategoryGenRel.δ_comp_σ_succ, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
Or.inl δ_comp_σ_self

Premises used: SimplexCategoryGenRel.δ_comp_σ_self, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
exact Or.inl δ_comp_σ_self

Premises used: SimplexCategoryGenRel.δ_comp_σ_self, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
inr :
  ∀ (i' : Fin (n + 2)) (h : i'.castSucc < i.castSucc),
    δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i = σ j ≫ δ j'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Premises used: Fin.eq_castSucc_of_ne_last, Fin.ne_last_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i i' : Fin (n + 2)
h : i'.castSucc < i.castSucc
⊢ i' < i

Tactic:
rw [Fin.castSucc_lt_castSucc_iff] at h

Premises used: Fin.castSucc_lt_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i i' : Fin (n + 2)
h : i' < i
inr :
  ∀ (i : Fin (n + 1)) (h : i' < i.succ),
    δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨
      ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' < i.succ
⊢ i' ≤ i.castSucc

Tactic:
rw [← Fin.le_castSucc_iff] at h

Premises used: Fin.le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
rw rw₁ : σ i ≫ δ i' = σ i ≫ δ i'
⊢ δ i'.castSucc ≫ σ i.succ = σ i ≫ δ i'

Tactic:
rw [δ_comp_σ_of_le h]

Premises used: SimplexCategoryGenRel.δ_comp_σ_of_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨
    ∃ (j : Fin (n + 1)) (j' : Fin (n + 2)), δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'

Tactic:
exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_le h]⟩

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i : Fin 1
i' : Fin 2
0 :
  δ i' ≫
      σ
        ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 0 : SimplexCategory }.len + 1))) =
    𝟙 (mk 0)
⊢ δ i' ≫ σ i = 𝟙 (mk 0)

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
i' : Fin 2
0 :
  δ
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
      σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    𝟙 (mk 0)
h :
  δ
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
          (⟨1, ⋯⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
      σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    𝟙 (mk 0)
⊢ δ i' ≫
      σ
        ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 0 : SimplexCategory }.len + 1))) =
    𝟙 (mk 0)

Tactic:
fin_cases i'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
⊢ δ
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i)
          (⟨0, ⋯⟩ : Fin ({ len := 1 : SimplexCategory }.len + 1))) ≫
      σ ((fun (i : Fin ({ len := 0 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    𝟙 (mk 0)

Tactic:
δ_comp_σ_self

Premises used: SimplexCategoryGenRel.δ_comp_σ_self