-- Mathlib/AlgebraicTopology/Quasicategory/Basic.lean
lemma quasicategory_of_filler (S : SSet)
    (filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : Λ[n+2, i] ⟶ S)
      (_h0 : 0 < i) (_hn : i < Fin.last (n+2)),
      ∃ σ : S _⦋n+2⦌, ∀ (j) (h : j ≠ i), S.δ j σ = σ₀.app _ (horn.face i j h)) :
    Quasicategory S where
  hornFilling' n i σ₀ h₀ hₙ

Proof state:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∃ σ, σ₀ = hornInclusion (n + 2) i ≫ σ

Tactic:
obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ

Result:
case intro
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
⊢ ∃ σ, σ₀ = hornInclusion (n + 2) i ≫ σ

Proof state:
case intro.h
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
⊢ ∀ (j : Fin (n + 1 + 2)) (h : j ≠ i),
    σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h) =
      (hornInclusion (n + 2) i ≫ (S.yonedaEquiv ⦋n + 2⦌).symm σ).app (Opposite.op ⦋n + 1⦌) (horn.face i j h)

Tactic:
intro j hj

Result:
case intro.h
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j hj) =
    (hornInclusion (n + 2) i ≫ (S.yonedaEquiv ⦋n + 2⦌).symm σ).app (Opposite.op ⦋n + 1⦌) (horn.face i j hj)

Proof state:
case intro.h
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j hj) =
    (hornInclusion (n + 2) i ≫ (S.yonedaEquiv ⦋n + 2⦌).symm σ).app (Opposite.op ⦋n + 1⦌) (horn.face i j hj)

Tactic:
rw [← h j hj, NatTrans.comp_app]

Result:
case intro.h
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ SimplicialObject.δ S j σ =
    ((hornInclusion (n + 2) i).app (Opposite.op ⦋n + 1⦌) ≫ ((S.yonedaEquiv ⦋n + 2⦌).symm σ).app (Opposite.op ⦋n + 1⦌))
      (horn.face i j hj)

Proof state:
case intro
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
⊢ σ₀ = hornInclusion (n + 2) i ≫ (S.yonedaEquiv ⦋n + 2⦌).symm σ

Tactic:
apply horn.hom_ext

Result:
case intro.h
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
⊢ ∀ (j : Fin (n + 1 + 2)) (h : j ≠ i),
    σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h) =
      (hornInclusion (n + 2) i ≫ (S.yonedaEquiv ⦋n + 2⦌).symm σ).app (Opposite.op ⦋n + 1⦌) (horn.face i j h)

Proof state:
case intro
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
⊢ ∃ σ, σ₀ = hornInclusion (n + 2) i ≫ σ

Tactic:
refine ⟨(S.yonedaEquiv _).symm σ, ?_⟩

Result:
case intro
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
⊢ σ₀ = hornInclusion (n + 2) i ≫ (S.yonedaEquiv ⦋n + 2⦌).symm σ

Proof state:
case intro.h
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i] ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op ⦋n + 1⦌) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ SimplicialObject.δ S j σ =
    ((hornInclusion (n + 2) i).app (Opposite.op ⦋n + 1⦌) ≫ ((S.yonedaEquiv ⦋n + 2⦌).symm σ).app (Opposite.op ⦋n + 1⦌))
      (horn.face i j hj)

Tactic:
rfl

Result:
no goals