-- 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 :
  ∀ (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
⊢ Eq (α := f.sigmaHorn j _⦋d⦌ ⟶ (↑((f.filtration (Order.succ j)).obj (op ⦋d⦌)) : Type u))
      (NatTrans.app (f.t j) (op ⦋d⦌) ≫
        ↾fun (x : (↑((f.filtration 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) (↑x : X _⦋d⦌) ⋯)
      (NatTrans.app (f.m j) (op ⦋d⦌) ≫ NatTrans.app (f.b j) (op ⦋d⦌)) ∧
    (∀ (x₁ y₁ : f.sigmaHorn j _⦋d⦌),
        Eq (α := (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
              ((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₁ :
                (↑((f.filtration j).obj (op ⦋d⦌)) : Type u))
              ((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))
                  y₁ :
                (↑((f.filtration j).obj (op ⦋d⦌)) : Type u)) ∧
            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) (NatTrans.app (f.m j) (op ⦋d⦌)) :
                    (a : f.sigmaHorn j _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
                  y₁ :
                f.sigmaStdSimplex j _⦋d⦌) →
          x₁ = y₁) ∧
      ∀ (x₂ : (↑((f.filtration j).obj (op ⦋d⦌)) : Type u)) (x₃ : f.sigmaStdSimplex j _⦋d⦌),
        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) (↑x₂ : 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))
              x₃) →
          ∃ (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₁ =
                x₂ ∧
              (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.m j) (op ⦋d⦌)) :
                    (a : f.sigmaHorn j _⦋d⦌) → f.sigmaStdSimplex j _⦋d⦌)
                  x₁ =
                x₃

Tactic:
refine ⟨congr_app (f.w j) (op ⦋d⦌),
      fun a₁ a₂ h ↦ (mono_iff_injective _).mp
        ((NatTrans.mono_iff_mono_app (f.m j)).mp inferInstance _) h.2, fun y b h ↦ ?_⟩