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
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij)) (∑ i ∈ s, (Q : (a : M) → N) (f i))
⊢ (Q : (a : M) → N) (∑ i ∈ Finset.cons a s ha, f i) =
    HSub.hSub (α := N) (∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
      (∑ i ∈ Finset.cons a s ha, (Q : (a : M) → N) (f i))
have cons : HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
    (HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
        (∑ i ∈ s, (Q : (a : M) → N) (f i)) +
      ∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
  HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) (f a) : N) + ∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x) +
      ∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij) -
    HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (f a) : N) (∑ i ∈ s, (Q : (a : M) → N) (f i) : N)
Tactic: simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]
-- 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
s : Finset ι
f : ι → M
⊢ (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij)) (∑ i ∈ s, (Q : (a : M) → N) (f i))
have empty : (Q : (a : M) → N) (∑ i ∈ ∅, f i) =
  HSub.hSub (α := N) (∑ ij ∈ Finset.sym2 ∅, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
    (∑ i ∈ ∅, (Q : (a : M) → N) (f i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]
    abel_nf
Cleared hypotheses: s
-- 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
s : Finset ι
f : ι → M
empty :
  (Q : (a : M) → N) (∑ i ∈ ∅, f i) =
    HSub.hSub (α := N) (∑ ij ∈ Finset.sym2 ∅, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
      (∑ i ∈ ∅, (Q : (a : M) → N) (f i))
⊢ (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij)) (∑ i ∈ s, (Q : (a : M) → N) (f i))
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    (Q : (a : M) → N) (∑ i ∈ s, f i) =
      HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
        (∑ i ∈ s, (Q : (a : M) → N) (f i))),
  (Q : (a : M) → N) (∑ i ∈ Finset.cons a s ha, f i) =
    HSub.hSub (α := N) (∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
      (∑ i ∈ Finset.cons a s ha, (Q : (a : M) → N) (f i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]
    abel_nf
Cleared hypotheses: s
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : Monoid T
inst_7 : DistribMulAction S N
inst_8 : DistribMulAction T N
inst_9 : SMulCommClass S R N
inst_10 : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
⊢ HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) (b • x) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
have rw : HSMul.hSMul (β := N) a ((Q : (a : M) → N) (b • x) : N) = (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
Tactic: rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : Monoid T
inst_7 : DistribMulAction S N
inst_8 : DistribMulAction T N
inst_9 : SMulCommClass S R N
inst_10 : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
rw :
  HSMul.hSMul (β := N) a ((Q : (a : M) → N) (b • x) : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
⊢ HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) (b • x) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
have rw₁ : a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) =
  (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
Tactic: rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : Monoid T
inst_7 : DistribMulAction S N
inst_8 : DistribMulAction T N
inst_9 : SMulCommClass S R N
inst_10 : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
rw :
  HSMul.hSMul (β := N) a ((Q : (a : M) → N) (b • x) : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
rw₁ :
  a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
⊢ HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) (b • x) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
have rw₂ : a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) = (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N)
Tactic: rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : Monoid T
inst_7 : DistribMulAction S N
inst_8 : DistribMulAction T N
inst_9 : SMulCommClass S R N
inst_10 : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
rw :
  HSMul.hSMul (β := N) a ((Q : (a : M) → N) (b • x) : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
rw₁ :
  a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
rw₂ :
  a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) =
    (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N)
⊢ HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) (b • x) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
have rw₃ : (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N) = (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N)
Tactic: rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
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)
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)
x y : M
⊢ HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) (x + y) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) x +
        HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) y)
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have simp_rw : HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q' : (a : M) → N) (x + y) : N) =
  HAdd.hAdd (β := N)
    (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
    ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
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)
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)
x y : M
simp_rw :
  HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q' : (a : M) → N) (x + y) : N) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
        HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) (x + y) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) x +
        HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) y)
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have simp_rw₁ : HAdd.hAdd (β := 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 + y) : N) =
  HAdd.hAdd (β := N)
    (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
    ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
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)
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)
x y : M
simp_rw :
  HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q' : (a : M) → N) (x + y) : N) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
        HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw₁ :
  HAdd.hAdd (β := 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 + y) : N) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
        HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) (x + y) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) x +
        HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) y)
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have simp_rw₂ : 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) +
    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) =
  HAdd.hAdd (β := N)
    (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
    ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass S R N
a : S
⊢ HSMul.hSMul (β := QuadraticMap R M N) a 0 = 0
have H : ∀ (x : M),
  Eq.{u_5 + 1} (α := N) ((HSMul.hSMul (β := QuadraticMap R M N) a 0 : (a : M) → N) x : N) ((0 : (a : M) → N) x : N)
Tactic: ext
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass S R N
a : S
Q Q' : QuadraticMap R M N
⊢ a • (Q + Q') = a • Q + a • Q'
have H : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((a • (Q + Q') : (a : M) → N) x : N) ((a • Q + a • Q' : (a : M) → N) x : N)
Tactic: ext
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Module S N
inst_7 : SMulCommClass S R N
a b : S
Q : QuadraticMap R M N
⊢ (a + b) • Q = a • Q + b • Q
have H : ∀ (x : M), Eq.{u_5 + 1} (α := N) (((a + b) • Q : (a : M) → N) x : N) ((a • Q + b • Q : (a : M) → N) x : N)
Tactic: ext
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Module S N
inst_7 : SMulCommClass S R N
Q : QuadraticMap R M N
⊢ HSMul.hSMul (α := S) 0 Q = 0
have H : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((HSMul.hSMul (α := S) 0 Q : (a : M) → N) x : N) ((0 : (a : M) → N) x : N)
Tactic: ext
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
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)
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)
have simp_rw : -(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)
Tactic: simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
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)
x y : M
simp_rw :
  -(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)
⊢ (-(⇑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)
have simp_rw₁ : -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) =
  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)
Tactic: simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
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)
x y : M
simp_rw :
  -(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₁ :
  -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) =
    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 + 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)
have simp_rw₂ : -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) =
  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)
Tactic: simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h :
  ∀ (x y : N),
    (Q : (a : N) → P) (x + y) =
      HAdd.hAdd (β := P) (HAdd.hAdd (α := P) (β := P) ((Q : (a : N) → P) x : P) ((Q : (a : N) → P) y : P))
        ((((B : (a : N) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x y : M
⊢ (Q : (a : N) → P) ((f : (a : M) → N) (x + y) : N) =
    HAdd.hAdd (β := P)
      (HAdd.hAdd (α := P) (β := P) ((Q : (a : N) → P) ((f : (a : M) → N) x : N) : P)
        ((Q : (a : N) → P) ((f : (a : M) → N) y : N) : P))
      ((((LinearMap.compl₁₂ B f f : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) : (a : M) → P) y : P)
have simp_rw : (Q : (a : N) → P) (HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)) =
  HAdd.hAdd (β := P)
    (HAdd.hAdd (α := P) (β := P) ((Q : (a : N) → P) ((f : (a : M) → N) x : N) : P)
      ((Q : (a : N) → P) ((f : (a : M) → N) y : N) : P))
    ((((LinearMap.compl₁₂ B f f : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) : (a : M) → P) y : P)
Tactic: simp_rw [f.map_add]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
  (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]