-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
lemma eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P_δ f) :
    (∃ h : x = y, f = eqToHom h) ∨ x.len < y.len

Proof state:
case id.h
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ ∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h

Tactic:
use rfl

Result:
case h
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ 𝟙 x✝ = eqToHom ⋯

Proof state:
case id
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ (∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h) ∨ x✝.len < x✝.len

Tactic:
left

Result:
case id.h
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ ∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h

Proof state:
case comp_of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : 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

Tactic:
rcases h' with ⟨e, _⟩ | h' <;>
apply Or.inr <;>
cases hg

Result:
case comp_of.inl.intro.h.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ x✝.len < (mk (n✝ + 1)).len

case comp_of.inr.h.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
h' : x✝.len < (mk n✝).len
⊢ x✝.len < (mk (n✝ + 1)).len

Proof state:
case comp_of.inr.h.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
h' : x✝.len < (mk n✝).len
⊢ x✝.len < (mk (n✝ + 1)).len

Tactic:
exact Nat.lt_succ_of_lt h'

Result:
no goals

Proof state:
case comp_of.inl.intro.h.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Tactic:
exact Nat.lt_add_one _

Result:
no goals

Proof state:
case of.δ.h
x y : SimplexCategoryGenRel
f : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 2)
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Tactic:
simp

Result:
no goals

Proof state:
case of.δ
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

Tactic:
right

Result:
case of.δ.h
x y : SimplexCategoryGenRel
f : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 2)
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Proof state:
case h
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ 𝟙 x✝ = eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
case comp_of.inl.intro.h.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ x✝.len < (mk (n✝ + 1)).len

Tactic:
rw [e]

Result:
case comp_of.inl.intro.h.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Proof state:
case of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
hx : faces f✝
⊢ (∃ (h : x✝ = y✝), f✝ = eqToHom h) ∨ x✝.len < y✝.len

Tactic:
cases hx

Result:
case of.δ
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