-- Mathlib/LinearAlgebra/QuadraticForm/Dual.lean
theorem separatingLeft_dualProd :
    (dualProd R M).SeparatingLeft ↔ Function.Injective (Module.Dual.eval R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective (Prod.map ⇑id ⇑(Module.Dual.eval R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
refine Prod.map_injective.trans ?_

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective ⇑id ∧ Function.Injective ⇑(Module.Dual.eval R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Proof state:
case refine_2.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
x✝ : Module.Dual R M
⊢ x✝ x.2 + x.1 0 = x✝ x.2

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective ⇑h_d ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
rw [this, coe_prodMap]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective (Prod.map ⇑id ⇑(Module.Dual.eval R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective (⇑e.symm ∘ ⇑(dualProd R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
rw [← LinearEquiv.coe_toLinearMap, ← coe_comp]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective ⇑(↑e.symm ∘ₗ dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ h_d = id.prodMap (Module.Dual.eval R M)

Tactic:
refine ext fun x => Prod.ext ?_ ?_

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).1 = ((id.prodMap (Module.Dual.eval R M)) x).1

case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).2 = ((id.prodMap (Module.Dual.eval R M)) x).2

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).1 = ((id.prodMap (Module.Dual.eval R M)) x).1

Tactic:
ext

Result:
case refine_1.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
x✝ : M
⊢ (h_d x).1 x✝ = ((id.prodMap (Module.Dual.eval R M)) x).1 x✝

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
this : h_d = id.prodMap (Module.Dual.eval R M)
⊢ Function.Injective ⇑id ∧ Function.Injective ⇑(Module.Dual.eval R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
exact and_iff_right Function.injective_id

Result:
no goals