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 ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono g
h₃ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex

Tactic:
obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.S.IsUniquelyCodimOneFace.unique, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono g
h₃ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
⊢ Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))

Tactic:
obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.S.IsUniquelyCodimOneFace.unique, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))
⊢ ¬LE.le.{u} (α := Δ[c.dim + 1].Subcomplex) (stdSimplex.face {c.index}ᶜ)
      (stdSimplex.face {S.IsUniquelyCodimOneFace.index ⋯ ⋯}ᶜ)

Tactic:
rw [← ofSimplex_le_iff, subcomplex_le_horn_iff, ← stdSimplex.face_singleton_compl] at h₁

Premises used: SSet.Subcomplex.ofSimplex_le_iff, SSet.subcomplex_le_horn_iff, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))
h₃ :
  ¬LE.le.{u} (α := Δ[c.dim + 1].Subcomplex) (stdSimplex.face {c.index}ᶜ)
      (stdSimplex.face {S.IsUniquelyCodimOneFace.index ⋯ ⋯}ᶜ)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex

Tactic:
rw [← ofSimplex_le_iff, subcomplex_le_horn_iff, ← stdSimplex.face_singleton_compl] at h₁

Premises used: SSet.Subcomplex.ofSimplex_le_iff, SSet.subcomplex_le_horn_iff, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))
h₃ :
  ¬LE.le.{u} (α := Δ[c.dim + 1].Subcomplex) (stdSimplex.face {c.index}ᶜ)
      (stdSimplex.face {S.IsUniquelyCodimOneFace.index ⋯ ⋯}ᶜ)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
⊢ Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))

Tactic:
rw [← ofSimplex_le_iff, subcomplex_le_horn_iff, ← stdSimplex.face_singleton_compl] at h₁

Premises used: SSet.Subcomplex.ofSimplex_le_iff, SSet.subcomplex_le_horn_iff, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h₁ :
  ¬LE.le.{u} (α := Δ[c.dim + 1].Subcomplex) (stdSimplex.face {c.index}ᶜ)
      (stdSimplex.face {S.IsUniquelyCodimOneFace.index ⋯ ⋯}ᶜ)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))
⊢ False

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
rw :
  c.horn.image c.map ≤
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ∧
    c.horn.image c.map ≠
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
⊢ c.horn.image c.map <
    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 [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ c.horn.image c.map ≤
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))

Tactic:
simpa using image_le_range c.horn c.map

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.map, SSet.Subcomplex.Pairing.RankFunction.Cell.horn, SSet.Subcomplex.image_le_range
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h :
  c.horn.image c.map =
    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).subcomplex ≤ c.horn.image c.map

Tactic:
simpa only [h] using P.le c.s

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.s, 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 ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ c.horn.image c.map ≤
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ∧
    c.horn.image c.map ≠
      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 ⟨by simpa using image_le_range c.horn c.map,
    fun h ↦ c.subcomplex_not_le_image_horn (by simpa only [h] using P.le c.s)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
rw :
  ofSimplex (n := c.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
            (SimplexCategory.δ c.index) :
          Δ[c.dim + 1] _⦋c.dim⦌)) =
    (↑c.s : A.N).subcomplex
⊢ image (stdSimplex.face {c.index}ᶜ) c.map = (↑c.s : A.N).subcomplex

Tactic:
rw [stdSimplex.face_singleton_compl, image_ofSimplex]

Premises used: SSet.Subcomplex.image_ofSimplex, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
e_x :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
        (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
          (SimplexCategory.δ c.index) :
        Δ[c.dim + 1] _⦋c.dim⦌) =
    (↑c.s : A.N).simplex
⊢ ofSimplex (n := c.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
            (SimplexCategory.δ c.index) :
          Δ[c.dim + 1] _⦋c.dim⦌)) =
    (↑c.s : A.N).subcomplex

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
        (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
          (SimplexCategory.δ c.index) :
        Δ[c.dim + 1] _⦋c.dim⦌) =
    (↑c.s : A.N).simplex

Tactic:
exact (P.isUniquelyCodimOneFace c.s).δ_index rfl

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.S.IsUniquelyCodimOneFace.δ_index, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
⊢ f.filtration 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)))

Tactic:
rfl

Premises used: SSet.Subcomplex.Pairing.RankFunction.filtration, rfl
-- 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 : ι
h : 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

Tactic:
le_trans ?_ le_sup_right

Premises used: 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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
refine :
  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),
        ⨆ (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

Tactic:
refine le_trans ?_ le_sup_right

Premises used: 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 ι
j : ι
c : f.Cell j
i : ι
h : j < 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)) c.s) : A.N))))
    (⨆ (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))))

Tactic:
le_trans ?_ (le_iSup _ j)

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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
refine :
  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 < 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))))
⊢ 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),
        ⨆ (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:
refine le_trans ?_ (le_iSup _ j)

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 ι
j : ι
c : f.Cell j
i : ι
h : j < 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)) c.s) : A.N))))
    (⨆ (_ : 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))))

Tactic:
le_trans ?_ (le_iSup _ h)

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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
refine :
  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))))
    (⨆ (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))))
⊢ 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 < 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))))

Tactic:
refine le_trans ?_ (le_iSup _ h)

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 ι
j : ι
c : f.Cell j
i : ι
h : j < 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)) 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 ι
j : ι
c : f.Cell j
i : ι
h : j < 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)) c.s) : A.N))))
    (⨆ (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 (by rfl) (le_iSup _ c)

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 ι
i : ι
⊢ A ≤ f.filtration i

Tactic:
le_sup_left

Premises used: le_sup_left
-- 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 ι
⊢ f.filtration ⊥ = A

Tactic:
simp [filtration_def]

Premises used: SSet.Subcomplex.Pairing.RankFunction.filtration_def
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ i₂
simp :
  ∀ (i : ι) (i_1 : i < i₁) (i_2 : f.Cell i),
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_2.s) : A.N))) ≤
      f.filtration 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))) ≤
    f.filtration i₂

Tactic:
simp only [sup_le_iff, iSup_le_iff, le_filtration, true_and]

Premises used: sup_le_iff, iSup_le_iff, SSet.Subcomplex.Pairing.RankFunction.le_filtration, true_and
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ 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₂

Tactic:
f.subcomplex_le_filtration c (lt_of_lt_of_le hj h)

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, lt_of_lt_of_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ 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₂

Tactic:
exact f.subcomplex_le_filtration c (lt_of_lt_of_le hj h)

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, lt_of_lt_of_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 : 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)))
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)
⊢ 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

Premises used: le_antisymm