-- 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)
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:
dsimp at H₁ H₂

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₁ :
  σ₁.app (op ⦋m⦌) (Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)) =
    S.map (factor_δ f' j).op (σ₁.app (op ⦋n⦌) (face i j hji))
H₂ :
  σ₂.app (op ⦋m⦌) (Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)) =
    S.map (factor_δ f' j).op (σ₂.app (op ⦋n⦌) (face i j hji))
⊢ σ₁.app (op ⦋m⦌) f = σ₂.app (op ⦋m⦌) f

Proof state:
case app.h.op
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)
⊢ ∀ (unop : SimplexCategory), σ₁.app (op unop) = σ₂.app (op unop)

Tactic:
apply SimplexCategory.rec

Result:
case app.h.op.h
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)
⊢ ∀ (n_1 : ℕ), σ₁.app (op ⦋n_1⦌) = σ₂.app (op ⦋n_1⦌)

Proof state:
case app.h
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)
⊢ ∀ (x : SimplexCategoryᵒᵖ), σ₁.app x = σ₂.app x

Tactic:
apply Opposite.rec

Result:
case app.h.op
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)
⊢ ∀ (unop : SimplexCategory), σ₁.app (op unop) = σ₂.app (op unop)

Proof state:
case app
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)
⊢ σ₁.app = σ₂.app

Tactic:
apply funext

Result:
case app.h
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)
⊢ ∀ (x : SimplexCategoryᵒᵖ), σ₁.app x = σ₂.app x

Proof state:
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⦌
hf' : Set.range ⇑(asOrderHom ((stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)).symm f')) ∪ {i} ≠ Set.univ
⊢ ∃ j, ¬j = i ∧ ∀ (k : Fin ((unop (op ⦋m⦌)).len + 1)), (Hom.toOrderHom f') k ≠ j

Tactic:
simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, not_or] using hf'

Result:
no goals

Proof state:
case app.h.op.h
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 : ℕ
⊢ σ₁.app (op ⦋m⦌) = σ₂.app (op ⦋m⦌)

Tactic:
ext f

Result:
case app.h.op.h.h
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⦌
⊢ σ₁.app (op ⦋m⦌) f = σ₂.app (op ⦋m⦌) f

Proof state:
case 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
⊢ ↑f = ↑(Λ[n + 1, i].map (factor_δ f' j).op (face i j hji))

Tactic:
apply (stdSimplex.objEquiv _ _).injective

Result:
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⦌)) ↑f =
    (stdSimplex.objEquiv ⦋n + 1⦌ (op ⦋m⦌)) ↑(Λ[n + 1, i].map (factor_δ f' j).op (face i j hji))

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
⊢ σ₁.app (op ⦋m⦌) f = σ₂.app (op ⦋m⦌) f

Tactic:
have H : f = (Λ[n+1, i].map (factor_δ f' j).op) (face i j hji) := by
  apply Subtype.ext
  apply (stdSimplex.objEquiv _ _).injective
  rw [← hf]
  exact (factor_δ_spec f' j hfj).symm

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)
⊢ σ₁.app (op ⦋m⦌) f = σ₂.app (op ⦋m⦌) f