awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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
have hy₁ : ∃ (h : x' = c),
  Eq.{u + 1} (α := Δ[c.dim + 1] _⦋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⦌)
    (cast sorry
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (x'.horn.ι.app (op ⦋c.dim + 1⦌)) :
            (a : x'.horn.toSSet _⦋c.dim + 1⦌) → Δ[x'.dim + 1] _⦋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')) :
      Δ[c.dim + 1] _⦋c.dim + 1⦌)
Tactic: rw [← NatTrans.comp_app_apply, ι_m, NatTrans.comp_app_apply, ιSigmaStdSimplex_eq_iff] at hy
Cleared hypotheses: hy
-- 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 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 :
  ∃ (h : x' = c),
    Eq.{u + 1} (α := Δ[c.dim + 1] _⦋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⦌)
      (cast ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x'.horn.ι.app (op ⦋c.dim + 1⦌)) :
              (a : x'.horn.toSSet _⦋c.dim + 1⦌) → Δ[x'.dim + 1] _⦋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')) :
        Δ[c.dim + 1] _⦋c.dim + 1⦌)
⊢ False
have hy'₁ : Membership.mem (α := Δ[x'.dim + 1] _⦋x'.dim + 1⦌) (γ := Set (Δ[x'.dim + 1] _⦋x'.dim + 1⦌))
  (x'.horn.obj (op ⦋x'.dim + 1⦌))
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x'.dim + 1⦌) ⟶ ⦋x'.dim + 1⦌) → Δ[x'.dim + 1] _⦋x'.dim + 1⦌)
      (𝟙 (unop (op ⦋x'.dim + 1⦌))) :
    Δ[x'.dim + 1] _⦋x'.dim + 1⦌)
Tactic: obtain ⟨rfl, rfl⟩ := hy
Cleared hypotheses: c, y, hy', hy
-- 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⦌) (γ := Set (f.sigmaStdSimplex j _⦋c.dim⦌))
    ((f.sigmaStdSimplex j).nonDegenerate c.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
have rw : Mono (SimplexCategory.δ c.index)
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⦌
hy :
  Eq (α := f.sigmaStdSimplex j _⦋c.dim⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
        y :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
⊢ False
have obtain : ∀ (x' : f.Cell j) (y : Δ[x'.dim + 1] _⦋c.dim⦌)
  (hy' : Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) y)
  (hy :
    Eq (α := f.sigmaStdSimplex j _⦋c.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋c.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌)) →
              (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app x'.ιSigmaHorn (op ⦋c.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (x'.horn.toSSet _⦋c.dim⦌)) →
                  (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌))
              (Subtype.mk (p := fun (x : Δ[x'.dim + 1] _⦋c.dim⦌) ↦
                Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) x) y hy') :
            (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌)) :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) →
              (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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⦌) :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))),
  False
Tactic: obtain ⟨x', ⟨y, hy'⟩, rfl⟩ := f.ιSigmaHorn_jointly_surjective y
Cleared hypotheses: y, hy
-- 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 x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) y
hy :
  Eq (α := f.sigmaStdSimplex j _⦋c.dim⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app x'.ιSigmaHorn (op ⦋c.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (x'.horn.toSSet _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌))
            (Subtype.mk (p := fun (x : Δ[x'.dim + 1] _⦋c.dim⦌) ↦
              Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) x) y hy') :
          (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋c.dim⦌)) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋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⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋c.dim⦌))
⊢ False
have hy₁ : ∃ (h : x' = c),
  Eq.{u + 1} (α := Δ[c.dim + 1] _⦋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⦌)
    (cast sorry
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (x'.horn.ι.app (op ⦋c.dim⦌)) :
            (a : x'.horn.toSSet _⦋c.dim⦌) → Δ[x'.dim + 1] _⦋c.dim⦌)
          (Subtype.mk (p := fun (x : Δ[x'.dim + 1] _⦋c.dim⦌) ↦
            Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) x) y hy')) :
      Δ[c.dim + 1] _⦋c.dim⦌)
Tactic: rw [← NatTrans.comp_app_apply, ι_m, NatTrans.comp_app_apply, ιSigmaStdSimplex_eq_iff] at hy
Cleared hypotheses: hy
-- 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 x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) y
hy :
  ∃ (h : x' = c),
    Eq.{u + 1} (α := Δ[c.dim + 1] _⦋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⦌)
      (cast ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x'.horn.ι.app (op ⦋c.dim⦌)) :
              (a : x'.horn.toSSet _⦋c.dim⦌) → Δ[x'.dim + 1] _⦋c.dim⦌)
            (Subtype.mk (p := fun (x : Δ[x'.dim + 1] _⦋c.dim⦌) ↦
              Membership.mem (γ := Set (Δ[x'.dim + 1] _⦋c.dim⦌)) (x'.horn.obj (op ⦋c.dim⦌)) x) y hy')) :
        Δ[c.dim + 1] _⦋c.dim⦌)
⊢ False
have hy'₁ : Membership.mem (α := Δ[x'.dim + 1] _⦋x'.dim⦌) (γ := Set (Δ[x'.dim + 1] _⦋x'.dim⦌)) (x'.horn.obj (op ⦋x'.dim⦌))
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x'.dim⦌) ⟶ ⦋x'.dim + 1⦌) → Δ[x'.dim + 1] _⦋x'.dim⦌)
      (SimplexCategory.δ x'.index) :
    Δ[x'.dim + 1] _⦋x'.dim⦌)
Tactic: obtain ⟨rfl, rfl⟩ := hy
Cleared hypotheses: c, y, hy', hy
-- 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 : ι
s : (range (X := f.sigmaHorn j) (f.m j)).N
⊢ ∃ (c : f.Cell j), s = Cell.type₁ f c ∨ s = Cell.type₂ f c
have obtain : ∀ (d : ℕ) (s : f.sigmaStdSimplex j _⦋d⦌)
  (hs : Membership.mem (γ := Set (f.sigmaStdSimplex j _⦋d⦌)) ((f.sigmaStdSimplex j).nonDegenerate d) s)
  (hs' : s ∉ (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)),
  ∃ (c : f.Cell j), N.mk s hs hs' = Cell.type₁ f c ∨ N.mk s hs hs' = Cell.type₂ f c
Tactic: obtain ⟨d, s, hs, hs', rfl⟩ := s.mk_surjective
Cleared hypotheses: 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 : ι
d : ℕ
s : f.sigmaStdSimplex j _⦋d⦌
hs : Membership.mem (γ := Set (f.sigmaStdSimplex j _⦋d⦌)) ((f.sigmaStdSimplex j).nonDegenerate d) s
hs' : s ∉ (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
⊢ ∃ (c : f.Cell j), N.mk s hs hs' = Cell.type₁ f c ∨ N.mk s hs hs' = Cell.type₂ f c
have obtain : ∀ (x : f.Cell j) (s : Δ[x.dim + 1] _⦋d⦌)
  (hs :
    Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
      ((f.sigmaStdSimplex j).nonDegenerate 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⦌)))
  (hs' :
    ((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⦌)) ∉
      (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)),
  ∃ (c : f.Cell j),
    N.mk
          ((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)
          hs hs' =
        Cell.type₁ f c ∨
      N.mk
          ((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)
          hs hs' =
        Cell.type₂ f c
Tactic: obtain ⟨x, s, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective s
Cleared hypotheses: s, hs, 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 : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate 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⦌))
hs' :
  ((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⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((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)
          hs hs' =
        Cell.type₁ f c ∨
      N.mk
          ((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)
          hs hs' =
        Cell.type₂ f c
have hs'₁ : s ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
Tactic: replace hs' : s ∉ (horn _ x.index).obj _ :=
    fun h ↦ hs' ⟨x.ιSigmaHorn.app _ ⟨_, h⟩, by rw [← NatTrans.comp_app_apply]; simp⟩
-- 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 : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate 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⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs'_1 :
  ((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⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs hs'_1 =
        Cell.type₂ f c
have hs₁ : Mono g
Tactic: rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply] at hs
Cleared hypotheses: hs'_1, 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 : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate 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⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs : Mono g
hs'_1 :
  ((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⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c
have inl : ∀ (hd : d < x.dim + 1),
  ∃ (c : f.Cell j),
    N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c
Tactic: obtain hd | rfl := (SimplexCategory.le_of_mono g).lt_or_eq
-- 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 : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate 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⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs : Mono g
hs'_1 :
  ((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⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd : d < x.dim + 1
⊢ ∃ (c : f.Cell j),
    N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((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⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c
have hd₁ : d ≤ x.dim
Tactic: rw [Nat.lt_succ_iff] at hd
Cleared hypotheses: hd