awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ (f.filtration (Order.succ j)).obj d
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
      (Set.range (ι := (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (homOfLE ⋯) d)) :
            (a : (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d)) →
              (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)) ⊔
        Set.range (ι := (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d)) :
            (a : (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d)) →
              (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
      (Subtype.mk (p := fun (x : X.obj d) ↦ x ∈ (f.filtration (Order.succ j)).obj d) x hx) ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d))) Set.univ
      (Subtype.mk (p := fun (x : X.obj d) ↦ x ∈ (f.filtration (Order.succ j)).obj d) x hx)
have h : ∀
  (hx :
    x ∈ A.obj d ∨
      ∃ i ≤ j,
        ∃ (i_1 : f.Cell i),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
              d)
            x),
  (x ∈ A.obj d ∨
      ∃ i < j,
        ∃ (i_1 : f.Cell i),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
              d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex j).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d) :
                (a : (f.sigmaStdSimplex j).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j_1 : ι),
                              ⨆ (_ : j_1 < Order.succ j),
                                ⨆ (c : f.Cell j_1),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
Tactic: simp only [filtration_def, Order.lt_succ_iff, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, exists_prop, Subfunctor.toFunctor_obj, Subfunctor.homOfLe_app,
    TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, Set.sup_eq_union, Set.mem_range, Subtype.ext_iff,
    Subtype.exists, exists_eq_right, Set.mem_univ, iff_true] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx :
  x ∈ A.obj d ∨
    ∃ i ≤ j,
      ∃ (i_1 : f.Cell i),
        Membership.mem (γ := Set (X.obj d))
          (Subfunctor.obj
            (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N)))) d)
          x
⊢ (x ∈ A.obj d ∨
      ∃ i < j,
        ∃ (i_1 : f.Cell i),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
              d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex j).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d) :
                (a : (f.sigmaStdSimplex j).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j_1 : ι),
                              ⨆ (_ : j_1 < Order.succ j),
                                ⨆ (c : f.Cell j_1),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
have h : ∀ (hx : x ∈ A.obj d),
  (x ∈ A.obj d ∨
      ∃ i < j,
        ∃ (i_1 : f.Cell i),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
              d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex j).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d) :
                (a : (f.sigmaStdSimplex j).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j_1 : ι),
                              ⨆ (_ : j_1 < Order.succ j),
                                ⨆ (c : f.Cell j_1),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
Tactic: obtain hx | ⟨i, hi, c, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi : i ≤ j
c : f.Cell i
hx :
  Membership.mem (γ := Set (X.obj d))
    (Subfunctor.obj
      (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))) d)
    x
⊢ (x ∈ A.obj d ∨
      ∃ i < j,
        ∃ (i_1 : f.Cell i),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
              d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex j).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d) :
                (a : (f.sigmaStdSimplex j).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j_1 : ι),
                              ⨆ (_ : j_1 < Order.succ j),
                                ⨆ (c : f.Cell j_1),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
have h : ∀ (hi : i < j),
  (x ∈ A.obj d ∨
      ∃ i < j,
        ∃ (i_1 : f.Cell i),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
              d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex j).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d) :
                (a : (f.sigmaStdSimplex j).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j_1 : ι),
                              ⨆ (_ : j_1 < Order.succ j),
                                ⨆ (c : f.Cell j_1),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
Tactic: obtain hi | rfl := hi.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx :
  Membership.mem (γ := Set (X.obj d))
    (Subfunctor.obj
      (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))) d)
    x
hi : i ≤ i
⊢ (x ∈ A.obj d ∨
      ∃ i_1 < i,
        ∃ (i : f.Cell i_1),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i.s) : A.N)))) d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex i).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b i) d) :
                (a : (f.sigmaStdSimplex i).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j : ι),
                              ⨆ (_ : j < Order.succ i),
                                ⨆ (c : f.Cell j),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
have hx₁ : x ∈ (range (c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι)).obj d
Tactic: rw [← c.range_map, ← c.mapToSucc_ι, ← c.ι_b_assoc] at hx
Cleared hypotheses: hx, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (range (c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι)).obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨
      ∃ i_1 < i,
        ∃ (i : f.Cell i_1),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i.s) : A.N)))) d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex i).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b i) d) :
                (a : (f.sigmaStdSimplex i).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j : ι),
                              ⨆ (_ : j < Order.succ i),
                                ⨆ (c : f.Cell j),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
have h : ∀ (y : Δ[c.dim + 1].obj d)
  (hy :
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι).app d) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1].obj d)) → (fun (X : Type u) ↦ X) (X.obj d))
        y =
      x),
  (x ∈ A.obj d ∨
      ∃ i_1 < i,
        ∃ (i : f.Cell i_1),
          Membership.mem (γ := Set (X.obj d))
            (Subfunctor.obj
              (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i.s) : A.N)))) d)
            x) ∨
    ∃ (y : (f.sigmaStdSimplex i).obj d),
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b i) d) :
                (a : (f.sigmaStdSimplex i).obj d) →
                  (↑(A.obj d ∪
                        (⨆ (j : ι),
                              ⨆ (_ : j < Order.succ i),
                                ⨆ (c : f.Cell j),
                                  (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                          d) :
                    Type u))
              y) :
          X.obj d) =
        x
Tactic: obtain ⟨y, hy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ Eq.{u + 1} (α := X.S)
    (S.mk (dim := c.dim + 1)
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋c.dim + 1⦌)) :
              (a : f.sigmaStdSimplex j _⦋c.dim + 1⦌) → (f.filtration (Order.succ j)).toSSet _⦋c.dim + 1⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)) :
                (a : Δ[c.dim + 1] _⦋c.dim + 1⦌) → f.sigmaStdSimplex j _⦋c.dim + 1⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim + 1⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
                  (𝟙 ⦋c.dim + 1⦌) :
                Δ[c.dim + 1] _⦋c.dim + 1⦌))) :
        X _⦋c.dim + 1⦌))
    (S.mk (dim :=
      S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))))
have rw : S.mk (dim := c.dim + 1)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋c.dim + 1⦌)) :
            (a : f.sigmaStdSimplex j _⦋c.dim + 1⦌) → (f.filtration (Order.succ j)).toSSet _⦋c.dim + 1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)) :
              (a : Δ[c.dim + 1] _⦋c.dim + 1⦌) → f.sigmaStdSimplex j _⦋c.dim + 1⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim + 1⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
                (𝟙 ⦋c.dim + 1⦌) :
              Δ[c.dim + 1] _⦋c.dim + 1⦌))) :
      X _⦋c.dim + 1⦌) =
  { dim := ((↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).cast sorry).dim,
    simplex :=
      (S.cast (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) sorry).simplex :
    X.S }
Tactic: rw [← S.cast_eq_self _ (P.dim_p c.s)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ S.mk (dim := c.dim + 1)
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋c.dim + 1⦌)) :
              (a : f.sigmaStdSimplex j _⦋c.dim + 1⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋c.dim + 1⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)) :
                (a : Δ[c.dim + 1] _⦋c.dim + 1⦌) → f.sigmaStdSimplex j _⦋c.dim + 1⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim + 1⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
                  (𝟙 ⦋c.dim + 1⦌) :
                Δ[c.dim + 1] _⦋c.dim + 1⦌))) :
        X _⦋c.dim + 1⦌) =
    { dim := (↑c.s : A.N).dim + 1,
      simplex :=
        (S.cast (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ⋯).simplex :
      X.S }
have rw : (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app c.mapToSucc (op ⦋c.dim + 1⦌)) :
          (a : Δ[c.dim + 1] _⦋c.dim + 1⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋c.dim + 1⦌)) : Type u))
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim + 1⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
          (𝟙 ⦋c.dim + 1⦌))) :
    X _⦋c.dim + 1⦌) =
  (S.cast (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) sorry).simplex
Tactic: rw [S.ext_iff, c.ι_b_app_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₂ f c) = { dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex }
have dsimp : S.mk (dim := c.dim)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋c.dim⦌)) :
            (a : f.sigmaStdSimplex j _⦋c.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋c.dim⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)) :
              (a : Δ[c.dim + 1] _⦋c.dim⦌) → f.sigmaStdSimplex j _⦋c.dim⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
                (SimplexCategory.δ c.index) :
              Δ[c.dim + 1] _⦋c.dim⦌))) :
      X _⦋c.dim⦌) =
  { dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex : X.S }
Tactic: dsimp [mapN]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ S.mk (dim := c.dim)
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋c.dim⦌)) :
              (a : f.sigmaStdSimplex j _⦋c.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋c.dim⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)) :
                (a : Δ[c.dim + 1] _⦋c.dim⦌) → f.sigmaStdSimplex j _⦋c.dim⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
                  (SimplexCategory.δ c.index) :
                Δ[c.dim + 1] _⦋c.dim⦌))) :
        X _⦋c.dim⦌) =
    { dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex : X.S }
have rw : (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (lift c.map sorry) (op ⦋c.dim⦌)) :
          (a : Δ[c.dim + 1] _⦋c.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋c.dim⦌)) : Type u))
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
          (SimplexCategory.δ c.index))) :
    X _⦋c.dim⦌) =
  (↑c.s : A.N).simplex
Tactic: rw [S.ext_iff, c.ι_b_app_apply, Cell.mapToSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) : (a : Δ[c.dim + 1] _⦋c.dim⦌) → X _⦋c.dim⦌)
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋c.dim⦌ ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
          (SimplexCategory.δ c.index) :
        Δ[c.dim + 1] _⦋c.dim⦌) =
    (↑c.s : A.N).simplex
have rw : (↑c.s : A.N).simplex = (↑c.s : A.N).simplex
Tactic: rw [Cell.map_app_objEquiv_symm_δ_index]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
s : (range (X := f.sigmaHorn j) (f.m j)).N
⊢ Membership.mem (γ := Set (X _⦋(f.mapN s).dim⦌)) (X.nonDegenerate (f.mapN s).dim) (f.mapN s).simplex
have inl : ∀ (c : f.Cell j),
  Membership.mem (γ := Set (X _⦋(f.mapN (Cell.type₁ f c)).dim⦌)) (X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim)
    (f.mapN (Cell.type₁ f c)).simplex
Tactic: obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
s : (range (X := f.sigmaHorn j) (f.m j)).N
inl :
  ∀ (c : f.Cell j),
    Membership.mem (γ := Set (X _⦋(f.mapN (Cell.type₁ f c)).dim⦌)) (X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim)
      (f.mapN (Cell.type₁ f c)).simplex
⊢ Membership.mem (γ := Set (X _⦋(f.mapN s).dim⦌)) (X.nonDegenerate (f.mapN s).dim) (f.mapN s).simplex
have inr : ∀ (c : f.Cell j),
  Membership.mem (γ := Set (X _⦋(f.mapN (Cell.type₂ f c)).dim⦌)) (X.nonDegenerate (f.mapN (Cell.type₂ f c)).dim)
    (f.mapN (Cell.type₂ f c)).simplex
Tactic: obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ Membership.mem (γ := Set (X _⦋(f.mapN (Cell.type₁ f c)).dim⦌)) (X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim)
    (f.mapN (Cell.type₁ f c)).simplex
have inl : Membership.mem (γ :=
  Set
    (X _⦋S.dim.{u} (X := X)
        (S.mk (dim :=
          S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))))⦌))
  (X.nonDegenerate
    (S.dim.{u} (X := X)
      (S.mk (dim :=
        S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
        (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))))))
  (S.simplex
    (S.mk (dim :=
      S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))))
Tactic: rw [f.mapN_type₁]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ Membership.mem (γ := Set (X _⦋(f.mapN (Cell.type₂ f c)).dim⦌)) (X.nonDegenerate (f.mapN (Cell.type₂ f c)).dim)
    (f.mapN (Cell.type₂ f c)).simplex
have inr : Membership.mem (γ := Set (X _⦋{ dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex : X.S }.dim⦌))
  (X.nonDegenerate { dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex : X.S }.dim)
  { dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex : X.S }.simplex
Tactic: rw [f.mapN_type₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
s t : (range (X := f.sigmaHorn j) (f.m j)).N
h : f.mapN s = f.mapN t
⊢ s = t
have inl : ∀ (c : f.Cell j) (h : f.mapN (Cell.type₁ f c) = f.mapN t), Cell.type₁ f c = t
Tactic: obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
s t : (range (X := f.sigmaHorn j) (f.m j)).N
h : f.mapN s = f.mapN t
inl : ∀ (c : f.Cell j) (h : f.mapN (Cell.type₁ f c) = f.mapN t), Cell.type₁ f c = t
⊢ s = t
have inr : ∀ (c : f.Cell j) (h : f.mapN (Cell.type₂ f c) = f.mapN t), Cell.type₂ f c = t
Tactic: obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
t : (range (X := f.sigmaHorn j) (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN t
⊢ Cell.type₁ f c = t
have inl : ∀ (c' : f.Cell j) (h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')),
  Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c')
Tactic: obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t
Cleared hypotheses: t, h