awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ (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:
Or.inl (Or.inl hx)

Premises used: Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ (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:
exact Or.inl (Or.inl hx)

Premises used: Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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_1 : 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
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:
Or.inl (Or.inr ⟨i, hi, c, hx⟩)

Premises used: And.intro, Exists.intro, Or.inl, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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_1 : 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
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:
exact Or.inl (Or.inr ⟨i, hi, c, hx⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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 ∈ (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

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_assoc, SSet.Subcomplex.Pairing.RankFunction.Cell.range_map, SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
hx₁ : x ∈ (range (c.ιSigmaStdSimplex ≫ f.b i ≫ (f.filtration (Order.succ i)).ι)).obj d
⊢ i ≤ i

Tactic:
rw [← c.range_map, ← c.mapToSucc_ι, ← c.ι_b_assoc] at hx

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_assoc, SSet.Subcomplex.Pairing.RankFunction.Cell.range_map, SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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
⊢ (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
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
hi : i ≤ i
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:
Or.inr ⟨_, hy⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
hi : i ≤ i
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:
exact Or.inr ⟨_, hy⟩

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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 ⋯).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))) ⋯).simplex :
      X.S }
⊢ 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)))))

Tactic:
rw [← S.cast_eq_self _ (P.dim_p c.s)]

Premises used: SSet.Subcomplex.Pairing.dim_p, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.S.cast_eq_self
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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))) ⋯).simplex
⊢ 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 }

Tactic:
rw [S.ext_iff, c.ι_b_app_apply]

Premises used: SSet.S.ext_iff, SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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) (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))) ⋯).simplex

Tactic:
apply yonedaEquiv_symm_app_id

Premises used: SSet.yonedaEquiv_symm_app_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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 }
⊢ f.mapN (Cell.type₂ f c) = { dim := (↑c.s : A.N).dim, simplex := (↑c.s : A.N).simplex }

Tactic:
dsimp [mapN]

Premises used: SSet.Subcomplex.Pairing.RankFunction.mapN
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
rw :
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (lift c.map ⋯) (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
⊢ 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:
rw [S.ext_iff, c.ι_b_app_apply, Cell.mapToSucc]

Premises used: SSet.S.ext_iff, SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc, SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
rw rw₁ : (↑c.s : A.N).simplex = (↑c.s : A.N).simplex
⊢ (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

Tactic:
rw [Cell.map_app_objEquiv_symm_δ_index]

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.map_app_objEquiv_symm_δ_index
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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
⊢ Membership.mem (γ := Set (X _⦋(f.mapN s).dim⦌)) (X.nonDegenerate (f.mapN s).dim) (f.mapN s).simplex

Tactic:
obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s

Premises used: SSet.Subcomplex.Pairing.RankFunction.exists_or_of_range_m_N, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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))))))
⊢ 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:
rw [f.mapN_type₁]

Premises used: SSet.Subcomplex.Pairing.RankFunction.mapN_type₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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 _⦋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:
(P.p c.s).val.nonDegenerate

Premises used: Set.Mem, SSet.Subcomplex.Pairing.p, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.Subcomplex.N.toN, SSet.N.nonDegenerate, Subtype.val, DFunLike.coe