awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
rw :
  modelCategoryQuillen.J.rlp.llp =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
rw₁ rw₂ :
  ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
⊢ anodyneExtensions =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
rw [anodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]

Premises used: CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0, SSet.anodyneExtensions_eq_llp_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y : SSet
f : X ⟶ Y
hf : strongAnodyneExtensions f
⊢ Mono f

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
generalize : ∀ (B : X.Subcomplex) (h : range A.ι = B), ∃ (P : B.Pairing), P.IsRegular
⊢ ∃ (P : (range A.ι).Pairing), P.IsRegular

Tactic:
generalize h : Subcomplex.range A.ι = B

Premises used: SSet.Subcomplex.range, SSet.Subcomplex.ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
B : X.Subcomplex
h : range A.ι = B
⊢ B = A

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
B : X.Subcomplex
h : range A.ι = B
obtain : ∀ (P : B.Pairing) [P.IsRegular] (h : range B.ι = B), ∃ (P : B.Pairing), P.IsRegular
⊢ ∃ (P : B.Pairing), P.IsRegular

Tactic:
obtain rfl : B = A := by simpa using h.symm

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
B : X.Subcomplex
P : B.Pairing
inst : P.IsRegular
h : range B.ι = B
⊢ ∃ (P : B.Pairing), P.IsRegular

Tactic:
⟨P, inferInstance⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
B : X.Subcomplex
P : B.Pairing
inst : P.IsRegular
h : range B.ι = B
⊢ ∃ (P : B.Pairing), P.IsRegular

Tactic:
exact ⟨P, inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
hA : strongAnodyneExtensions A.ι
obtain :
  Mono A.ι →
    ∀ (P : (Subcomplex.range A.ι).Pairing), P.IsRegular → ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A
⊢ ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A

Tactic:
obtain ⟨_, P, _⟩ := hA
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
left : Mono A.ι
P : (Subcomplex.range A.ι).Pairing
h : P.IsRegular
⊢ Subcomplex.range A.ι = A

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
left : Mono A.ι
P : (Subcomplex.range A.ι).Pairing
h : P.IsRegular
⊢ ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A

Tactic:
exact ⟨_, P, inferInstance, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
hA : strongAnodyneExtensions A.ι
obtain :
  ∀ (w : X.Subcomplex) (P : w.Pairing),
    P.IsRegular → ∀ (hA : strongAnodyneExtensions w.ι), ∃ (P : w.Pairing), P.IsRegular
⊢ ∃ (P : A.Pairing), P.IsRegular

Tactic:
obtain ⟨_, P, _, rfl⟩ :
        ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A := by
      obtain ⟨_, P, _⟩ := hA
      exact ⟨_, P, inferInstance, by simp⟩

Premises used: SSet.Subcomplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
w : X.Subcomplex
P : w.Pairing
left : P.IsRegular
hA : strongAnodyneExtensions w.ι
⊢ ∃ (P : w.Pairing), P.IsRegular

Tactic:
⟨P, inferInstance⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
w : X.Subcomplex
P : w.Pairing
left : P.IsRegular
hA : strongAnodyneExtensions w.ι
⊢ ∃ (P : w.Pairing), P.IsRegular

Tactic:
exact ⟨P, inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
⊢ SSet.anodyneExtensions (Y :=
    (TransfiniteCompositionOfShape.F
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := P.rankFunction.Cell) (A :=
            fun (j : ℕ) (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) P.rankFunction.relativeCellComplex)).obj
      (Order.succ j))
    ((TransfiniteCompositionOfShape.F
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := P.rankFunction.Cell) (A :=
            fun (j : ℕ) (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) P.rankFunction.relativeCellComplex)).map
      (CategoryTheory.homOfLE ⋯))

Tactic:
(?_ : (_ : MorphismProperty _) ≤ _ ) _
        (P.rankFunction.relativeCellComplex.attachCells j hj).pushouts_coproducts

Premises used: SSet.Subcomplex.Pairing.rankFunction, HomotopicalAlgebra.AttachCells.pushouts_coproducts, SSet.Subcomplex.Pairing.RankFunction.relativeCellComplex, HomotopicalAlgebra.RelativeCellComplex.attachCells
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
refine :
  (coproducts.{u, u, u + 1}
        (ofHoms (X := fun (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) (P.rankFunction.basicCell j))).pushouts ≤
    SSet.anodyneExtensions
⊢ SSet.anodyneExtensions (Y :=
    (TransfiniteCompositionOfShape.F
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := P.rankFunction.Cell) (A :=
            fun (j : ℕ) (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) P.rankFunction.relativeCellComplex)).obj
      (Order.succ j))
    ((TransfiniteCompositionOfShape.F
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := P.rankFunction.Cell) (A :=
            fun (j : ℕ) (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) P.rankFunction.relativeCellComplex)).map
      (CategoryTheory.homOfLE ⋯))

Tactic:
refine (?_ : (_ : MorphismProperty _) ≤ _ ) _
        (P.rankFunction.relativeCellComplex.attachCells j hj).pushouts_coproducts

Premises used: SSet.Subcomplex.Pairing.rankFunction, HomotopicalAlgebra.AttachCells.pushouts_coproducts, SSet.Subcomplex.Pairing.RankFunction.relativeCellComplex, HomotopicalAlgebra.RelativeCellComplex.attachCells
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
simp :
  ofHoms (X := fun (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) (P.rankFunction.basicCell j) ≤ SSet.anodyneExtensions
⊢ (coproducts.{u, u, u + 1}
        (ofHoms (X := fun (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) (P.rankFunction.basicCell j))).pushouts ≤
    SSet.anodyneExtensions

Tactic:
simp only [pushouts_le_iff, coproducts_le_iff]

Premises used: CategoryTheory.MorphismProperty.coproducts_le_iff, CategoryTheory.MorphismProperty.pushouts_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X_1 : SSet
A : X_1.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
⊢ SSet.anodyneExtensions (X := c.horn.toSSet) (P.rankFunction.basicCell j c)

Tactic:
.horn_ι c.index

Premises used: SSet.anodyneExtensions.horn_ι, SSet.Subcomplex.Pairing.RankFunction.Cell.index
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X_1 : SSet
A : X_1.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
⊢ SSet.anodyneExtensions (X := c.horn.toSSet) (P.rankFunction.basicCell j c)

Tactic:
exact .horn_ι c.index
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : X ⟶ Y
h : isomorphisms SSet e
f : Y ⟶ Z
hf : strongAnodyneExtensions f
obtain : Mono f → ∀ (P : (Subcomplex.range f).Pairing) (hP : P.IsRegular), strongAnodyneExtensions (e ≫ f)
⊢ strongAnodyneExtensions (e ≫ f)

Tactic:
obtain ⟨_, P, hP⟩ := hf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : X ⟶ Y
h : isomorphisms SSet e
f : Y ⟶ Z
left : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ strongAnodyneExtensions (e ≫ f)

Tactic:
⟨inferInstance, P.ofIso (Iso.refl _) ?_, inferInstance⟩

Premises used: SSet.Subcomplex.Pairing.ofIso, inferInstance, CategoryTheory.Iso.refl, SSet.strongAnodyneExtensions, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : X ⟶ Y
h : isomorphisms SSet e
f : Y ⟶ Z
left : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
refine : (Subcomplex.range f).preimage (Iso.hom (Iso.refl Z)) = Subcomplex.range (e ≫ f)
⊢ strongAnodyneExtensions (e ≫ f)

Tactic:
refine ⟨inferInstance, P.ofIso (Iso.refl _) ?_, inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : X ⟶ Y
h : isomorphisms SSet e
f : Y ⟶ Z
left : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ (Subcomplex.range f).preimage (Iso.hom (Iso.refl Z)) = Subcomplex.range (e ≫ f)

Tactic:
simp [Subcomplex.range_comp, Subcomplex.range_eq_top e,
      Subcomplex.image_top]

Premises used: SSet.Subcomplex.range_eq_top, SSet.Subcomplex.image_top, SSet.Subcomplex.range_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : Y ⟶ Z
h : isomorphisms SSet e
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ strongAnodyneExtensions (f ≫ e)

Tactic:
⟨inferInstance, P.ofIso (asIso e).symm ?_, inferInstance⟩

Premises used: SSet.Subcomplex.Pairing.ofIso, inferInstance, SSet.strongAnodyneExtensions, And.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : Y ⟶ Z
h : isomorphisms SSet e
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
refine : (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)
⊢ strongAnodyneExtensions (f ≫ e)

Tactic:
refine ⟨inferInstance, P.ofIso (asIso e).symm ?_, inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y Z : SSet
e : Y ⟶ Z
h : isomorphisms SSet e
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)

Tactic:
simp [Subcomplex.preimage_inv, Subcomplex.range_comp]

Premises used: SSet.Subcomplex.preimage_inv, SSet.Subcomplex.range_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y : SSet
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
h : P.IsRegular
rw : anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
⊢ anodyneExtensions f

Tactic:
rw [← Subfunctor.toRange_ι f]

Premises used: CategoryTheory.Subfunctor.toRange_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y : SSet
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
h : P.IsRegular
⊢ anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)

Tactic:
comp_mem _ _ _ (.of_isIso _) P.anodyneExtensions

Premises used: SSet.Subcomplex.Pairing.anodyneExtensions, CategoryTheory.MorphismProperty.comp_mem, SSet.anodyneExtensions.of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y : SSet
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
h : P.IsRegular
⊢ anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)

Tactic:
exact comp_mem _ _ _ (.of_isIso _) P.anodyneExtensions

Premises used: SSet.Subcomplex.Pairing.anodyneExtensions, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
⊢ innerAnodyneExtensions f

Tactic:
MorphismProperty.of_isIso innerAnodyneExtensions f

Premises used: CategoryTheory.MorphismProperty.of_isIso, SSet.innerAnodyneExtensions
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
⊢ innerAnodyneExtensions = innerHornInclusions.rlp.llp

Tactic:
rfl

Premises used: SSet.innerAnodyneExtensions, SSet.innerFibrations, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι

Tactic:
le_llp_rlp _ _ (horn_ι_mem_innerHornInclusions h0 hn)

Premises used: CategoryTheory.MorphismProperty.le_llp_rlp, SSet.horn_ι_mem_innerHornInclusions
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι

Tactic:
exact le_llp_rlp _ _ (horn_ι_mem_innerHornInclusions h0 hn)

Premises used: CategoryTheory.MorphismProperty.le_llp_rlp, SSet.horn_ι_mem_innerHornInclusions
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
rw : modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp
⊢ innerAnodyneExtensions ≤ anodyneExtensions

Tactic:
rw [anodyneExtensions_eq_llp_rlp, innerAnodyneExtensions_eq_llp_rlp, le_llp_iff_le_rlp,
    rlp_llp_rlp]

Premises used: CategoryTheory.MorphismProperty.le_llp_iff_le_rlp, CategoryTheory.MorphismProperty.rlp_llp_rlp, SSet.innerAnodyneExtensions_eq_llp_rlp, SSet.anodyneExtensions_eq_llp_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp

Tactic:
antitone_rlp innerHornInclusions_le_J

Premises used: SSet.innerHornInclusions_le_J, CategoryTheory.MorphismProperty.antitone_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp

Tactic:
exact antitone_rlp innerHornInclusions_le_J

Premises used: SSet.innerHornInclusions_le_J, CategoryTheory.MorphismProperty.antitone_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
rw :
  IsSmall.{u, u, u + 1} (C := SSet)
    (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
⊢ IsSmall.{u, u, u + 1} innerHornInclusions

Tactic:
rw [innerHornInclusions_eq_iSup]

Premises used: SSet.innerHornInclusions_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
⊢ ∀ (n : ℕ),
    IsSmall.{u, u, u + 1} (C := SSet)
      (ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)

Tactic:
have (n : ℕ) : MorphismProperty.IsSmall.{u}
    (MorphismProperty.ofHoms.{u}
      fun p : {p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2)} ↦ Λ[n + 2, p].ι) :=
    isSmall_ofHoms ..
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
this :
  ∀ (n : ℕ),
    IsSmall.{u, u, u + 1} (C := SSet)
      (ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
⊢ IsSmall.{u, u, u + 1} (C := SSet)
    (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)

Tactic:
isSmall_iSup _

Premises used: CategoryTheory.MorphismProperty.isSmall_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
this :
  ∀ (n : ℕ),
    IsSmall.{u, u, u + 1} (C := SSet)
      (ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
⊢ IsSmall.{u, u, u + 1} (C := SSet)
    (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)

Tactic:
exact isSmall_iSup _

Premises used: CategoryTheory.MorphismProperty.isSmall_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
hi : innerHornInclusions i
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑innerHornInclusions.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ innerHornInclusions.homFamily) f
⊢ ∃ (i_1 : ℕ),
    ofHoms (X := fun (p : { p : Fin (i_1 + 3) // 0 < p ∧ p < Fin.last (i_1 + 2) }) ↦
      Λ[i_1 + 2, (↑p : Fin (i_1 + 3))].toSSet) (Y := fun (p : { p : Fin (i_1 + 3) // 0 < p ∧ p < Fin.last (i_1 + 2) }) ↦
      Δ[i_1 + 2])
      (fun (p : { p : Fin (i_1 + 3) // 0 < p ∧ p < Fin.last (i_1 + 2) }) ↦ Λ[i_1 + 2, (↑p : Fin (i_1 + 3))].ι) i

Tactic:
simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi

Premises used: CategoryTheory.MorphismProperty.iSup_iff, SSet.innerHornInclusions_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑innerHornInclusions.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ innerHornInclusions.homFamily) f
hi :
  ∃ (i_1 : ℕ),
    ofHoms (X := fun (p : { p : Fin (i_1 + 3) // 0 < p ∧ p < Fin.last (i_1 + 2) }) ↦
      Λ[i_1 + 2, (↑p : Fin (i_1 + 3))].toSSet) (Y := fun (p : { p : Fin (i_1 + 3) // 0 < p ∧ p < Fin.last (i_1 + 2) }) ↦
      Δ[i_1 + 2])
      (fun (p : { p : Fin (i_1 + 3) // 0 < p ∧ p < Fin.last (i_1 + 2) }) ↦ Λ[i_1 + 2, (↑p : Fin (i_1 + 3))].ι) i
obtain :
  ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }),
    IsFinitelyPresentable Λ[n + 2, (↑i : Fin (n + 3))].toSSet
⊢ IsFinitelyPresentable A

Tactic:
obtain ⟨n, ⟨i⟩⟩ := hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
X_1 Y_1 : SSet
f : X_1 ⟶ Y_1
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑innerHornInclusions.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ innerHornInclusions.homFamily) f
n : ℕ
X Y : SSet
i : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }
⊢ IsFinitelyPresentable Λ[n + 2, (↑i : Fin (n + 3))].toSSet

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
hi : innerHornInclusions i
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑innerHornInclusions.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑innerHornInclusions.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ innerHornInclusions.homFamily) f
⊢ IsFinitelyPresentable A

Tactic:
have : IsFinitelyPresentable.{u} A := by
      simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
rw :
  innerHornInclusions.rlp.llp =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts
rw₁ rw₂ :
  (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts
⊢ innerAnodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts

Tactic:
rw [innerAnodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]

Premises used: CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument, SSet.innerAnodyneExtensions_eq_llp_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Goal:
rw :
  innerHornInclusions.rlp.llp =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
rw₁ rw₂ :
  ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
⊢ innerAnodyneExtensions =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
rw [innerAnodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]

Premises used: SSet.innerAnodyneExtensions_eq_llp_rlp, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
mp :
  { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } →
    ∃! i : Fin (d + 2),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
            (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
          y =
        x
mpr :
  (∃! i : Fin (d + 2),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
            (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
          y =
        x) →
    { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } ↔
    ∃! i : Fin (d + 2),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
            (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
          y =
        x

Tactic:
constructor