-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw :
  Eq (α := Submodule R (Module.Dual R M × M)) (ker (dualProd R M)) ⊥ ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))
rw₁ rw₂ rw₃ :
  Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × M →ₗ[R] R)
      (⇑(dualProd R M) : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))
rw₄ rw₅ :
  Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × M →ₗ[R] R)
      (⇑(dualProd R M) : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))
rw₆ :
  let e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
    LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
      Module.dualProdDualEquivDual R (Module.Dual R M) M;
  Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × Module.Dual R (Module.Dual R M))
      (Function.comp (β := Module.Dual R (Module.Dual R M × M))
        (⇑e.symm : (a : Module.Dual R (Module.Dual R M × M)) → Module.Dual R M × Module.Dual R (Module.Dual R M))
        (⇑(dualProd R M) : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R)) ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))
⊢ SeparatingLeft (M₁ := Module.Dual R M × M) (dualProd R M) ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))
have rw₇ : let e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M;
Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × Module.Dual R (Module.Dual R M))
    (⇑((↑e.symm : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
          dualProd R M) :
      (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) ↔
  Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
    (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))
Tactic: classical
  rw [separatingLeft_iff_ker_eq_bot, ker_eq_bot]
  let e := LinearEquiv.prodComm R _ _ ≪≫ₗ Module.dualProdDualEquivDual R (Module.Dual R M) M
  let h_d := e.symm.toLinearMap.comp (dualProd R M)
  refine (Function.Injective.of_comp_iff e.symm.injective
    (dualProd R M)).symm.trans ?_
  rw [← LinearEquiv.coe_toLinearMap, ← coe_comp]
  change Function.Injective h_d ↔ _
  have : h_d = prodMap id (Module.Dual.eval R M) := by
    refine ext fun x => Prod.ext ?_ ?_
    · ext
      dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
      simp
    · ext
      dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
      simp
  rw [this, coe_prodMap]
  refine Prod.map_injective.trans ?_
  exact and_iff_right Function.injective_id