awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
⊢ Factors (X :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)))
    (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌))

Tactic:
(finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_

Premises used: Iff.mpr, CategoryTheory.Subobject.arrow, Finset.univ, Fin.succ, CategoryTheory.Limits.kernelSubobject_factors, CategoryTheory.Subobject.finset_inf_factors, HAdd.hAdd, SimplexCategory.mk, Opposite.op, CategoryTheory.CategoryStruct.comp, CategoryTheory.SimplicialObject.δ, Finset.inf, OfNat.ofNat, CategoryTheory.NatTrans.app, CategoryTheory.Limits.kernelSubobject
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
succ :
  ∀ (i : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
      Eq (α :=
        Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
            (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
          Y _⦋n⦌)
        ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌)) ≫
          Y.δ i.succ)
        0
⊢ Factors (X :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)))
    (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌))

Tactic:
refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_

Premises used: Iff.mpr, CategoryTheory.Limits.kernelSubobject_factors, CategoryTheory.Subobject.finset_inf_factors
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
succ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌)) ≫
      Y.δ i.succ)
    0

Tactic:
rw [Category.assoc, SimplicialObject.δ, ← f.naturality,
          ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
          Category.assoc]

Premises used: CategoryTheory.Category.assoc, Finset.univ, CategoryTheory.NatTrans.naturality, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.SimplicialObject.δ, CategoryTheory.Subobject.finset_inf_arrow_factors
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
succ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.δ i.succ ≫ f.app (op ⦋n⦌))
    0
succ₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0 ≫ f.app (op ⦋n⦌))
    0
succ₂ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0)
    0
succ₃ succ₄ :
  Eq.{v_1 + 1} (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    0 0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
    0

Tactic:
rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Premises used: CategoryTheory.SimplicialObject.δ_def, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
zero :
  Eq (α := HomologicalComplex.X (obj X) (HAdd.hAdd (α := ℕ) 0 1) ⟶ HomologicalComplex.X (obj Y) 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (HAdd.hAdd (α := ℕ) 0 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.d (obj Y) (HAdd.hAdd (α := ℕ) 0 1) 0))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) 0) (HomologicalComplex.d (obj X) (HAdd.hAdd (α := ℕ) 0 1) 0)
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) 0))
succ :
  ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (obj X) (n + 1 + 1) ⟶ HomologicalComplex.X (obj Y) (n + 1))
      (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1 + 1))
        ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1 + 1))
        (HomologicalComplex.d (obj Y) (n + 1 + 1) (n + 1)))
      (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) (n + 1))
        (HomologicalComplex.d (obj X) (n + 1 + 1) (n + 1))
        ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1)))
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1) ⟶ HomologicalComplex.X (obj Y) n)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1))
      (HomologicalComplex.d (obj Y) (n + 1) n))
    (HomologicalComplex.d (obj X) (n + 1) n ≫
      (fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) n)

Tactic:
cases n
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
zero :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (Y.δ k.succ))
          (arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋1⦌)) ⋯ ≫
        𝟙
            (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋1⦌)) underlying
              (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (Y.δ k.succ))) ≫
          arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (Y.δ k.succ)) ≫ Y.δ 0 ≫ inv (arrow ⊤) :
      Quiver.Hom.{v_1, u_1} (V := C)
        (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
          (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
        (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤))
    (CategoryStruct.comp (Y := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤)
        (𝟙
              (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
                (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))) ≫
            arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤) :
          Quiver.Hom.{v_1, u_1} (V := C)
            (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
              (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
            (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
        (factorThru ⊤ (arrow ⊤ ≫ f.app (op ⦋0⦌)) ⋯ :
          Quiver.Hom.{v_1, u_1} (V := C) (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤)
            (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤)) :
      Quiver.Hom.{v_1, u_1} (V := C)
        (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
          (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
        (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤))
⊢ Eq (α := HomologicalComplex.X (obj X) (HAdd.hAdd (α := ℕ) 0 1) ⟶ HomologicalComplex.X (obj Y) 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (HAdd.hAdd (α := ℕ) 0 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.d (obj Y) (HAdd.hAdd (α := ℕ) 0 1) 0))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) 0) (HomologicalComplex.d (obj X) (HAdd.hAdd (α := ℕ) 0 1) 0)
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) 0))

Tactic:
dsimp [objD, objX, ChainComplex.of.d]

Premises used: ChainComplex.of.d, AlgebraicTopology.NormalizedMooreComplex.objX, AlgebraicTopology.NormalizedMooreComplex.objD
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
succ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (Y.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫
          f.app (op ⦋n + 1 + 1⦌))
        ⋯ ≫
      if n + 1 + 1 = n + 1 + 1 then
        𝟙
            (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋n + 1 + 1⦌)) underlying
              (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (Y.δ k.succ))) ≫
          factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
            (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (Y.δ k.succ)) ≫ Y.δ 0) ⋯
      else 0)
    ((if n + 1 + 1 = n + 1 + 1 then
        𝟙
            (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
              (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ≫
          factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
            (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯
      else 0) ≫
      factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌)) ⋯)
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1 + 1) ⟶ HomologicalComplex.X (obj Y) (n + 1))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1 + 1))
      (HomologicalComplex.d (obj Y) (n + 1 + 1) (n + 1)))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) (n + 1)) (HomologicalComplex.d (obj X) (n + 1 + 1) (n + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1)))

Tactic:
dsimp [objD, objX, ChainComplex.of.d]

Premises used: ChainComplex.of.d, AlgebraicTopology.NormalizedMooreComplex.objX, AlgebraicTopology.NormalizedMooreComplex.objD
-- Module: Mathlib.AlgebraicTopology.MooreComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (normalizedMooreComplex C) X) (n + 1) ⟶
      HomologicalComplex.X (Functor.obj (normalizedMooreComplex C) X) n)
    (HomologicalComplex.d (Functor.obj (normalizedMooreComplex C) X) (n + 1) n) (objD X n)

Tactic:
simp [-objD, -obj_X]

Premises used: AlgebraicTopology.NormalizedMooreComplex.obj_X, AlgebraicTopology.NormalizedMooreComplex.objD
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
inst : S.Quasicategory
n : ℕ
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h0 : 0 < i
hn : i < Fin.last 0
σ₀ : Λ[0, i].toSSet ⟶ S
⊢ ∃ (σ : Δ[0] ⟶ S), σ₀ = Λ[0, i].ι ≫ σ

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
inst : S.Quasicategory
n : ℕ
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h0 : 0 < i
hn : i < Fin.last 1
σ₀ : Λ[1, i].toSSet ⟶ S
⊢ ∃ (σ : Δ[1] ⟶ S), σ₀ = Λ[1, i].ι ≫ σ

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
inst : S.Quasicategory
n_1 n : ℕ
i : Fin (n + 2 + 1)
h0 : 0 < i
hn : i < Fin.last (n + 2)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
Quasicategory.hornFilling' σ₀ h0 hn

Premises used: SSet.Quasicategory.hornFilling'
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
inst : S.Quasicategory
n_1 n : ℕ
i : Fin (n + 2 + 1)
h0 : 0 < i
hn : i < Fin.last (n + 2)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
exact Quasicategory.hornFilling' σ₀ h0 hn

Premises used: SSet.Quasicategory.hornFilling'
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
inst : S.Quasicategory
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
σ₀ : Λ[n, i].toSSet ⟶ S
⊢ ∃ (σ : Δ[n] ⟶ S), σ₀ = Λ[n, i].ι ≫ σ

Tactic:
match n with
  | 0
  | 1 => lia
  | n + 2 => exact Quasicategory.hornFilling' σ₀ h0 hn
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
obtain :
  ∀ (σ : S _⦋n + 2⦌)
    (h :
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))),
    ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          σ :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
⟨yonedaEquiv.symm σ, ?_⟩

Premises used: SSet.yonedaEquiv, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          σ :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
refine : σ₀ = Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
refine ⟨yonedaEquiv.symm σ, ?_⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          σ :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
h₁ :
  ∀ (j : Fin (n + 1 + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ)
                (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
⊢ σ₀ = Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ

Tactic:
apply horn.hom_ext

Premises used: SSet.horn.hom_ext