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 : SuccOrder ι
i : ι
hi : ¬IsMax i
a :
  A ≤
      f.filtration i ⊔
        ⨆ (c : f.Cell i),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ∧
    ∀ (i_1 : ι) (i_2 : i_1 < Order.succ i) (i_3 : f.Cell i_1),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_3.s) : A.N))) ≤
        f.filtration i ⊔
          ⨆ (c : f.Cell i),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
⊢ A ⊔
      ⨆ (j : ι),
        ⨆ (_ : j < Order.succ i),
          ⨆ (c : f.Cell j),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration i ⊔
      ⨆ (c : f.Cell i),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_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 : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ A ≤
      f.filtration i ⊔
        ⨆ (c : f.Cell i),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ∧
    ∀ (i_1 : ι) (i_2 : i_1 < Order.succ i) (i_3 : f.Cell i_1),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_3.s) : A.N))) ≤
        f.filtration i ⊔
          ⨆ (c : f.Cell i),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
⟨(f.le_filtration _).trans le_sup_left, fun j hj c ↦ ?_⟩

Premises used: le_sup_left, And.intro, LE.le.trans, SSet.Subcomplex.Pairing.RankFunction.le_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 : SuccOrder ι
i : ι
hi : ¬IsMax i
a :
  ∀ (j : ι) (hj : j < Order.succ i) (c : f.Cell j),
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
      f.filtration i ⊔
        ⨆ (c : f.Cell i),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
⊢ A ≤
      f.filtration i ⊔
        ⨆ (c : f.Cell i),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ∧
    ∀ (i_1 : ι) (i_2 : i_1 < Order.succ i) (i_3 : f.Cell i_1),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_3.s) : A.N))) ≤
        f.filtration i ⊔
          ⨆ (c : f.Cell i),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
refine ⟨(f.le_filtration _).trans le_sup_left, fun j hj c ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj : j < Order.succ i
c : f.Cell j
a :
  ∀ (hj : j ≤ i) (c : f.Cell j),
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
      f.filtration i ⊔
        ⨆ (c : f.Cell i),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration i ⊔
      ⨆ (c : f.Cell i),
        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 [Order.lt_succ_iff_of_not_isMax hi] at hj

Premises used: Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj : j ≤ i
c : f.Cell j
a :
  ∀ (hj : j < i),
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
      f.filtration i ⊔
        ⨆ (c : f.Cell i),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
a₁ :
  ∀ (hi : ¬IsMax j) (hj : j ≤ j),
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
      f.filtration j ⊔
        ⨆ (c : f.Cell j),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration i ⊔
      ⨆ (c : f.Cell i),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
obtain hj | rfl := hj.lt_or_eq

Premises used: LE.le.lt_or_eq, 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 : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj_1 : j ≤ i
c : f.Cell j
hj : j < i
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration i ⊔
      ⨆ (c : f.Cell i),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
(f.subcomplex_le_filtration _ hj).trans le_sup_left

Premises used: le_sup_left, SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, LE.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 : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj_1 : j ≤ i
c : f.Cell j
hj : j < i
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration i ⊔
      ⨆ (c : f.Cell i),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
exact (f.subcomplex_le_filtration _ hj).trans le_sup_left

Premises used: le_sup_left, SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, LE.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 : SuccOrder ι
j : ι
c : f.Cell j
hi : ¬IsMax j
hj : j ≤ j
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : 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 : SuccOrder ι
j : ι
c : f.Cell j
hi : ¬IsMax j
hj : j ≤ j
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration j ⊔
      ⨆ (c : f.Cell j),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
exact le_trans (le_trans (by rfl) (le_iSup _ c)) le_sup_right

Premises used: le_iSup, le_sup_right, 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 : SuccOrder ι
i : ι
hi : ¬IsMax i
a :
  f.filtration i ≤ f.filtration (Order.succ i) ∧
    ∀ (i_1 : f.Cell i),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))) ≤
        f.filtration (Order.succ i)
⊢ f.filtration i ⊔
      ⨆ (c : f.Cell i),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration (Order.succ i)

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_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 : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration i ≤ f.filtration (Order.succ i) ∧
    ∀ (i_1 : f.Cell i),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))) ≤
        f.filtration (Order.succ i)

Tactic:
⟨f.filtration_monotone (Order.le_succ i),
      fun c ↦ f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hi)⟩

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, Order.lt_succ_of_not_isMax, And.intro, SSet.Subcomplex.Pairing.RankFunction.filtration_monotone, Order.le_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 : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration i ≤ f.filtration (Order.succ i) ∧
    ∀ (i_1 : f.Cell i),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))) ≤
        f.filtration (Order.succ i)

Tactic:
exact ⟨f.filtration_monotone (Order.le_succ i),
      fun c ↦ f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hi)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a : f.filtration i ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
a₁ : ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ≤ f.filtration i
⊢ f.filtration i = ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j

Tactic:
apply le_antisymm

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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a :
  A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ∧
    ∀ (i_1 : ι) (i_2 : i_1 < i) (i_3 : f.Cell i_1),
      LE.le.{u} (α := X.Subcomplex)
        (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_3.s) : A.N))))
        (⨆ (j : ι), ⨆ (_ : j < i), f.filtration j)
⊢ A ⊔
      ⨆ (j : ι),
        ⨆ (_ : j < i),
          ⨆ (c : f.Cell j),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ∧
    ∀ (i_1 : ι) (i_2 : i_1 < i) (i_3 : f.Cell i_1),
      LE.le.{u} (α := X.Subcomplex)
        (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_3.s) : A.N))))
        (⨆ (j : ι), ⨆ (_ : j < i), f.filtration j)

Tactic:
⟨?_, fun j hj c ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a : A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
a₁ :
  ∀ (j : ι) (hj : j < i) (c : f.Cell j),
    LE.le.{u} (α := X.Subcomplex)
      (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
      (⨆ (j : ι), ⨆ (_ : j < i), f.filtration j)
⊢ A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ∧
    ∀ (i_1 : ι) (i_2 : i_1 < i) (i_3 : f.Cell i_1),
      LE.le.{u} (α := X.Subcomplex)
        (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_3.s) : A.N))))
        (⨆ (j : ι), ⨆ (_ : j < i), f.filtration j)

Tactic:
refine ⟨?_, fun j hj c ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j

Tactic:
le_trans ?_ (le_iSup _ ⊥)

Premises used: le_iSup, Bot.bot, 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a : A ≤ ⨆ (_ : ⊥ < i), f.filtration ⊥
⊢ A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j

Tactic:
refine le_trans ?_ (le_iSup _ ⊥)

Premises used: le_iSup, Bot.bot, 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ (_ : ⊥ < i), f.filtration ⊥

Tactic:
exact le_trans (by simp) (le_iSup _ hi.bot_lt)

Premises used: le_iSup, Order.IsSuccLimit.bot_lt, 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (⨆ (j : ι), ⨆ (_ : j < i), f.filtration j)

Tactic:
le_trans ?_ (le_iSup _ (Order.succ j))

Premises used: Order.succ, le_iSup, 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
a :
  LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (⨆ (_ : Order.succ j < i), f.filtration (Order.succ j))
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (⨆ (j : ι), ⨆ (_ : j < i), f.filtration j)

Tactic:
refine le_trans ?_ (le_iSup _ (Order.succ j))

Premises used: Order.succ, le_iSup, 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
rwa rwa₁ rwa₂ rwa₃ : ∀ (hj : Order.succ j < i) (c : f.Cell j), Order.succ j < i
⊢ Order.succ j < i

Tactic:
rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj

Premises used: Order.IsSuccLimit.succ_lt_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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
a :
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration (Order.succ j)
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (⨆ (_ : Order.succ j < i), f.filtration (Order.succ j))

Tactic:
refine le_trans ?_ (le_iSup _
        (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj))

Premises used: le_iSup, 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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration (Order.succ j)

Tactic:
f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax)

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, Order.lt_succ_of_not_isMax, LT.lt.not_isMax
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration (Order.succ j)

Tactic:
exact f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax)

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, Order.lt_succ_of_not_isMax, LT.lt.not_isMax
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a : ∀ (i_1 : ι) (i_2 : i_1 < i), f.filtration i_1 ≤ f.filtration i
⊢ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ≤ f.filtration i

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_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 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
⊢ f.filtration j ≤ f.filtration i

Tactic:
f.filtration_monotone hj.le

Premises used: LT.lt.le, SSet.Subcomplex.Pairing.RankFunction.filtration_monotone
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
⊢ f.filtration j ≤ f.filtration i

Tactic:
exact f.filtration_monotone hj.le

Premises used: LT.lt.le, SSet.Subcomplex.Pairing.RankFunction.filtration_monotone
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
a : ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ≤ f.filtration m
a₁ : f.filtration m ≤ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι)
⊢ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) = f.filtration m

Tactic:
apply le_antisymm

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 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
a : ∀ (a : ι) (b : a < m), f.filtration a ≤ f.filtration m
⊢ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ≤ f.filtration m

Tactic:
simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]

Premises used: Set.mem_Iio, Subtype.forall, iSup_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 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
j : ι
hj : j < m
⊢ f.filtration j ≤ f.filtration m

Tactic:
f.filtration_monotone hj.le

Premises used: LT.lt.le, SSet.Subcomplex.Pairing.RankFunction.filtration_monotone
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
j : ι
hj : j < m
⊢ f.filtration j ≤ f.filtration m

Tactic:
exact f.filtration_monotone hj.le

Premises used: LT.lt.le, SSet.Subcomplex.Pairing.RankFunction.filtration_monotone
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
a :
  f.filtration ⊥ ≤ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ∧
    ∀ (i : ι) (i_1 : i < m) (i_2 : f.Cell i),
      LE.le.{u} (α := X.Subcomplex)
        (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_2.s) : A.N))))
        (⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι))
⊢ A ⊔
      ⨆ (j : ι),
        ⨆ (_ : j < m),
          ⨆ (c : f.Cell j),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι)

Tactic:
simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot]

Premises used: SSet.Subcomplex.Pairing.RankFunction.filtration_bot, sup_le_iff, iSup_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 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration ⊥ ≤ f.filtration ⊥

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 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
j : ι
hj : j < m
c : f.Cell j
⊢ f.filtration (Order.succ j) ≤ f.filtration (Order.succ j)

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 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration ⊥ ≤ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ∧
    ∀ (i : ι) (i_1 : i < m) (i_2 : f.Cell i),
      LE.le.{u} (α := X.Subcomplex)
        (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_2.s) : A.N))))
        (⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι))

Tactic:
exact ⟨le_trans (by rfl) (le_iSup _ ⟨⊥, hm.bot_lt⟩), fun j hj c ↦
      (f.subcomplex_le_filtration c (Order.lt_succ_of_not_isMax (not_isMax_of_lt hj))).trans
        (le_trans (by rfl) (le_iSup _ ⟨Order.succ j, hm.succ_lt_iff.mpr hj⟩))⟩