awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
S : Type u_5
inst_6 : CommSemiring S
inst_7 : Algebra S R
inst_8 : Module S N
inst_9 : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ Eq.{u_4 + 1} (α := N)
    (((((s • Q).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) i : M) :
      N)
    ((((s • Q.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) i : M) :
      N)

Tactic:
simp [toBilin_apply]

Premises used: QuadraticMap.toBilin_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
S : Type u_5
inst_6 : CommSemiring S
inst_7 : Algebra S R
inst_8 : Module S N
inst_9 : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ Eq.{u_4 + 1} (α := N)
    (((((s • Q).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((s • Q.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)

Tactic:
simp [h.ne', h.not_gt, toBilin_apply]

Premises used: QuadraticMap.toBilin_apply, LT.lt.ne', LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Complex
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module ℂ M
inst_2 : FiniteDimensional ℂ M
Q : QuadraticForm ℂ M
hQ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_1, u_1} (R := ℂ) (R₁ := ℂ) (R₂ := ℂ) (M := ℂ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℂ) (I₂ := RingHom.id ℂ) ((associated : (a : QuadraticMap ℂ M ℂ) → LinearMap.BilinMap ℂ M ℂ) Q)
⊢ Equivalent (M₂ := Fin (Module.finrank ℂ M) → ℂ) Q (weightedSumSquares (S := ℂ) ℂ 1)

Tactic:
equivalent_weightedSumSquares_of_isAlgClosed Q hQ

Premises used: QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Complex
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module ℂ M
inst_2 : FiniteDimensional ℂ M
Q₁ Q₂ : QuadraticForm ℂ M
hQ₁ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_1, u_1} (R := ℂ) (R₁ := ℂ) (R₂ := ℂ) (M := ℂ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℂ) (I₂ := RingHom.id ℂ) ((associated : (a : QuadraticMap ℂ M ℂ) → LinearMap.BilinMap ℂ M ℂ) Q₁)
hQ₂ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_1, u_1} (R := ℂ) (R₁ := ℂ) (R₂ := ℂ) (M := ℂ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℂ) (I₂ := RingHom.id ℂ) ((associated : (a : QuadraticMap ℂ M ℂ) → LinearMap.BilinMap ℂ M ℂ) Q₂)
⊢ Equivalent Q₁ Q₂

Tactic:
equivalent_of_isAlgClosed Q₁ Q₂ hQ₁ hQ₂

Premises used: QuadraticForm.equivalent_of_isAlgClosed
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsSymm (M := Module.Dual R M × M) (dualProd R M)

Tactic:
⟨fun _x _y => add_comm _ _⟩

Premises used: LinearMap.fst, LinearMap.applyₗ, LinearMap.snd, add_comm, LinearMap.comp, LinearMap.IsSymm.mk, LinearMap.flip, DFunLike.coe, Module.Dual, LinearMap.compl₂
-- 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 :
  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))
⊢ 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:
rw [separatingLeft_iff_ker_eq_bot, ker_eq_bot]

Premises used: LinearMap.ker_eq_bot, LinearMap.separatingLeft_iff_ker_eq_bot
-- 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
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 : 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 × 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))

Tactic:
(Function.Injective.of_comp_iff e.symm.injective
    (dualProd R M)).symm.trans ?_

Premises used: LinearEquiv.symm, LinearMap.dualProd, Iff.trans, LinearEquiv.injective, Function.Injective.of_comp_iff, DFunLike.coe, Iff.symm
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
refine :
  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))
⊢ 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))

Tactic:
refine (Function.Injective.of_comp_iff e.symm.injective
    (dualProd R M)).symm.trans ?_

Premises used: LinearEquiv.symm, LinearMap.dualProd, Iff.trans, LinearEquiv.injective, Function.Injective.of_comp_iff, DFunLike.coe, Iff.symm
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
rw :
  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))
⊢ 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))

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

Premises used: LinearMap.coe_comp, LinearEquiv.coe_toLinearMap
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
change :
  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))
⊢ 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:
change Function.Injective h_d ↔ _

Premises used: Function.Injective, DFunLike.coe
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
⊢ h_d = prodMap id (Module.Dual.eval R M)

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

Premises used: LinearMap.ext, Prod.ext
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
refine_1 :
  ∀ (x : Module.Dual R M × M),
    Eq (α := Module.Dual R M)
      ((h_d : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) x).1
      ((prodMap id (Module.Dual.eval R M) :
            (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
          x).1
refine_2 :
  ∀ (x : Module.Dual R M × M),
    Eq (α := 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)) x).2
      ((prodMap id (Module.Dual.eval R M) :
            (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
          x).2
⊢ h_d = prodMap id (Module.Dual.eval R M)

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

Premises used: LinearMap.ext, Prod.ext
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
x : Module.Dual R M × M
refine_1 :
  ∀ (x_1 : M),
    Eq.{u_1 + 1} (α := R)
      ((((h_d : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) x).1 : (a : M) → R) x_1 :
        R)
      ((((prodMap id (Module.Dual.eval R M) :
                  (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
                x).1 :
            (a : M) → R)
          x_1 :
        R)
⊢ Eq (α := Module.Dual R M) ((h_d : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) x).1
    ((prodMap id (Module.Dual.eval R M) : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
        x).1

Tactic:
ext
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
x : Module.Dual R M × M
x_1 : M
refine_1 : HAdd.hAdd (α := R) (β := R) (0 : R) ((x.1 : (a : M) → R) x_1 : R) = (x.1 : (a : M) → R) x_1
⊢ Eq.{u_1 + 1} (α := R)
    ((((h_d : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) x).1 : (a : M) → R) x_1 :
      R)
    ((((prodMap id (Module.Dual.eval R M) :
                (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
              x).1 :
          (a : M) → R)
        x_1 :
      R)

Tactic:
dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]

Premises used: LinearEquiv.prodComm, Module.Dual.eval
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
x : Module.Dual R M × M
x_1 : M
⊢ HAdd.hAdd (α := R) (β := R) (0 : R) ((x.1 : (a : M) → R) x_1 : R) = (x.1 : (a : M) → R) x_1

Tactic:
simp
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
x : Module.Dual R M × M
refine_2 :
  ∀ (x_1 : Module.Dual R M),
    Eq.{u_1 + 1} (α := R)
      ((((h_d : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) x).2 :
            (a : Module.Dual R M) → R)
          x_1 :
        R)
      ((((prodMap id (Module.Dual.eval R M) :
                  (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
                x).2 :
            (a : Module.Dual R M) → R)
          x_1 :
        R)
⊢ Eq (α := 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)) x).2
    ((prodMap id (Module.Dual.eval R M) : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
        x).2

Tactic:
ext
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
x : Module.Dual R M × M
x_1 : Module.Dual R M
refine_2 :
  HAdd.hAdd (α := R) (β := R) ((x_1 : (a : M) → R) x.2 : R) ((x.1 : (a : M) → R) 0 : R) = (x_1 : (a : M) → R) x.2
⊢ Eq.{u_1 + 1} (α := R)
    ((((h_d : (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M)) x).2 :
          (a : Module.Dual R M) → R)
        x_1 :
      R)
    ((((prodMap id (Module.Dual.eval R M) :
                (a : Module.Dual R M × M) → Module.Dual R M × Module.Dual R (Module.Dual R M))
              x).2 :
          (a : Module.Dual R M) → R)
        x_1 :
      R)

Tactic:
dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]

Premises used: LinearEquiv.prodComm, Module.Dual.eval
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
x : Module.Dual R M × M
x_1 : Module.Dual R M
⊢ HAdd.hAdd (α := R) (β := R) ((x_1 : (a : M) → R) x.2 : R) ((x.1 : (a : M) → R) 0 : R) = (x_1 : (a : M) → R) x.2

Tactic:
simp
-- 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
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 : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
⊢ h_d = prodMap id (Module.Dual.eval R M)

Tactic:
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
-- 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
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 : 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)
rw :
  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))
⊢ 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))

Tactic:
rw [this, coe_prodMap]

Premises used: LinearMap.coe_prodMap
-- 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
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 : 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))

Tactic:
Prod.map_injective.trans ?_

Premises used: Prod.map_injective, Iff.trans
-- 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
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 : 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)
refine :
  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))
⊢ 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))

Tactic:
refine Prod.map_injective.trans ?_

Premises used: Prod.map_injective, Iff.trans