-- 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 : ℕ
⊢ 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₃
have 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⦌) 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))
        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
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 ↦ ?_⟩