-- Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean
/-- Two morphisms from a horn are equal if they are equal on all suitable faces. -/
protected
lemma hom_ext {n : ℕ} {i : Fin (n+2)} {S : SSet} (σ₁ σ₂ : Λ[n+1, i] ⟶ S)
    (h : ∀ (j) (h : j ≠ i), σ₁.app _ (face i j h) = σ₂.app _ (face i j h)) :
    σ₁ = σ₂

Proof state:
case app.h.op.h.h.intro.intro.intro
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i] ⟶ S
h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op ⦋n⦌) (face i j h) = σ₂.app (op ⦋n⦌) (face i j h)
m : ℕ
f : Λ[n + 1, i] _⦋m⦌
f' : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f' = ↑f
j : Fin (n + 2)
hji : ¬j = i
hfj : ∀ (k : Fin ((unop (op ⦋m⦌)).len + 1)), (Hom.toOrderHom f') k ≠ j
H : f = Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)
H₁ :
  (Λ[n + 1, i].map (factor_δ f' j).op ≫ σ₁.app (op ⦋m⦌)) (face i j hji) =
    (σ₁.app (op ⦋n⦌) ≫ S.map (factor_δ f' j).op) (face i j hji)
⊢ σ₁.app (op ⦋m⦌) f = σ₂.app (op ⦋m⦌) f

Tactic:
have H₂ := congrFun (σ₂.naturality (factor_δ f' j).op) (face i j hji)

Result:
case app.h.op.h.h.intro.intro.intro
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i] ⟶ S
h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op ⦋n⦌) (face i j h) = σ₂.app (op ⦋n⦌) (face i j h)
m : ℕ
f : Λ[n + 1, i] _⦋m⦌
f' : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f' = ↑f
j : Fin (n + 2)
hji : ¬j = i
hfj : ∀ (k : Fin ((unop (op ⦋m⦌)).len + 1)), (Hom.toOrderHom f') k ≠ j
H : f = Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)
H₁ :
  (Λ[n + 1, i].map (factor_δ f' j).op ≫ σ₁.app (op ⦋m⦌)) (face i j hji) =
    (σ₁.app (op ⦋n⦌) ≫ S.map (factor_δ f' j).op) (face i j hji)
H₂ :
  (Λ[n + 1, i].map (factor_δ f' j).op ≫ σ₂.app (op ⦋m⦌)) (face i j hji) =
    (σ₂.app (op ⦋n⦌) ≫ S.map (factor_δ f' j).op) (face i j hji)
⊢ σ₁.app (op ⦋m⦌) f = σ₂.app (op ⦋m⦌) f

Proof state:
case a.a
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i] ⟶ S
h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op ⦋n⦌) (face i j h) = σ₂.app (op ⦋n⦌) (face i j h)
m : ℕ
f : Λ[n + 1, i] _⦋m⦌
f' : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f' = ↑f
j : Fin (n + 2)
hji : ¬j = i
hfj : ∀ (k : Fin ((unop (op ⦋m⦌)).len + 1)), (Hom.toOrderHom f') k ≠ j
⊢ (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)) ((stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f') =
    (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)) ↑(Λ[n + 1, i].map (factor_δ f' j).op (face i j hji))

Tactic:
exact (factor_δ_spec f' j hfj).symm

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i] ⟶ S
h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op ⦋n⦌) (face i j h) = σ₂.app (op ⦋n⦌) (face i j h)
m : ℕ
f : Λ[n + 1, i] _⦋m⦌
f' : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f' = ↑f
⊢ ∃ j, ¬j = i ∧ ∀ (k : Fin ((unop (op ⦋m⦌)).len + 1)), (Hom.toOrderHom f') k ≠ j

Tactic:
obtain ⟨f, hf'⟩ := f

Result:
case mk
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i] ⟶ S
h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op ⦋n⦌) (face i j h) = σ₂.app (op ⦋n⦌) (face i j h)
m : ℕ
f' : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
f : Δ[n + 1] _⦋m⦌
hf' : Set.range ⇑(asOrderHom f) ∪ {i} ≠ Set.univ
hf : (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f' = ↑⟨f, hf'⟩
⊢ ∃ j, ¬j = i ∧ ∀ (k : Fin ((unop (op ⦋m⦌)).len + 1)), (Hom.toOrderHom f') k ≠ j