awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
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 : ι
inl :
  ∀ (h : i < j),
    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)
⊢ 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)
have inr : 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: obtain h | rfl | h := lt_trichotomy i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
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 : ι
inl :
  ∀ (h : i < j),
    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)
inr :
  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)
⊢ 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)
have inr₁ : ∀ (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: obtain h | rfl | h := lt_trichotomy i j
-- 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
⊢ 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 : 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: rw [separatingLeft_iff_ker_eq_bot, ker_eq_bot]
-- 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
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))
have 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))
Tactic: refine (Function.Injective.of_comp_iff e.symm.injective
    (dualProd R M)).symm.trans ?_
-- 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
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 × 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))
have 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))
Tactic: rw [← LinearEquiv.coe_toLinearMap, ← coe_comp]
-- 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
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)
have 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
Tactic: refine ext fun x => Prod.ext ?_ ?_
-- 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
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
⊢ h_d = prodMap id (Module.Dual.eval R M)
have 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
Tactic: refine ext fun x => Prod.ext ?_ ?_
-- 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
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
⊢ 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
have 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)
Tactic: ext
-- 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
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
⊢ 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)
have refine_1 : HAdd.hAdd (α := R) (β := R) (0 : R) ((x.1 : (a : M) → R) x_1 : R) = (x.1 : (a : M) → R) x_1
Tactic: dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
-- 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
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
⊢ 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
have 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)
Tactic: ext
-- 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
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
⊢ 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)
have 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
Tactic: dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
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 × 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))
have this : 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
-- 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
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))
      (⇑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))
have 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))
Tactic: rw [this, coe_prodMap]
-- 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
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))
have 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))
Tactic: refine Prod.map_injective.trans ?_
-- 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
⊢ 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 : 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))
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
-- 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))
⊢ 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₁ : 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: 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