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 : P.IsProper
inst_2 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
⊢ LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (i : ι), f.filtration i)
have rw : ∀ (s : X.N), s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ (i : ι), f.filtration i
Tactic: rw [N.subcomplex_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 ι
s : A.N
h : s.subcomplex ≤ ⊤
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i
have notMem : ∀ (t : (↑P.II : Type u)) (ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)),
  s.subcomplex ≤ ⨆ (i : ι), f.filtration i
Tactic: obtain ⟨t, ht⟩ := P.exists_or s
-- 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 ι
s : A.N
h : s.subcomplex ≤ ⊤
t : (↑P.II : Type u)
ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i
have notMem : s.subcomplex ≤
  S.subcomplex
    (N.toS
      (N.toN (A := A)
        (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := sorry })) :
          A.N)))
Tactic: refine le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (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 : P.IsProper
inst_2 : OrderBot ι
inst_3 : SuccOrder ι
inst_4 : NoMaxOrder ι
s : A.N
h : s.subcomplex ≤ ⊤
t : (↑P.II : Type u)
ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
⊢ s.subcomplex ≤
    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)))
have notMem : (↑t : A.N).subcomplex ≤ ⊤ →
  (↑t : A.N).subcomplex ≤
    S.subcomplex
      (N.toS
        (N.toN (A := A)
          (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := sorry })) :
            A.N)))
Tactic: obtain rfl | rfl := ht
Cleared hypotheses: s, h, ht
-- 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 ι
s : A.N
h : s.subcomplex ≤ ⊤
t : (↑P.II : Type u)
ht : s = (↑t : A.N) ∨ s = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
notMem :
  (↑t : A.N).subcomplex ≤ ⊤ →
    (↑t : A.N).subcomplex ≤
      S.subcomplex
        (N.toS
          (N.toN (A := A)
            (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u))
                  (Cell.s.{v, u} (ι := ι) (f := f) { s := t, rank_s := ⋯ })) :
              A.N)))
⊢ 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)))
have notMem₁ : LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)))) ⊤ →
  LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))))
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))))
Tactic: obtain rfl | rfl := ht
Cleared hypotheses: s, h, ht
-- 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 ι
s : X.N
h : s.subcomplex ≤ ⊤
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i
have mem : ∀ (hs : s.subcomplex ≤ A), s.subcomplex ≤ ⨆ (i : ι), f.filtration i
Tactic: cases s using SSet.Subcomplex.N.cases A with
  | mem s hs => exact hs.trans (le_trans (by simp) (le_iSup _ ⊥))
  | notMem s =>
    obtain ⟨t, ht⟩ := P.exists_or s
    refine le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _))
    obtain rfl | rfl := ht
    · exact P.le t
    · rfl
-- 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 ι
s : X.N
h : s.subcomplex ≤ ⊤
mem : ∀ (hs : s.subcomplex ≤ A), s.subcomplex ≤ ⨆ (i : ι), f.filtration i
⊢ s.subcomplex ≤ ⨆ (i : ι), f.filtration i
have notMem : ∀ (s : A.N), s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ (i : ι), f.filtration i
Tactic: cases s using SSet.Subcomplex.N.cases A with
  | mem s hs => exact hs.trans (le_trans (by simp) (le_iSup _ ⊥))
  | notMem s =>
    obtain ⟨t, ht⟩ := P.exists_or s
    refine le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _))
    obtain rfl | rfl := ht
    · exact P.le t
    · rfl
Cleared hypotheses: s, 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 ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
y : f.Cell j
t : Δ[y.dim + 1] _⦋d⦌
h : x = y
⊢ Δ[x.dim + 1] _⦋d⦌ = Δ[y.dim + 1] _⦋d⦌
have rw : Δ[y.dim + 1] _⦋d⦌ = Δ[y.dim + 1] _⦋d⦌
Tactic: rw [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 ι
inst_1 : P.IsProper
j : ι
c : f.Cell j
⊢ Mono c.ιSigmaStdSimplex
have rw : ∀ (k : SimplexCategoryᵒᵖ), Mono (c.ιSigmaStdSimplex.app k)
Tactic: rw [NatTrans.mono_iff_mono_app]
-- 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
j : ι
c : f.Cell j
d : ℕ
⊢ Mono (X := Δ[c.dim + 1] _⦋d⦌) (c.ιSigmaStdSimplex.app (op ⦋d⦌))
have 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⦌))
Tactic: rw [mono_iff_injective]
-- 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
j : ι
c : f.Cell j
⊢ (f.filtration j).preimage c.map = c.horn
have a : (f.filtration j).preimage c.map ≤ c.horn
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 : P.IsProper
j : ι
c : f.Cell j
a : (f.filtration j).preimage c.map ≤ c.horn
⊢ (f.filtration j).preimage c.map = c.horn
have a₁ : c.horn ≤ (f.filtration j).preimage c.map
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 : P.IsProper
j : ι
c : f.Cell j
⊢ c.horn ≤ (f.filtration j).preimage c.map
have a : ∀ (s : X.N), s.subcomplex ≤ c.horn.image c.map → s.subcomplex ≤ f.filtration j
Tactic: rw [← Subcomplex.image_le_iff, N.subcomplex_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
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
⊢ s.subcomplex ≤ f.filtration j
have 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
Tactic: obtain ⟨t, ht⟩ := P.exists_or s
-- 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
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 j
have a : s.subcomplex ≤ f.filtration (f.rank c.s)
Tactic: rw [← c.rank_s]
-- 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
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)
have 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 := sorry })) :
          A.N)))
Tactic: refine le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (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 ι
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)))
⊢ s.subcomplex ≤ f.filtration (f.rank c.s)
have a₁ : P.AncestralRel t c.s
Tactic: refine le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (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 ι
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 ≤
    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)))
have 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 := sorry })) :
            A.N)))
Tactic: obtain rfl | rfl := ht
Cleared hypotheses: s, hs, ht
-- 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
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)))
⊢ 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)))
have 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 := sorry })) :
            A.N))))
Tactic: obtain rfl | rfl := ht
Cleared hypotheses: s, hs, ht
-- 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
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
have inl : ∀ (hs : (↑t : A.N).subcomplex ≤ c.horn.image c.map), (↑t : A.N).subcomplex ≤ c.horn.image c.map
Tactic: obtain rfl | rfl := ht
Cleared hypotheses: s, hs, ht
-- 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
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
⊢ (↑t : A.N).subcomplex ≤ c.horn.image c.map
have 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
Tactic: obtain rfl | rfl := ht
Cleared hypotheses: s, hs, ht
-- 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
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
have 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)))
Tactic: refine le_trans ?_ hs
-- 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 ι
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)
⊢ P.AncestralRel t c.s
have hs₁ : (↑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
Cleared hypotheses: hs
-- 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
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
have a : t ≠ c.s
Tactic: refine ⟨?_, ?_⟩
-- 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
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
⊢ P.AncestralRel t c.s
have a₁ : (↑t : A.N) < (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)
Tactic: refine ⟨?_, ?_⟩
-- 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
j : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
⊢ s.subcomplex ≤ f.filtration j
have a : ∀ (hs' : s.subcomplex ≤ A), 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)
-- 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
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
⊢ s.subcomplex ≤ f.filtration j
have a₁ : ∀ (s : A.N) (hs : s.subcomplex ≤ c.horn.image c.map), 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)
Cleared hypotheses: s, hs
-- 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
j : ι
c : f.Cell j
⊢ Membership.mem (α := f.sigmaStdSimplex j _⦋c.dim + 1⦌) (γ := Set (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
    ((f.sigmaStdSimplex j).nonDegenerate (c.dim + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim + 1⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
            (𝟙 (unop (op ⦋c.dim + 1⦌))) :
          Δ[c.dim + 1] _⦋c.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
have rw : Mono (𝟙 (unop (op ⦋c.dim + 1⦌)))
Tactic: rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
      Equiv.apply_symm_apply]
-- 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
j : ι
c : f.Cell j
y : f.sigmaHorn j _⦋c.dim + 1⦌
hy :
  Eq (α := f.sigmaStdSimplex j _⦋c.dim + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋c.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
        y :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim + 1⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
            (𝟙 (unop (op ⦋c.dim + 1⦌))) :
          Δ[c.dim + 1] _⦋c.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
⊢ False
have obtain : ∀ (x' : f.Cell j) (y : Δ[x'.dim + 1] _⦋c.dim + 1⦌)
  (hy' : Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim + 1⦌)) (x'.horn.obj (op ⦋c.dim + 1⦌)) y)
  (hy :
    Eq (α := f.sigmaStdSimplex j _⦋c.dim + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋c.dim + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim + 1⦌)) →
              (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app x'.ιSigmaHorn (op ⦋c.dim + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) (x'.horn.toSSet _⦋c.dim + 1⦌)) →
                  (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim + 1⦌))
              (Subtype.mk (p := fun (x : Δ[x'.dim + 1] _⦋c.dim + 1⦌) ↦
                Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim + 1⦌)) (x'.horn.obj (op ⦋c.dim + 1⦌)) x) y hy') :
            (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim + 1⦌)) :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim + 1⦌)) →
              (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))
          ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim + 1⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim + 1⦌)
              (𝟙 (unop (op ⦋c.dim + 1⦌))) :
            Δ[c.dim + 1] _⦋c.dim + 1⦌) :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim + 1⦌))),
  False
Tactic: obtain ⟨x', ⟨y, hy'⟩, rfl⟩ := f.ιSigmaHorn_jointly_surjective y
Cleared hypotheses: y, hy