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 ι
j : ι
c : f.Cell j
simp :
  (↑c.s : A.N).simplex ∉ A.obj (op ⦋(↑c.s : A.N).dim⦌) ∧
    ∀ (x : ι) (x_1 : x < j) (x_2 : f.Cell x),
      (↑c.s : A.N).simplex ∉
        Subfunctor.obj
          (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x_2.s) : A.N))))
          (op ⦋(↑c.s : A.N).dim⦌)
⊢ ¬(↑c.s : A.N).subcomplex ≤ f.filtration j

Tactic:
simp only [ofSimplex_le_iff, filtration_def, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, not_or, not_exists]

Premises used: Set.mem_union, CategoryTheory.Subfunctor.max_obj, Set.mem_iUnion, not_exists, SSet.Subcomplex.Pairing.RankFunction.filtration_def, not_or, SSet.Subcomplex.ofSimplex_le_iff, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
⊢ (↑c.s : A.N).simplex ∉ A.obj (op ⦋(↑c.s : A.N).dim⦌) ∧
    ∀ (x : ι) (x_1 : x < j) (x_2 : f.Cell x),
      (↑c.s : A.N).simplex ∉
        Subfunctor.obj
          (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x_2.s) : A.N))))
          (op ⦋(↑c.s : A.N).dim⦌)

Tactic:
⟨c.s.val.notMem, fun i hi c' h ↦ ?_⟩

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.s, And.intro, Subtype.val, SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
refine :
  ∀ (i : ι) (hi : i < j) (c' : f.Cell i)
    (h :
      Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
        (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))))
          (op ⦋(↑c.s : A.N).dim⦌))
        (↑c.s : A.N).simplex),
    False
⊢ (↑c.s : A.N).simplex ∉ A.obj (op ⦋(↑c.s : A.N).dim⦌) ∧
    ∀ (x : ι) (x_1 : x < j) (x_2 : f.Cell x),
      (↑c.s : A.N).simplex ∉
        Subfunctor.obj
          (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x_2.s) : A.N))))
          (op ⦋(↑c.s : A.N).dim⦌)

Tactic:
refine ⟨c.s.val.notMem, fun i hi c' h ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
hi : i < j
c' : f.Cell i
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
rw :
  ∀ (c' : f.Cell i) (hi : f.rank c'.s < f.rank c.s)
    (h :
      Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
        (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))))
          (op ⦋(↑c.s : A.N).dim⦌))
        (↑c.s : A.N).simplex),
    False
⊢ False

Tactic:
rw [← c.rank_s, ← c'.rank_s] at hi

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.rank_s
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
⊢ False

Tactic:
lt_irrefl _ (hi.trans (f.lt ?_))

Premises used: lt_irrefl, LT.lt.trans, SSet.Subcomplex.Pairing.RankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
refine : P.AncestralRel c.s c'.s
⊢ False

Tactic:
refine lt_irrefl _ (hi.trans (f.lt ?_))

Premises used: lt_irrefl, LT.lt.trans, SSet.Subcomplex.Pairing.RankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
⊢ P.AncestralRel c.s c'.s

Tactic:
⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩

Premises used: SSet.Subcomplex.Pairing.ne, Ne.symm, And.intro, SSet.Subcomplex.Pairing.AncestralRel, lt_of_le_of_ne
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
refine_1 : ∀ (hxy : c.s = c'.s), False
refine_2 : (↑c.s : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
⊢ P.AncestralRel c.s c'.s

Tactic:
refine ⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
hxy : c.s = c'.s
⊢ f.rank c'.s < f.rank c'.s

Tactic:
rw [hxy] at hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
hxy : c.s = c'.s
hi₁ : f.rank c'.s < f.rank c'.s
⊢ Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex

Tactic:
rw [hxy] at hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
hxy : c.s = c'.s
hi₁ : f.rank c'.s < f.rank c'.s
h₁ :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
⊢ c.s = c'.s

Tactic:
rw [hxy] at hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c'.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
hxy : c.s = c'.s
⊢ False

Tactic:
(lt_irrefl _ hi).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c'.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
hxy : c.s = c'.s
⊢ False

Tactic:
exact (lt_irrefl _ hi).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  Membership.mem (γ := Set (X _⦋(↑c.s : A.N).dim⦌))
    (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))))
      (op ⦋(↑c.s : A.N).dim⦌))
    (↑c.s : A.N).simplex
⊢ ofSimplex (↑c.s : A.N).simplex ≤
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)))

Tactic:
rw [← ofSimplex_le_iff] at h

Premises used: SSet.Subcomplex.ofSimplex_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h :
  ofSimplex (↑c.s : A.N).simplex ≤
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)))
refine_2 : (↑c.s : A.N).toN ≤ N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  (↑c.s : A.N).subcomplex ≤
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)))
⊢ (↑c.s : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)

Tactic:
rwa [Subcomplex.N.le_iff, SSet.N.le_iff]

Premises used: SSet.Subcomplex.N.le_iff, SSet.N.le_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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
⊢ LE.le.{u} (α := X.Subcomplex) (⨆ (i : ι), f.filtration i) ⊤

Tactic:
simp
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
refine : LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (i : ι), f.filtration i)
⊢ Eq.{u + 1} (α := X.Subcomplex) (⨆ (i : ι), f.filtration i) ⊤

Tactic:
refine le_antisymm (by simp) ?_

Premises used: le_antisymm
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
rw : ∀ (s : X.N), s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ (i : ι), f.filtration i
⊢ LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (i : ι), f.filtration i)

Tactic:
rw [N.subcomplex_le_iff]

Premises used: SSet.N.subcomplex_le_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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : X.N
_ : s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ (i : ι), f.filtration i
⊢ s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ (i : ι), f.filtration i

Tactic:
_
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : X.N
h : s.subcomplex ≤ ⊤
hs : s.subcomplex ≤ A
⊢ A ≤ f.filtration ⊥

Tactic:
simp
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : X.N
h : s.subcomplex ≤ ⊤
hs : s.subcomplex ≤ A
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i

Tactic:
exact hs.trans (le_trans (by simp) (le_iSup _ ⊥))

Premises used: le_iSup, Bot.bot, LE.le.trans, le_trans
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : A.N
h : s.subcomplex ≤ ⊤
notMem :
  ∀ (t : (↑P.II : Type u)) (ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)),
    s.subcomplex ≤ ⨆ (i : ι), f.filtration i
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i

Tactic:
obtain ⟨t, ht⟩ := P.exists_or s

Premises used: SSet.Subcomplex.Pairing.exists_or
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : A.N
h : s.subcomplex ≤ ⊤
t : (↑P.II : Type u)
ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i

Tactic:
le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _))

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, le_iSup, Order.lt_succ, SSet.Subcomplex.Pairing.RankFunction.Cell.mk, rfl, le_trans
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : A.N
h : s.subcomplex ≤ ⊤
t : (↑P.II : Type u)
ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
notMem :
  s.subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
            A.N)))
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i

Tactic:
refine le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _))

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, le_iSup, Order.lt_succ, SSet.Subcomplex.Pairing.RankFunction.Cell.mk, rfl, le_trans
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : A.N
h : s.subcomplex ≤ ⊤
t : (↑P.II : Type u)
ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
notMem :
  (↑t : A.N).subcomplex ≤ ⊤ →
    (↑t : A.N).subcomplex ≤
      S.subcomplex
        (N.toS
          (N.toN (A := A)
            (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                  (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
              A.N)))
notMem₁ :
  LE.le.{u} (α := X.Subcomplex)
      (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)))) ⊤ →
    LE.le.{u} (α := X.Subcomplex)
      (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))))
      (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))))
⊢ s.subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
            A.N)))

Tactic:
obtain rfl | rfl := ht

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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
t : (↑P.II : Type u)
h : (↑t : A.N).subcomplex ≤ ⊤
⊢ (↑t : A.N).subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
            A.N)))

Tactic:
P.le t

Premises used: setOf, SSet.Subcomplex.Pairing.le
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
t : (↑P.II : Type u)
h : (↑t : A.N).subcomplex ≤ ⊤
⊢ (↑t : A.N).subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
            A.N)))

Tactic:
exact P.le t

Premises used: SSet.Subcomplex.Pairing.le
-- 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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
t : (↑P.II : Type u)
h :
  LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)))) ⊤
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))))
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))))

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 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : X.N
h : s.subcomplex ≤ ⊤
mem : ∀ (hs : s.subcomplex ≤ A), s.subcomplex ≤ ⨆ (i : ι), f.filtration i
notMem : ∀ (s : A.N), s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ (i : ι), f.filtration i
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i

Tactic:
cases s using SSet.Subcomplex.N.cases A with
  | mem s hs => exact hs.trans (le_trans (by simp) (le_iSup _ ⊥))
  | notMem s =>
    obtain ⟨t, ht⟩ := P.exists_or s
    refine le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _))
    obtain rfl | rfl := ht
    · exact P.le t
    · rfl

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
j : ι
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
c : f.Cell j
⊢ range c.map ≤ f.filtration (Order.succ j)

Tactic:
simpa using f.subcomplex_le_filtration c (Order.lt_succ _)

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, Order.lt_succ
-- 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
j : ι
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
c : f.Cell j
⊢ c.mapToSucc ≫ (f.filtration (Order.succ j)).ι = c.map

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, 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
d : ℕ
j : ι
a : f.sigmaHorn j _⦋d⦌
⊢ ∃ (c : f.Cell j) (x : c.horn.toSSet _⦋d⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app c.ιSigmaHorn (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (c.horn.toSSet _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋d⦌))
        x =
      a

Tactic:
Cofan.inj_jointly_surjective_of_isColimit
    ((isColimitCofanMkObjOfIsColimit ((CategoryTheory.evaluation _ _).obj _) _ _
      (coproductIsCoproduct _))) a

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit, CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit, CategoryTheory.evaluation, 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 ι
d : ℕ
j : ι
a : f.sigmaStdSimplex j _⦋d⦌
⊢ ∃ (c : f.Cell j) (x : Δ[c.dim + 1] _⦋d⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        x =
      a

Tactic:
Cofan.inj_jointly_surjective_of_isColimit
    ((isColimitCofanMkObjOfIsColimit ((CategoryTheory.evaluation _ _).obj _) _ _
      (coproductIsCoproduct _))) a

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit, CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit, CategoryTheory.evaluation, 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
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
y : f.Cell j
t : Δ[y.dim + 1] _⦋d⦌
h : x = y
rw rw₁ : Δ[y.dim + 1] _⦋d⦌ = Δ[y.dim + 1] _⦋d⦌
⊢ Δ[x.dim + 1] _⦋d⦌ = Δ[y.dim + 1] _⦋d⦌

Tactic:
rw [h]