awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ 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)))
have a : 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)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax i
a :
  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) =
    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)))
have 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))) ≤
  f.filtration (Order.succ i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ 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)))
have 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)))
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : 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)))
have 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)))
Tactic: refine ⟨(f.le_filtration _).trans le_sup_left, fun j hj c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax i
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)))
have 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)))
Tactic: rw [Order.lt_succ_iff_of_not_isMax hi] at hj
Cleared hypotheses: hj, c
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax 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 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)))
have 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)))
Tactic: obtain hj | rfl := hj.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : 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)))
⊢ 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)))
have 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)))
Tactic: obtain hj | rfl := hj.lt_or_eq
Cleared hypotheses: i, hi, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : SuccOrder ι
i : ι
hi : ¬IsMax 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)
have 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)
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i = ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
have a : f.filtration i ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a : f.filtration i ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
⊢ f.filtration i = ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
have a₁ : ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ≤ f.filtration i
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ 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
have 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)
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : 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)
have a : A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
Tactic: refine ⟨?_, fun j hj c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
a : A ≤ ⨆ (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)
have 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)
Tactic: refine ⟨?_, fun j hj c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j
have a : A ≤ ⨆ (_ : ⊥ < i), f.filtration ⊥
Tactic: refine le_trans ?_ (le_iSup _ ⊥)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : 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)
have 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))
Tactic: refine le_trans ?_ (le_iSup _ (Order.succ j))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
⊢ Order.succ j < i
have rwa : ∀ (hj : Order.succ j < i) (c : f.Cell j), Order.succ j < i
Tactic: rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj
Cleared hypotheses: hj, c
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : 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))))
    (⨆ (_ : Order.succ j < i), f.filtration (Order.succ j))
have 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)
Tactic: refine le_trans ?_ (le_iSup _
        (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j ≤ f.filtration i
have a : ∀ (i_1 : ι) (i_2 : i_1 < i), f.filtration i_1 ≤ f.filtration i
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) = f.filtration m
have a : ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ≤ f.filtration m
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
a : ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ≤ f.filtration m
⊢ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) = f.filtration m
have a₁ : f.filtration m ≤ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι) ≤ f.filtration m
have a : ∀ (a : ι) (b : a < m), f.filtration a ≤ f.filtration m
Tactic: simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : OrderBot ι
inst_2 : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ 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 : ι)
have 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 : ι))
Tactic: simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
⊢ ¬(↑c.s : A.N).subcomplex ≤ f.filtration j
have 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⦌)
Tactic: simp only [ofSimplex_le_iff, filtration_def, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, not_or, not_exists]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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⦌)
have 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
Tactic: refine ⟨c.s.val.notMem, fun i hi c' h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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
⊢ False
have 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
Tactic: rw [← c.rank_s, ← c'.rank_s] at hi
Cleared hypotheses: hi, c', h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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
have refine : P.AncestralRel c.s c'.s
Tactic: refine lt_irrefl _ (hi.trans (f.lt ?_))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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
have refine_1 : ∀ (hxy : c.s = c'.s), False
Tactic: refine ⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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
⊢ P.AncestralRel c.s c'.s
have refine_2 : (↑c.s : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
Tactic: refine ⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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
have hi₁ : f.rank c'.s < f.rank c'.s
Tactic: rw [hxy] at hi
Cleared hypotheses: hi, h, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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
⊢ (↑c.s : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
have 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)))
Tactic: rw [← ofSimplex_le_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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)))
⊢ (↑c.s : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
have 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)
Tactic: rwa [Subcomplex.N.le_iff, SSet.N.le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
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)
⊢ (↑c.s : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
have 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)))
Tactic: rwa [Subcomplex.N.le_iff, SSet.N.le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
⊢ Eq.{u + 1} (α := X.Subcomplex) (⨆ (i : ι), f.filtration i) ⊤
have refine : LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (i : ι), f.filtration i)
Tactic: refine le_antisymm (by simp) ?_