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 ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ Eq (α := Δ[c.dim + 1] ⟶ (f.filtration (Order.succ j)).toSSet) (c.ιSigmaStdSimplex ≫ f.b j) c.mapToSucc

Tactic:
simp [b, Sigma.ι_desc]

Premises used: SSet.Subcomplex.Pairing.RankFunction.b, 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c : f.Cell j
x : SimplexCategoryᵒᵖ
⊢ Eq (α := Δ[c.dim + 1].obj x ⟶ (f.filtration (Order.succ j)).toSSet.obj x)
    (c.ιSigmaStdSimplex.app x ≫ NatTrans.app (f.b j) x) (NatTrans.app c.mapToSucc x)

Tactic:
NatTrans.congr_app c.ι_b x

Premises used: CategoryTheory.NatTrans.congr_app, SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b
-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
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 ⋯))
      (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))
⊢ Eq (α := f.sigmaHorn j ⟶ (f.filtration (Order.succ j)).toSSet) (f.t j ≫ homOfLE ⋯) (f.m j ≫ f.b j)

Tactic:
ext c : 1
-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
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 ⋯))
    (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:
simp [← cancel_mono (Subcomplex.ι _)]

Premises used: CategoryTheory.cancel_mono, SSet.Subcomplex.ι
-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x : SimplexCategoryᵒᵖ
d : ℕ
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 ⋯))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j))
⊢ 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) ⋯))

Tactic:
refine (isLimitMapConePullbackConeEquiv _ _).symm
      (IsPullback.isLimit ?_)

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.IsPullback.isLimit
-- 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
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)
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⦌) ⋯)
        ((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⦌))
⊢ ∃ (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

Tactic:
obtain ⟨x, b, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective b

Premises used: SSet.Subcomplex.Pairing.RankFunction.ιSigmaStdSimplex_jointly_surjective, 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
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))
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⦌)
          ⋯)
        ((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
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b

Tactic:
obtain ⟨y, hy⟩ := y
-- 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
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))
simp : Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (((f.filtration j).preimage x.map).obj (op ⦋d⦌)) b
⊢ Membership.mem (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌)) b

Tactic:
simp only [← x.preimage_filtration_map]

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.preimage_filtration_map
-- 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
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))
⊢ (↑(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⦌)
          ⋯) :
      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

Premises used: Subtype.ext_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
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 _⦋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
-- 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
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⦌)
rwa rwa₁ rwa₂ 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
⊢ 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

Premises used: SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply
-- 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
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

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
-- 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
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⦌))

Tactic:
⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Subtype.mk, And.intro, Exists.intro, DFunLike.coe, CategoryTheory.NatTrans.app, SSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaHorn
-- 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
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
⊢ (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:
simpa only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
        x.ι_b_app_apply, x.ι_t_app_apply] using h.symm

Premises used: CategoryTheory.Subfunctor.toFunctor_obj, SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_apply, Subtype.ext_iff, SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply, 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
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
⊢ Eq (α := f.sigmaStdSimplex j _⦋d⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (x.ιSigmaHorn ≫ f.m j) (op ⦋d⦌)) :
          (a : x.horn.toSSet _⦋d⦌) → f.sigmaStdSimplex 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) :
      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:
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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
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 ⋯) 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)
⊢ 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

Tactic:
ext ⟨x, hx⟩