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
ι : Type u_8
Q : QuadraticMap R M N
g : ι → M
l : ι → R
p : Sym2 ι
⊢ polarSym2 (⇑Q : (a : M) → N) (Sym2.map (l • g) p) =
    HSMul.hSMul (β := N) (Sym2.map l p).mul (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g p))
have mk : ∀ (fst snd : ι),
  polarSym2 (⇑Q : (a : M) → N) (Sym2.map (l • g) (Quot.mk (Sym2.Rel ι) (fst, snd))) =
    HSMul.hSMul (β := N) (Sym2.map l (Quot.mk (Sym2.Rel ι) (fst, snd))).mul
      (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g (Quot.mk (Sym2.Rel ι) (fst, snd))))
Tactic: obtain ⟨_, _⟩ := p
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have rw : polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) y =
  HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
rw :
  polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) y =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) a : R) (polar (⇑Q : (a : M) → N) x y) =
  HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
rw :
  polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) y =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₁ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) a : R) (polar (⇑Q : (a : M) → N) x y) =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have rw₂ : HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
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) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) y) =
  HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
rw :
  polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) y) =
    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₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) a : R) (polar (⇑Q : (a : M) → N) x y) =
  HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
rw :
  polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) y) =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₁ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) a : R) (polar (⇑Q : (a : M) → N) x y) =
    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₂ : HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 x_2 : M
⊢ polar toFun x (x_1 + x_2) = polar toFun x x_1 + polar toFun x x_2
have simp_rw : polar toFun (x_1 + x_2) x = polar toFun x_1 x + polar toFun x_2 x
Tactic: simp_rw [polar_comm _ x, polar_add_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x : R
x_1 x_2 : M
⊢ polar toFun x_1 (x • x_2) = x • polar toFun x_1 x_2
have rw : polar toFun (x • x_2) x_1 = x • polar toFun x_1 x_2
Tactic: rw [polar_comm, polar_smul_left, polar_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x : R
x_1 x_2 : M
rw : polar toFun (x • x_2) x_1 = x • polar toFun x_1 x_2
⊢ polar toFun x_1 (x • x_2) = x • polar toFun x_1 x_2
have rw₁ : x • polar toFun x_2 x_1 = x • polar toFun x_1 x_2
Tactic: rw [polar_comm, polar_smul_left, polar_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x : R
x_1 x_2 : M
rw : polar toFun (x • x_2) x_1 = x • polar toFun x_1 x_2
rw₁ : x • polar toFun x_2 x_1 = x • polar toFun x_1 x_2
⊢ polar toFun x_1 (x • x_2) = x • polar toFun x_1 x_2
have rw₂ : x • polar toFun x_1 x_2 = x • polar toFun x_1 x_2
Tactic: rw [polar_comm, polar_smul_left, polar_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 : M
⊢ toFun (x + x_1) =
    HAdd.hAdd (β := N) (toFun x + toFun x_1)
      ((((LinearMap.mk₂ R (polar toFun) polar_add_left polar_smul_left ⋯ ⋯ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) :
            (a : M) → N)
          x_1 :
        N)
have simp : toFun (x + x_1) = toFun x + toFun x_1 + polar toFun x x_1
Tactic: simp only [LinearMap.mk₂_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 : M
⊢ toFun (x + x_1) = toFun x + toFun x_1 + polar toFun x x_1
have rw : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - toFun x - toFun x_1)
Tactic: rw [polar, sub_sub, add_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 : M
rw : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - toFun x - toFun x_1)
⊢ toFun (x + x_1) = toFun x + toFun x_1 + polar toFun x x_1
have rw₁ : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - (toFun x + toFun x_1))
Tactic: rw [polar, sub_sub, add_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 : M
rw : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - toFun x - toFun x_1)
rw₁ : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - (toFun x + toFun x_1))
⊢ toFun (x + x_1) = toFun x + toFun x_1 + polar toFun x x_1
have rw₂ : toFun (x + x_1) = toFun (x + x_1)
Tactic: rw [polar, sub_sub, add_sub_cancel]
-- 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)
    ((((⋯.choose (p := fun (B : BilinMap R M N) ↦
                  ∀ (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have rw : Eq.{u_5 + 1} (α := N)
  ((((sorry.choose (p := fun (B : BilinMap R M N) ↦
                ∀ (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)) :
              (a : M) → M →ₗ[R] N)
            x :
          M →ₗ[R] N) :
        (a : M) → N)
      y :
    N)
  (polar (⇑Q : (a : M) → N) x y : N)
Tactic: rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, 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
rw :
  Eq.{u_5 + 1} (α := N)
    ((((⋯.choose (p := fun (B : BilinMap R M N) ↦
                  ∀ (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    (polar (⇑Q : (a : M) → N) x y : N)
⊢ Eq.{u_5 + 1} (α := N)
    ((((⋯.choose (p := fun (B : BilinMap R M N) ↦
                  ∀ (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have rw₁ : (((sorry.choose (p := fun (B : BilinMap R M N) ↦
              ∀ (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)) :
            (a : M) → M →ₗ[R] N)
          x :
        M →ₗ[R] N) :
      (a : M) → N)
    y =
  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: rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
⊢ (Q : (a : M) → N) (∑ i ∈ Finset.cons a s ha, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ Finset.cons a s ha, (Q : (a : M) → N) (f i))
      (∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
have cons : HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
    (∑ i ∈ s, (Q : (a : M) → N) (f i) +
      HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
        (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))) =
  HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
    (∑ i ∈ s, (Q : (a : M) → N) (f i) +
      HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
        (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0))
Tactic: simp_rw [Finset.sum_cons, QuadraticMap.map_add, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_filter, Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons,
      Sym2.mkEmbedding_apply, Sym2.mk_isDiag_iff, not_true, if_false, zero_add,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply]
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (∑ i ∈ s, (Q : (a : M) → N) (f i) +
        HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
          (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))) =
    HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (∑ i ∈ s, (Q : (a : M) → N) (f i) +
        HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
          (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0))
have cons : HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
    (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
  HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
    (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
Tactic: congr 2
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
⊢ HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
      (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
    HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
have cons : HAdd.hAdd (α := N) (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))
    (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0) =
  HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
    (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
Tactic: rw [add_comm]
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
⊢ HAdd.hAdd (α := N) (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0) =
    HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
have cons : ∀ (i : ι) (hi : i ∈ s),
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (f a) (f i))
    (if ¬a = i then polar (⇑Q : (a : M) → N) (f a) (f i) else 0)
Tactic: congr! with i hi
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
i : ι
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (f a) (f i))
    (if ¬a = i then polar (⇑Q : (a : M) → N) (f a) (f i) else 0)
have cons : Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (f a) (f i)) (polar (⇑Q : (a : M) → N) (f a) (f i))
Tactic: rw [if_pos (ne_of_mem_of_not_mem hi ha).symm]