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 : ι
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:
exact (P.p c.s).val.nonDegenerate

Premises used: SSet.Subcomplex.Pairing.p, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.Subcomplex.N.toN, SSet.N.nonDegenerate, Subtype.val, DFunLike.coe
-- 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
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
⊢ 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 _⦋{ 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:
c.s.val.nonDegenerate

Premises used: Set.Mem, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.Subcomplex.N.toN, SSet.N.nonDegenerate, Subtype.val
-- 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 _⦋{ 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:
exact c.s.val.nonDegenerate

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.Subcomplex.N.toN, SSet.N.nonDegenerate, Subtype.val
-- 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 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
inr : ∀ (c : f.Cell j) (h : f.mapN (Cell.type₂ f c) = f.mapN t), Cell.type₂ f c = t
⊢ s = t

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 : ι
t : (range (X := f.sigmaHorn j) (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN t
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')
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')
⊢ Cell.type₁ f c = t

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

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 : ι
t : (range (X := f.sigmaHorn j) (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN t
inr :
  ∀ (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')
inr₁ :
  ∀ (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')
⊢ Cell.type₂ f c = t

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

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 c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')
⊢ Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Premises used: SSet.Subcomplex.Pairing.RankFunction.mapN_type₂, SSet.Subcomplex.Pairing.RankFunction.mapN_type₁, SSet.Subcomplex.N.eq_iff_sMk_eq, Subtype.ext_iff
-- 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 c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₂ f c')
⊢ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) = (↑c'.s : A.N)

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Premises used: SSet.Subcomplex.Pairing.RankFunction.mapN_type₂, SSet.Subcomplex.Pairing.RankFunction.mapN_type₁, SSet.Subcomplex.N.eq_iff_sMk_eq, Subtype.ext_iff
-- 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 c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')
⊢ (↑c.s : A.N) = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Premises used: SSet.Subcomplex.Pairing.RankFunction.mapN_type₂, SSet.Subcomplex.Pairing.RankFunction.mapN_type₁, SSet.Subcomplex.N.eq_iff_sMk_eq, Subtype.ext_iff
-- 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 c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₂ f c')
⊢ c.s = c'.s

Tactic:
simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h

Premises used: SSet.Subcomplex.Pairing.RankFunction.mapN_type₂, SSet.Subcomplex.Pairing.RankFunction.mapN_type₁, SSet.Subcomplex.N.eq_iff_sMk_eq, Subtype.ext_iff
-- 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 c' : f.Cell j
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
s : c.s = c'.s
⊢ c = c'

Tactic:
ext : 1
-- 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 c' : f.Cell j
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
⊢ c.s = c'.s

Tactic:
P.p.injective h

Premises used: SSet.Subcomplex.Pairing.p, Equiv.injective
-- 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 c' : f.Cell j
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
⊢ c.s = c'.s

Tactic:
exact P.p.injective h

Premises used: SSet.Subcomplex.Pairing.p, Equiv.injective
-- 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 c' : f.Cell j
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
inl :
  ∀
    (h :
      Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
        ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))),
    Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c)
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c')

Tactic:
obtain rfl : c = c' := by ext : 1; exact P.p.injective h

Premises used: 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
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c)

Tactic:
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 c' : f.Cell j
h : (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) = (↑c'.s : A.N)
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₂ f c')

Tactic:
(P.ne _ _ h).elim

Premises used: False.elim, SSet.Subcomplex.Pairing.ne
-- 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 c' : f.Cell j
h : (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) = (↑c'.s : A.N)
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₂ f c')

Tactic:
exact (P.ne _ _ h).elim

Premises used: False.elim, SSet.Subcomplex.Pairing.ne
-- 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 c' : f.Cell j
h : (↑c.s : A.N) = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₁ f c')

Tactic:
(P.ne _ _ h.symm).elim

Premises used: False.elim, SSet.Subcomplex.Pairing.ne, Eq.symm
-- 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 c' : f.Cell j
h : (↑c.s : A.N) = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₁ f c')

Tactic:
exact (P.ne _ _ h.symm).elim

Premises used: False.elim, SSet.Subcomplex.Pairing.ne, Eq.symm
-- 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 c' : f.Cell j
h : c.s = c'.s
inr : c = c'
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₂ f c')

Tactic:
congr
-- 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 c' : f.Cell j
h : c.s = c'.s
⊢ c = c'

Tactic:
aesop
-- 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 : ι
⊢ Function.Injective (β := (f.filtration (Order.succ j)).toSSet.S) fun (x : (range (X := f.sigmaHorn j) (f.m j)).N) ↦
    S.mk (dim := x.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌)) →
            (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet _⦋x.dim⦌))
        x.simplex)

Tactic:
fun _ _ h ↦ f.isPushout_aux₂ (congr_arg (S.map (Subcomplex.ι _)) h)

Premises used: _private.0.SSet.Subcomplex.Pairing.RankFunction.isPushout_aux₂, Order.succ, SSet.Subcomplex.Pairing.RankFunction.filtration, congr_arg, SSet.Subcomplex.ι, SSet.S.map, Function.Injective
-- 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 : ι
x : SimplexCategoryᵒᵖ
d : ℕ
refine :
  IsPushout (Z := Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)) (P :=
    Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet)
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE ⋯))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j))
⊢ IsColimit (F := span (X := f.sigmaHorn j) (f.t j) (f.m j) ⋙ CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
    (Functor.mapCocone (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
      (PushoutCocone.mk (W := (f.filtration (Order.succ j)).toSSet) (homOfLE ⋯) (f.b j) ⋯))

Tactic:
refine (isColimitMapCoconePushoutCoconeEquiv _ _).symm
      (IsPushout.isColimit ?_)

Premises used: CategoryTheory.IsPushout.isColimit, Equiv.symm, CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv, DFunLike.coe
-- 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 : ι
x : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsPushout (Z := Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)) (P :=
    Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet)
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE ⋯))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j))

Tactic:
Types.isPushout_of_isPullback_of_mono'
      ((f.isPullback j).map ((CategoryTheory.evaluation _ _).obj _))
      (f.range_homOfLE_app_union_range_b_app _ _) (fun x₁ x₂ hx₁ hx₂ h ↦ ?_)

Premises used: CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono', SSet.Subcomplex.Pairing.RankFunction.range_homOfLE_app_union_range_b_app, SSet.Subcomplex.Pairing.RankFunction.isPullback, CategoryTheory.evaluation, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj
-- 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 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
dsimp :
  IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (f.filtration m)
⊢ IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (Cocone.pt (J := (↑(Set.Iio m) : Type v)) (F :=
      Monotone.functor (f :=
          (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s := fun (x1 x2 : ι) ↦
                x1 < x2) (Set.principalSegIio m)) :
            (a : (↑(Set.Iio m) : Type v)) → ι))
          ⋯ ⋙
        ⋯.functor)
      (PrincipalSeg.cocone (Set.principalSegIio m) ⋯.functor))

Tactic:
dsimp
-- 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 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
rw :
  IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι))
⊢ IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (f.filtration m)

Tactic:
rw [← f.iSup_filtration_iio m hm]

Premises used: SSet.Subcomplex.Pairing.RankFunction.iSup_filtration_iio
-- 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 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι))

Tactic:
apply isLUB_iSup

Premises used: isLUB_iSup
-- 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 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
rw : IsLUB (Set.range ⋯.functor.obj) (⨆ (i : ι), f.filtration i)
⊢ IsLUB (Set.range ⋯.functor.obj) ⊤

Tactic:
rw [← f.iSup_filtration]

Premises used: SSet.Subcomplex.Pairing.RankFunction.iSup_filtration
-- 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 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) (⨆ (i : ι), f.filtration i)

Tactic:
apply isLUB_iSup

Premises used: isLUB_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y : SSet
f g : X ⟶ Y
w : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
⊢ f = g

Tactic:
SimplicialObject.hom_ext _ _ w

Premises used: CategoryTheory.SimplicialObject.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X : SSet
n : SimplexCategoryᵒᵖ
⊢ NatTrans.app (𝟙 X) n = 𝟙 (X.obj n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
n : SimplexCategoryᵒᵖ
⊢ (f ≫ g).app n = f.app n ≫ g.app n

Tactic:
rfl

Premises used: rfl