-- 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
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⦌)

Tactic:
intro m

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

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

Tactic:
obtain ⟨j, hji, hfj⟩ : ∃ j, ¬j = i ∧ ∀ k, f'.toOrderHom k ≠ j := by
  obtain ⟨f, hf'⟩ := f
  subst hf
  simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, not_or] using hf'

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

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₁ :
  σ₁.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

Tactic:
rw [H, H₁, H₂, h _ hji]

Result:
no goals

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

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 : 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 Subtype.ext

Result:
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))

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)
⊢ σ₁ = σ₂

Tactic:
apply NatTrans.ext

Result:
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

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

Tactic:
rw [← hf]

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⦌)) ((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))

Proof state:
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

Tactic:
obtain ⟨f', hf⟩ := (stdSimplex.objEquiv _ _).symm.surjective f.1

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

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⦌
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

Tactic:
subst hf

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⦌
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