-- 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
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
refine_2 :
  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⦌)
        ((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) :
          (fun (X : Type u) ↦ X) (f.sigmaHorn j _⦋d⦌)) :
      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 ∧
      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:
refine ⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, ?_⟩