-- 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 + n) →ₗ[R] ↥R[X]_(m + n))
    ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          ((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)
          (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)))) :
      ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
    ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + 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 + n) →ₗ[R] ↥R[X]_(m + n))
rwa :
  ∀
    (this :
      Eq (α := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        ((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 + 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 + n) →ₗ[R] ↥R[X]_(m + 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.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
      HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
rwa₁ :
  ∀
    (this :
      Eq (α := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (f.sylvesterMap g hf hg ∘ₗ
          (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 + n) →ₗ[R] ↥R[X]_(m + 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.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
      HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
rwa₂ :
  ∀
    (this :
      f.sylvesterMap g hf hg ∘ₗ
          (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))) =
        HSMul.hSMul (α := R) (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
          (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)))
          ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) 1)),
    f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
      HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
rwa₃ :
  ∀
    (this :
      f.sylvesterMap g hf hg ∘ₗ
          (Matrix.toLin b₂ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_m × ↥R[X]_n)
            (f.sylvester g m n).adjugate =
        HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.sylvester g m n).det
          ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) 1)),
    f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
      HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
    HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
have rwa₄ : ∀
  (this :
    f.sylvesterMap g hf hg ∘ₗ
        (Matrix.toLin b₂ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_m × ↥R[X]_n)
          (f.sylvester g m n).adjugate =
      HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.sylvester g m n).det LinearMap.id),
  f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
    HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + 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