awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X Y Z : SSet
e : X ⟶ Y
h : isomorphisms SSet e
f : Y ⟶ Z
hf : strongAnodyneExtensions f
⊢ strongAnodyneExtensions (e ≫ f)
have obtain : Mono f → ∀ (P : (Subcomplex.range f).Pairing) (hP : P.IsRegular), strongAnodyneExtensions (e ≫ f)
Tactic: obtain ⟨_, P, hP⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
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)
have refine : (Subcomplex.range f).preimage (Iso.hom (Iso.refl Z)) = Subcomplex.range (e ≫ f)
Tactic: refine ⟨inferInstance, P.ofIso (Iso.refl _) ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
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)
have refine : (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)
Tactic: refine ⟨inferInstance, P.ofIso (asIso e).symm ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X Y : SSet
f : X ⟶ Y
left : Mono f
P : (Subcomplex.range f).Pairing
h : P.IsRegular
⊢ anodyneExtensions f
have rw : anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Tactic: rw [← Subfunctor.toRange_ι f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
Goal:
⊢ innerAnodyneExtensions ≤ anodyneExtensions
have rw : modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp
Tactic: rw [anodyneExtensions_eq_llp_rlp, innerAnodyneExtensions_eq_llp_rlp, le_llp_iff_le_rlp,
    rlp_llp_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
Goal:
⊢ IsSmall.{u, u, u + 1} innerHornInclusions
have 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))].ι)
Tactic: rw [innerHornInclusions_eq_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (hypothesis)
Goal:
⊢ 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))].ι)
have 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))].ι)
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 ..
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (hypothesis)
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
have 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
Tactic: simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
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
⊢ IsFinitelyPresentable A
have 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
Tactic: obtain ⟨n, ⟨i⟩⟩ := hi
Cleared hypotheses: A, B, i, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (hypothesis)
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
⊢ Limits.PreservesColimit
    hf.toTransfiniteCompositionOfShape (α := fun (x : Cardinal.aleph0.ord.ToType) ↦
        (↑innerHornInclusions.toSet : Type (u + 1))).F
    (Functor.obj coyoneda (Opposite.op A))
have this : IsFinitelyPresentable A
Tactic: have : IsFinitelyPresentable.{u} A := by
      simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
Goal:
⊢ innerAnodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts
have rw : innerHornInclusions.rlp.llp =
  (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts
Tactic: rw [innerAnodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
Goal:
rw :
  innerHornInclusions.rlp.llp =
    (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
have 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
Tactic: rw [innerAnodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
Goal:
⊢ innerAnodyneExtensions =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
have rw : innerHornInclusions.rlp.llp =
  ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Tactic: rw [innerAnodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic (goal)
Goal:
rw :
  innerHornInclusions.rlp.llp =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
⊢ innerAnodyneExtensions =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
have rw₁ : ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
  ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Tactic: rw [innerAnodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ { 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
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
⊢ { 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
have 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 }
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left : { dim := d + 1, simplex := y : X.S }.dim = { dim := d, simplex := x : X.S }.dim + 1
f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
    (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
          Mono f ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                    (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                { dim := d + 1, simplex := y : X.S }.simplex =
              { dim := d, simplex := x : X.S }.simplex)
        y_1 →
      y_1 = f
left_1 : Mono f
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
⊢ ∃! 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
have mp : ∀ (i : Fin ({ dim := d, simplex := x : X.S }.dim + 2))
  (h₂ :
    ∀ (y_1 : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
      (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
            Mono f ∧
              (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                      (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                  { dim := d + 1, simplex := y : X.S }.simplex =
                { dim := d, simplex := x : X.S }.simplex)
          y_1 →
        y_1 = SimplexCategory.δ i),
  Mono (SimplexCategory.δ i) →
    ∀
      (h₁ :
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ i).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d + 1, simplex := y : X.S }.simplex =
          { dim := d, simplex := x : X.S }.simplex),
      ∃! 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: obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f
Cleared hypotheses: f, h₂, left_1, h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (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
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (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)
        y_1 →
      y_1 = i
⊢ { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
have mpr : ∀ (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
  (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
        Mono f ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                  (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
              { dim := d + 1, simplex := y : X.S }.simplex =
            { dim := d, simplex := x : X.S }.simplex)
      f →
    ∀ (h₃ : Mono f)
      (h₄ :
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d + 1, simplex := y : X.S }.simplex =
          { dim := d, simplex := x : X.S }.simplex),
      f = SimplexCategory.δ i
Tactic: refine ⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (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
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (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)
        y_1 →
      y_1 = i
f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌
h :
  (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
      Mono f ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d + 1, simplex := y : X.S }.simplex =
          { dim := d, simplex := x : X.S }.simplex)
    f
h₃ : Mono f
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
⊢ f = SimplexCategory.δ i
have mpr : ∀ (j : Fin ({ dim := d, simplex := x : X.S }.dim + 2)),
  Mono (SimplexCategory.δ j) ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
          { dim := d + 1, simplex := y : X.S }.simplex =
        { dim := d, simplex := x : X.S }.simplex →
    ∀ (h₃ : Mono (SimplexCategory.δ j))
      (h₄ :
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d + 1, simplex := y : X.S }.simplex =
          { dim := d, simplex := x : X.S }.simplex),
      SimplexCategory.δ j = SimplexCategory.δ i
Tactic: obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f
Cleared hypotheses: f, h, h₃, h₄
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (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
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (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)
        y_1 →
      y_1 = i
j : Fin ({ dim := d, simplex := x : X.S }.dim + 2)
h :
  Mono (SimplexCategory.δ j) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex =
      { dim := d, simplex := x : X.S }.simplex
h₃ : Mono (SimplexCategory.δ j)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
⊢ SimplexCategory.δ j = SimplexCategory.δ i
have mpr : ∀
  (h₁ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
          (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        y =
      x)
  (h₂ :
    ∀ (y_1 : Fin (d + 2)),
      (fun (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)
          y_1 →
        y_1 = j),
  SimplexCategory.δ j = SimplexCategory.δ j
Tactic: obtain rfl : j = i := h₂ _ h₄
Cleared hypotheses: i, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ y.dim = d + 1
have rw : x.dim + 1 = d + 1
Tactic: rw [hxy.dim_eq, hd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
rw : x.dim + 1 = d + 1
⊢ y.dim = d + 1
have rw₁ : d + 1 = d + 1
Tactic: rw [hxy.dim_eq, hd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ y.dim = d + 1
have rw : x.dim + 1 = d + 1
Tactic: rw [hxy.dim_eq, hd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
rw : x.dim + 1 = d + 1
⊢ y.dim = d + 1
have rw₁ : d + 1 = d + 1
Tactic: rw [hxy.dim_eq, hd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (hypothesis)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ x ≤ y
have this : (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index sorry)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋x.dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
    (y.cast sorry).simplex =
  (x.cast sorry).simplex
Tactic: have := hxy.δ_index rfl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
      (y.cast ⋯).simplex =
    x.simplex
⊢ x ≤ y
have rw : Membership.mem (α := X _⦋x.dim⦌) (γ := Set (X _⦋x.dim⦌)) ((y.cast sorry).subcomplex.obj (Opposite.op ⦋x.dim⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index sorry)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
      (y.cast sorry).simplex :
    X _⦋x.dim⦌)
Tactic: rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff,
    ← this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
⊢ y.dim = d + 1
have rw : x.dim + 1 = d + 1
Tactic: rw [hxy.dim_eq, hd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
rw : x.dim + 1 = d + 1
⊢ y.dim = d + 1
have rw₁ : d + 1 = d + 1
Tactic: rw [hxy.dim_eq, hd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex
⊢ Mono (SimplexCategory.δ (hxy.index hd))
have dsimp : Mono (SimplexCategory.δ (hxy.index hd))
Tactic: dsimp