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
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
⊢ ∃ (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),
  ∃ (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 := hd.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
⊢ Eq (α := f.sigmaHorn j ⟶ (f.filtration (Order.succ j)).toSSet) (f.t j ≫ homOfLE ⋯) (f.m j ≫ f.b j)
have h : ∀ (c : f.Cell j),
  Eq (α := c.horn.toSSet ⟶ (f.filtration (Order.succ j)).toSSet)
    (CategoryStruct.comp (Y := ∐ fun (c : f.Cell j) ↦ c.horn.toSSet)
      (Sigma.ι (C := SSet) (fun (c : f.Cell j) ↦ c.horn.toSSet) c) (f.t j ≫ homOfLE sorry))
    (CategoryStruct.comp (Y := ∐ fun (c : f.Cell j) ↦ c.horn.toSSet)
      (Sigma.ι (C := SSet) (fun (c : f.Cell j) ↦ c.horn.toSSet) c) (f.m j ≫ f.b j))
Tactic: ext c : 1
-- 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 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsLimit (F :=
    cospan (Z := (f.filtration (Order.succ j)).toSSet) (homOfLE ⋯) (f.b j) ⋙
      CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
    (Functor.mapCone (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (PullbackCone.mk (f.t j) (f.m j) ⋯))
have refine : IsPullback (P := Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)) (Z :=
  Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet)
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j))
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE sorry))
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j))
Tactic: refine (isLimitMapConePullbackConeEquiv _ _).symm
      (IsPullback.isLimit ?_)
-- 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 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x : SimplexCategoryᵒᵖ
d : ℕ
y : (↑((f.filtration j).obj (op ⦋d⦌)) : Type u)
b : f.sigmaStdSimplex j _⦋d⦌
h :
  Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x) (↑y : X _⦋d⦌) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
        (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      b)
⊢ ∃ (x₁ : f.sigmaHorn j _⦋d⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.t j) (op ⦋d⦌)) :
            (a : f.sigmaHorn j _⦋d⦌) → (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
          x₁ =
        y ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋d⦌)) :
            (a : f.sigmaHorn j _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
          x₁ =
        b
have obtain : ∀ (x : f.Cell j) (b : Δ[x.dim + 1] _⦋d⦌)
  (h :
    Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
        Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x) (↑y : X _⦋d⦌) sorry)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
          (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
        ((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⦌))
          b))),
  ∃ (x₁ : f.sigmaHorn j _⦋d⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.t j) (op ⦋d⦌)) :
            (a : f.sigmaHorn j _⦋d⦌) → (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
          x₁ =
        y ∧
      Eq (α := f.sigmaStdSimplex j _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋d⦌)) :
              (a : f.sigmaHorn j _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
            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⦌))
            b :
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
Tactic: obtain ⟨x, b, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective b
Cleared hypotheses: b, 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
y : (↑((f.filtration j).obj (op ⦋d⦌)) : Type u)
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h :
  Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x) (↑y : X _⦋d⦌) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
        (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      ((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⦌))
        b))
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b
have obtain : ∀ (y : X _⦋d⦌) (hy : Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) y)
  (h :
    Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
        Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x)
        (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) x) y
              hy) :
          X _⦋d⦌)
        sorry)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
          (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
        ((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⦌))
          b))),
  Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b
Tactic: obtain ⟨y, hy⟩ := y
Cleared hypotheses: y, 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
y : X _⦋d⦌
hy : Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) y
h :
  Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x)
      (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) x) y
            hy) :
        X _⦋d⦌)
      ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
        (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      ((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⦌))
        b))
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b
have simp : Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (((f.filtration j).preimage x.map).obj (op ⦋d⦌)) b
Tactic: simp only [← x.preimage_filtration_map]
-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
y : X _⦋d⦌
hy : Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) y
h :
  Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x)
      (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) x) y
            hy) :
        X _⦋d⦌)
      ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
        (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      ((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⦌))
        b))
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (((f.filtration j).preimage x.map).obj (op ⦋d⦌)) b
have h₁ : (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦
        Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x)
        (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) x) y
              hy) :
          X _⦋d⦌)
        sorry) :
    X _⦋d⦌) =
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
          (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
        ((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⦌))
          b)) :
    X _⦋d⦌)
Tactic: rw [Subtype.ext_iff] at h
Cleared hypotheses: h
-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
y : X _⦋d⦌
hy : Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌)) y
h :
  y =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
            (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : Δ[x.dim + 1] _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
            b)) :
      X _⦋d⦌)
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (((f.filtration j).preimage x.map).obj (op ⦋d⦌)) b
have hy₁ : Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌))
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
          (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
            (a : Δ[x.dim + 1] _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
          b)) :
    X _⦋d⦌)
Tactic: subst h
Cleared hypotheses: y, hy, 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
hy :
  Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
            (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : Δ[x.dim + 1] _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
            b)) :
      X _⦋d⦌)
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (((f.filtration j).preimage x.map).obj (op ⦋d⦌)) b
have rwa : ∀
  (hy :
    Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration j).obj (op ⦋d⦌))
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app x.mapToSucc (op ⦋d⦌)) :
              (a : Δ[x.dim + 1] _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
            b) :
        X _⦋d⦌)),
  Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (((f.filtration j).preimage x.map).obj (op ⦋d⦌)) b
Tactic: rwa [x.ι_b_app_apply] 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
y : (↑((f.filtration j).obj (op ⦋d⦌)) : Type u)
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h :
  Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x) (↑y : X _⦋d⦌) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
        (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      ((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⦌))
        b))
⊢ ∃ (x₁ : f.sigmaHorn j _⦋d⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.t j) (op ⦋d⦌)) :
            (a : f.sigmaHorn j _⦋d⦌) → (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
          x₁ =
        y ∧
      Eq (α := f.sigmaStdSimplex j _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋d⦌)) :
              (a : f.sigmaHorn j _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
            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⦌))
            b :
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
have hb : Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b
Tactic: have hb : b ∈ Λ[_, x.index].obj _ := by
      obtain ⟨y, hy⟩ := y
      simp only [← x.preimage_filtration_map]
      rw [Subtype.ext_iff] at h
      dsimp at h
      subst h
      rwa [x.ι_b_app_apply] at 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x_1 : SimplexCategoryᵒᵖ
d : ℕ
y : (↑((f.filtration j).obj (op ⦋d⦌)) : Type u)
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h :
  Eq (α := (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) ((f.filtration (Order.succ j)).obj (op ⦋d⦌)) x) (↑y : X _⦋d⦌) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋d⦌)) :
        (a : f.sigmaStdSimplex j _⦋d⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      ((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⦌))
        b))
hb : Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b
⊢ ∃ (x₁ : f.sigmaHorn j _⦋d⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.t j) (op ⦋d⦌)) :
            (a : f.sigmaHorn j _⦋d⦌) → (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
          x₁ =
        y ∧
      Eq (α := f.sigmaStdSimplex j _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋d⦌)) :
              (a : f.sigmaHorn j _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
            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⦌))
            b :
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
have refine_1 : (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.t j) (op ⦋d⦌)) :
      (a : f.sigmaHorn j _⦋d⦌) → (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app x.ιSigmaHorn (op ⦋d⦌)) :
        (a : (fun (X : Type u) ↦ X) (x.horn.toSSet _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋d⦌))
      (Subtype.mk (p := fun (x_2 : Δ[x.dim + 1] _⦋d⦌) ↦
        Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (x.horn.obj (op ⦋d⦌)) x_2) b hb)) =
  y
Tactic: refine ⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, ?_⟩
-- 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 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
    (Set.range (ι := (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (homOfLE ⋯) d)) :
          (a : (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d)) →
            (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)) ⊔
      Set.range (ι := (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d)) :
          (a : (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d)) →
            (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
    Set.univ
have h : ∀ (x : X.obj d) (hx : x ∈ (f.filtration (Order.succ j)).obj d),
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
      (Set.range (ι := (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (homOfLE sorry) d)) :
            (a : (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d)) →
              (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)) ⊔
        Set.range (ι := (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d)) :
            (a : (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d)) →
              (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
      (Subtype.mk (p := fun (x : X.obj d) ↦ x ∈ (f.filtration (Order.succ j)).obj d) x hx) ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d))) Set.univ
      (Subtype.mk (p := fun (x : X.obj d) ↦ x ∈ (f.filtration (Order.succ j)).obj d) x hx)
Tactic: ext ⟨x, hx⟩