awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have simp_rw : HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (a • x + y) : N) ((Q : (a : M) → N) (a • x) : N))
    ((Q : (a : M) → N) y : N) =
  a •
    HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N)
Tactic: simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (a • x + y) : N) ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have simp_rw₁ : HSub.hSub (β := N)
    (HSub.hSub (β := N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (a • x) : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N))
      ((Q : (a : M) → N) (a • x) : N))
    ((Q : (a : M) → N) y : N) =
  a •
    HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N)
Tactic: simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (a • x + y) : N) ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
simp_rw₁ :
  HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (a • x) : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have simp_rw₂ : HSub.hSub (β := N)
    (HAdd.hAdd (β := N)
        (HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N) -
      HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N))
    ((Q : (a : M) → N) y : N) =
  a •
    HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N)
Tactic: simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (a • x + y) : N) ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
simp_rw₁ :
  HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (a • x) : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
simp_rw₂ :
  HSub.hSub (β := N)
      (HAdd.hAdd (β := N)
          (HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N) -
        HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have simp_rw₃ : HSub.hSub (β := N)
    (HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N) +
        HSMul.hSMul (β := N) a ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) -
      HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N))
    ((Q : (a : M) → N) y : N) =
  a •
    HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N)
Tactic: simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (-x) y) (-polar (⇑Q : (a : M) → N) x y)
have rw : Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) y)
  (-polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← neg_one_smul R x, polar_smul_left, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) y)
    (-polar (⇑Q : (a : M) → N) x y)
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (-x) y) (-polar (⇑Q : (a : M) → N) x y)
have rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (-1) (polar (⇑Q : (a : M) → N) x y) = -polar (⇑Q : (a : M) → N) x y
Tactic: rw [← neg_one_smul R x, polar_smul_left, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) y)
    (-polar (⇑Q : (a : M) → N) x y)
rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (-1) (polar (⇑Q : (a : M) → N) x y) = -polar (⇑Q : (a : M) → N) x y
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (-x) y) (-polar (⇑Q : (a : M) → N) x y)
have rw₂ : Eq.{u_5 + 1} (α := N) (-polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← neg_one_smul R x, polar_smul_left, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x x' y : M
⊢ polar (⇑Q : (a : M) → N) (x - x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
have rw : polar (⇑Q : (a : M) → N) (x + -x') y = HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x x' y : M
rw :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
⊢ polar (⇑Q : (a : M) → N) (x - x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
have rw₁ : polar (⇑Q : (a : M) → N) (x + -x') y =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x x' y : M
rw :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
rw₁ :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
⊢ polar (⇑Q : (a : M) → N) (x - x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
have rw₂ : HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) (-x') y) =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x x' y : M
rw :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
rw₁ :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
rw₂ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) (-x') y) =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
⊢ polar (⇑Q : (a : M) → N) (x - x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
have rw₃ : HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y) =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
⊢ polar (⇑Q : (a : M) → N) x (y + y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw : polar (⇑Q : (a : M) → N) (y + y') x = HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
⊢ polar (⇑Q : (a : M) → N) x (y + y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw₁ : polar (⇑Q : (a : M) → N) (y + y') x = HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) x y')
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
rw₁ :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) x y')
⊢ polar (⇑Q : (a : M) → N) x (y + y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw₂ : polar (⇑Q : (a : M) → N) (y + y') x = HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x)
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
rw₁ :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) x y')
rw₂ :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x)
⊢ polar (⇑Q : (a : M) → N) x (y + y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw₃ : HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x) =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x)
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
⊢ polar (⇑Q : (a : M) → N) x (a • y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have rw : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_smul_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
rw : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
⊢ polar (⇑Q : (a : M) → N) x (a • y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have rw₁ : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x)
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_smul_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
rw : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₁ : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x)
⊢ polar (⇑Q : (a : M) → N) x (a • y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have rw₂ : HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x)
Tactic: rw [polar_comm Q x, polar_comm Q x, polar_smul_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (-y)) (-polar (⇑Q : (a : M) → N) x y)
have rw : Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) y))
  (-polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← neg_one_smul R y, polar_smul_right, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) y))
    (-polar (⇑Q : (a : M) → N) x y)
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (-y)) (-polar (⇑Q : (a : M) → N) x y)
have rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (-1) (polar (⇑Q : (a : M) → N) x y) = -polar (⇑Q : (a : M) → N) x y
Tactic: rw [← neg_one_smul R y, polar_smul_right, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) y))
    (-polar (⇑Q : (a : M) → N) x y)
rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (-1) (polar (⇑Q : (a : M) → N) x y) = -polar (⇑Q : (a : M) → N) x y
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (-y)) (-polar (⇑Q : (a : M) → N) x y)
have rw₂ : Eq.{u_5 + 1} (α := N) (-polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← neg_one_smul R y, polar_smul_right, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
⊢ polar (⇑Q : (a : M) → N) x (y - y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw : polar (⇑Q : (a : M) → N) x (y + -y') = HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
⊢ polar (⇑Q : (a : M) → N) x (y - y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw₁ : polar (⇑Q : (a : M) → N) x (y + -y') =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
rw₁ :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
⊢ polar (⇑Q : (a : M) → N) x (y - y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw₂ : HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x (-y')) =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
rw₁ :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
rw₂ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x (-y')) =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
⊢ polar (⇑Q : (a : M) → N) x (y - y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
have rw₃ : HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y') =
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
⊢ polar (⇑Q : (a : M) → N) x x = HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N)
have rw : HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N) =
  HSMul.hSMul (β := N) (HMul.hMul (α := ℕ) 2 2) ((Q : (a : M) → N) x : N)
Tactic: rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_smul ℕ, ← two_smul ℕ, ← mul_smul]