awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ 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))
    (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: 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
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₂ : HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₂ :
  HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) =
    HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₃ : a • HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₂ :
  HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) =
    HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₃ :
  a • HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₄ : a * HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₂ :
  HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) =
    HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₃ :
  a • HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₄ :
  a * HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₅ : a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₂ :
  HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) =
    HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₃ :
  a • HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₄ :
  a * HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₅ :
  a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₆ : a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HMul.hMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₂ :
  HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) =
    HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₃ :
  a • HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₄ :
  a * HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₅ :
  a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₆ : a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HMul.hMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
have rw₇ : a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R)
Tactic: rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw : ((p + q).1 : (a : M) → R) (p + q).2 =
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₁ : (p.1 + q.1 : (a : M) → R) (p + q).2 =
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₁ :
  (p.1 + q.1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₂ : (p.1 + q.1 : (a : M) → R) (p.2 + q.2) =
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₁ :
  (p.1 + q.1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₂ :
  (p.1 + q.1 : (a : M) → R) (p.2 + q.2) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₃ : HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) (p.2 + q.2) : R) ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₁ :
  (p.1 + q.1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₂ :
  (p.1 + q.1 : (a : M) → R) (p.2 + q.2) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₃ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) (p.2 + q.2) : R) ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₄ : HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R))
    ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₁ :
  (p.1 + q.1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₂ :
  (p.1 + q.1 : (a : M) → R) (p.2 + q.2) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₃ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) (p.2 + q.2) : R) ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₄ :
  HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R))
      ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₅ : HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) =
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₁ :
  (p.1 + q.1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₂ :
  (p.1 + q.1 : (a : M) → R) (p.2 + q.2) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₃ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) (p.2 + q.2) : R) ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₄ :
  HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R))
      ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₅ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₆ : HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R) +
    HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) =
  HAdd.hAdd (β := R)
    (HAdd.hAdd (α := R) ((p.1 : (a : M) → R) p.2 : R)
      (HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)))
    ((q.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]