-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
/-- An unrolled version of the induction principle obtained in the previous lemma. -/
@[elab_as_elim, cases_eliminator, induction_eliminator]
lemma hom_induction (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) :
    P f :=
  by
  suffices generators.multiplicativeClosure ≤ P by
    rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
  intro _ _ f hf
  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)

Proof state:
case comp_of
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✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf : generators.multiplicativeClosure f
hg : generators g
hrec : P f
⊢ P (f ≫ g)

Tactic:
rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩

Result:
case comp_of.inl.δ
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✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
f : x✝ ⟶ mk n✝
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ δ i)

case comp_of.inr.σ
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✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
f : x✝ ⟶ mk (n✝ + 1)
hf : generators.multiplicativeClosure f
hrec : P f
⊢ P (f ≫ σ i)

Proof state:
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
⊢ generators.multiplicativeClosure ≤ P

Tactic:
intro _ _ f hf

Result:
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✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure f
⊢ P f