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 : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
y : f.Cell j
t : Δ[y.dim + 1] _⦋d⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
          s :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (y.ιSigmaStdSimplex.app (op ⦋d⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[y.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
          t :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ↔
    ∃ (h : x = y), t = cast ⋯ s

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

Premises used: CategoryTheory.Limits.Cofan.inj_apply_eq_iff_of_isColimit, CategoryTheory.Limits.coproductIsCoproduct, 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 : ι
c : f.Cell j
rw : ∀ (k : SimplexCategoryᵒᵖ), Mono (c.ιSigmaStdSimplex.app k)
⊢ Mono c.ιSigmaStdSimplex

Tactic:
rw [NatTrans.mono_iff_mono_app]

Premises used: CategoryTheory.NatTrans.mono_iff_mono_app
-- 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 : ι
c : f.Cell j
d : ℕ
rw :
  Function.Injective (α := (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋d⦌)) (β :=
    (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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⦌))
⊢ Mono (X := Δ[c.dim + 1] _⦋d⦌) (c.ιSigmaStdSimplex.app (op ⦋d⦌))

Tactic:
rw [mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
c : f.Cell j
d : ℕ
x y : Δ[c.dim + 1] _⦋d⦌
h :
  Eq (α := (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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 :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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⦌))
        y :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
⊢ x = y

Tactic:
simpa [f.ιSigmaStdSimplex_eq_iff] using h.symm

Premises used: SSet.Subcomplex.Pairing.RankFunction.ιSigmaStdSimplex_eq_iff, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
⊢ Mono (X := f.sigmaHorn j) (Y := f.sigmaStdSimplex j) (Limits.Sigma.map (f.basicCell j))

Tactic:
infer_instance
-- 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 : ι
c : f.Cell j
⊢ c.ιSigmaHorn ≫ f.m j = c.horn.ι ≫ c.ιSigmaStdSimplex

Tactic:
simp [m]

Premises used: SSet.Subcomplex.Pairing.RankFunction.m
-- 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 : ι
c : f.Cell j
a : (f.filtration j).preimage c.map ≤ c.horn
a₁ : c.horn ≤ (f.filtration j).preimage c.map
⊢ (f.filtration j).preimage c.map = c.horn

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 : P.IsProper
j : ι
c : f.Cell j
⊢ (f.filtration j).preimage c.map ≤ c.horn

Tactic:
simpa only [subcomplex_le_horn_iff, ← Subcomplex.image_le_iff,
      Cell.image_face_index_compl] using c.subcomplex_not_le_filtration

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.image_face_index_compl, SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_filtration, SSet.Subcomplex.image_le_iff, SSet.subcomplex_le_horn_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
j : ι
c : f.Cell j
a : ∀ (s : X.N), s.subcomplex ≤ c.horn.image c.map → s.subcomplex ≤ f.filtration j
⊢ c.horn ≤ (f.filtration j).preimage c.map

Tactic:
rw [← Subcomplex.image_le_iff, N.subcomplex_le_iff]

Premises used: SSet.Subcomplex.image_le_iff, 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
j : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
hs' : s.subcomplex ≤ A
⊢ A ≤ f.filtration j

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
j : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
hs' : s.subcomplex ≤ A
⊢ s.subcomplex ≤ f.filtration j

Tactic:
exact hs'.trans (by simp)

Premises used: 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 : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
a :
  ∀ (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 ≤ f.filtration j
⊢ s.subcomplex ≤ f.filtration j

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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
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)
a : s.subcomplex ≤ f.filtration (f.rank c.s)
⊢ s.subcomplex ≤ f.filtration j

Tactic:
rw [← c.rank_s]

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 ι
inst_1 : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
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 ≤ f.filtration (f.rank c.s)

Tactic:
le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (f.lt ?_))

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, SSet.Subcomplex.Pairing.RankFunction.lt, 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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
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)
a :
  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)))
a₁ : P.AncestralRel t c.s
⊢ s.subcomplex ≤ f.filtration (f.rank c.s)

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

Premises used: SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration, SSet.Subcomplex.Pairing.RankFunction.lt, 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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
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)
a :
  ∀ (hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map),
    (↑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)))
a₁ :
  ∀
    (hs :
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
        c.horn.image c.map),
    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))
                  (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
              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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : A.N).subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) (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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : A.N).subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) (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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs :
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
    c.horn.image c.map
⊢ 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)) (s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
            A.N))))

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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
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)
inl : ∀ (hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map), (↑t : A.N).subcomplex ≤ c.horn.image c.map
inr :
  ∀
    (hs :
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
        c.horn.image c.map),
    (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map

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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map

Tactic:
hs
-- 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 : ι
c : f.Cell j
t : (↑P.II : Type u)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map

Tactic:
exact hs
-- 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 : ι
c : f.Cell j
t : (↑P.II : Type u)
hs :
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
    c.horn.image c.map
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map

Tactic:
le_trans ?_ hs

Premises used: 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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs :
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
    c.horn.image c.map
inr :
  (↑t : A.N).subcomplex ≤
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)))
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map

Tactic:
refine le_trans ?_ hs

Premises used: 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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs :
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
    c.horn.image c.map
⊢ (↑t : A.N).toS ≤ N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))

Tactic:
(P.isUniquelyCodimOneFace t).le

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.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
j : ι
c : f.Cell j
t : (↑P.II : Type u)
hs :
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))) ≤
    c.horn.image c.map
⊢ (↑t : A.N).toS ≤ N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))

Tactic:
exact (P.isUniquelyCodimOneFace t).le

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
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)
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map

Tactic:
replace hs : t.val.subcomplex ≤ c.horn.image c.map := by
          obtain rfl | rfl := ht
          · exact hs
          · refine le_trans ?_ hs
            rw [← S.le_def]
            exact (P.isUniquelyCodimOneFace t).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
j : ι
c : f.Cell j
s : A.N
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)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ P.AncestralRel t c.s

Tactic:
⟨?_, ?_⟩

Premises used: And.intro, SSet.Subcomplex.Pairing.AncestralRel
-- 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 : ι
c : f.Cell j
s : A.N
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)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
a : t ≠ c.s
a₁ : (↑t : A.N) < (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)
⊢ P.AncestralRel t c.s

Tactic:
refine ⟨?_, ?_⟩
-- 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 : ι
c : f.Cell j
s : A.N
ht : s = (↑c.s : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)
hs : (↑c.s : A.N).subcomplex ≤ c.horn.image c.map
⊢ False

Tactic:
c.subcomplex_not_le_image_horn hs

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_horn
-- 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 : ι
c : f.Cell j
s : A.N
ht : s = (↑c.s : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)
hs : (↑c.s : A.N).subcomplex ≤ c.horn.image c.map
⊢ False

Tactic:
exact c.subcomplex_not_le_image_horn hs

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_horn
-- 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 : ι
c : f.Cell j
s : A.N
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)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : 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:
lt_of_le_of_lt hs (c.image_horn_lt_subcomplex)

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.image_horn_lt_subcomplex, lt_of_le_of_lt
-- 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 : ι
c : f.Cell j
s : A.N
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)
hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map
⊢ (↑t : 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:
exact lt_of_le_of_lt hs (c.image_horn_lt_subcomplex)

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.image_horn_lt_subcomplex, lt_of_le_of_lt
-- 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 : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
a : ∀ (hs' : s.subcomplex ≤ A), s.subcomplex ≤ f.filtration j
a₁ : ∀ (s : A.N) (hs : s.subcomplex ≤ c.horn.image c.map), s.subcomplex ≤ f.filtration j
⊢ s.subcomplex ≤ f.filtration j

Tactic:
cases s using N.cases A with
    | mem s hs' => exact hs'.trans (by simp)
    | notMem s =>
      obtain ⟨t, ht⟩ := P.exists_or s
      rw [← c.rank_s]
      refine le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (f.lt ?_))
      · obtain rfl | rfl := ht
        · exact P.le t
        · simp
      · replace hs : t.val.subcomplex ≤ c.horn.image c.map := by
          obtain rfl | rfl := ht
          · exact hs
          · refine le_trans ?_ hs
            rw [← S.le_def]
            exact (P.isUniquelyCodimOneFace t).le
        refine ⟨?_, ?_⟩
        · rintro rfl
          exact c.subcomplex_not_le_image_horn hs
        · rw [Subcomplex.N.lt_iff, SSet.N.lt_iff]
          exact lt_of_le_of_lt hs (c.image_horn_lt_subcomplex)

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.image_horn_lt_subcomplex, lt_of_le_of_lt, SSet.Subcomplex.N.lt_iff, SSet.N.lt_iff, SSet.Subcomplex.Pairing.RankFunction.Cell.rank_s, 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 : ι
c : f.Cell j
⊢ range (c.horn.ι ≫ c.map) ≤ f.filtration j

Tactic:
simp [← image_top, image_le_iff, preimage_comp, c.preimage_filtration_map]

Premises used: SSet.Subcomplex.image_le_iff, SSet.Subcomplex.Pairing.RankFunction.Cell.preimage_filtration_map, SSet.Subcomplex.image_top, SSet.Subcomplex.preimage_comp
-- 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 : ι
c : f.Cell j
⊢ mapHorn f c ≫ (f.filtration j).ι = c.horn.ι ≫ c.map

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, SSet.Subcomplex.lift, CategoryTheory.Subfunctor.lift, 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 : ι
c : f.Cell j
⊢ Eq (α := c.horn.toSSet ⟶ (f.filtration j).toSSet) (c.ιSigmaHorn ≫ f.t j) (mapHorn f c)

Tactic:
simp [t, Sigma.ι_desc]

Premises used: SSet.Subcomplex.Pairing.RankFunction.t, CategoryTheory.Limits.Sigma.ι_desc
-- 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 : ι
c : f.Cell j
x : SimplexCategoryᵒᵖ
⊢ Eq (α := c.horn.toSSet.obj x ⟶ (f.filtration j).toSSet.obj x) (NatTrans.app c.ιSigmaHorn x ≫ NatTrans.app (f.t j) x)
    (NatTrans.app (mapHorn f c) x)

Tactic:
NatTrans.congr_app c.ι_t x

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t, CategoryTheory.NatTrans.congr_app