-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  Eq (α := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
    ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
        (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.adjugate
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg) :
            Matrix (Fin (m + n)) (Fin (m + n)) R)) :
      ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
    ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
        (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.det (n := Fin (m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          1) :
      ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
rwa :
  ∀
    (this :
      Eq (α := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
        ((Matrix.toLin b₂ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_m × ↥R[X]_n)
            (Matrix.adjugate
              ((LinearMap.toMatrix b₁ b₂ :
                  (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
                (f.sylvesterMap g hf hg))) ∘ₗ
          (Matrix.toLin b₁ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
        ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
          (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
            (Matrix.det (n := Fin (m + n))
              ((LinearMap.toMatrix b₁ b₂ :
                  (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
                (f.sylvesterMap g hf hg)))
            1))),
    f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg =
      HSMul.hSMul (β := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n) (f.resultant g m n) LinearMap.id
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg =
    HSMul.hSMul (β := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n) (f.resultant g m n) LinearMap.id
have rwa₁ : ∀
  (this :
    Eq (α := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
      ((Matrix.toLin b₂ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_m × ↥R[X]_n)
          (Matrix.adjugate
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg))) ∘ₗ
        f.sylvesterMap g hf hg)
      ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
        (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.det (n := Fin (m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          1))),
  f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg =
    HSMul.hSMul (β := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n) (f.resultant g m n) LinearMap.id
Tactic: rwa [Matrix.toLin_mul b₁ b₂ b₁, Matrix.toLin_toMatrix, map_smul,
    toMatrix_sylvesterMap', Matrix.toLin_one, ← resultant] at this
Cleared hypotheses: this