-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
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))
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))
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;
  let h_d :=
    (↑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;
  Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × Module.Dual R (Module.Dual R M))
      (⇑h_d : (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))
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;
  let h_d :=
    (↑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;
  ∀ (this : h_d = prodMap id (Module.Dual.eval R M)),
    Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × Module.Dual R (Module.Dual R M))
        (⇑h_d : (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))
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;
  let h_d :=
    (↑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;
  ∀ (this : h_d = prodMap id (Module.Dual.eval R M)),
    Function.Injective (α := Module.Dual R M × M) (β := Module.Dual R M × Module.Dual R (Module.Dual R M))
        (Prod.map (⇑id : (a : Module.Dual R M) → Module.Dual R M)
          (⇑(Module.Dual.eval R M) : (a : 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))
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;
  let h_d :=
    (↑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;
  ∀ (this : h_d = prodMap id (Module.Dual.eval R M)),
    Function.Injective (α := Module.Dual R M) (β := Module.Dual R M) (⇑id : (a : Module.Dual R M) → 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)) ↔
      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))

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

Premises used: LinearMap.ker_eq_bot, and_iff_right, Function.injective_id, LinearMap.coe_comp, Prod.map_injective, LinearMap.coe_prodMap, Iff.trans, LinearEquiv.coe_toLinearMap, LinearMap.separatingLeft_iff_ker_eq_bot