awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
a : R
x : M
⊢ HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) (a • x) =
    (a * a) • HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) x

Tactic:
simp only [Pi.add_apply, smul_add, QuadraticMap.map_smul]

Premises used: QuadraticMap.map_smul, Pi.add_apply, smul_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
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
⊢ (⇑(Q + Q') : (a : M) → N) = HAdd.hAdd (α := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
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
x : M
⊢ (Q + Q' : (a : M) → N) x = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_8
Q : ι → QuadraticMap R M N
s : Finset ι
⊢ Eq (α := (a : M) → N) (⇑(∑ i ∈ s, Q i) : (a : M) → N) (∑ i ∈ s, (⇑(Q i) : (a : M) → N))

Tactic:
map_sum coeFnAddMonoidHom Q s

Premises used: map_sum, QuadraticMap.coeFnAddMonoidHom
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_8
Q : ι → QuadraticMap R M N
s : Finset ι
x : M
⊢ Eq.{u_5 + 1} (α := N) ((∑ i ∈ s, Q i : (a : M) → N) x : N) (∑ i ∈ s, (Q i : (a : M) → N) x : N)

Tactic:
map_sum (evalAddMonoidHom x : _ →+ N) Q s

Premises used: QuadraticMap.evalAddMonoidHom, map_sum
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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 b : S
Q : QuadraticMap R M N
x : M
⊢ Eq.{u_5 + 1} (α := N) (((a * b) • Q : (a : M) → N) x : N) ((a • b • Q : (a : M) → N) x : N)

Tactic:
simp only [smul_apply, mul_smul]

Premises used: QuadraticMap.smul_apply, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
Q : QuadraticMap R M N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((HSMul.hSMul (α := S) 1 Q : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)

Tactic:
simp only [QuadraticMap.smul_apply, one_smul]

Premises used: QuadraticMap.smul_apply, one_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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)
⊢ HSMul.hSMul (β := QuadraticMap R M N) a 0 = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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:
simp only [zero_apply, smul_apply, smul_zero]

Premises used: QuadraticMap.zero_apply, smul_zero, QuadraticMap.smul_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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)
⊢ a • (Q + Q') = a • Q + a • Q'

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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:
simp only [add_apply, smul_apply, smul_add]

Premises used: QuadraticMap.smul_apply, smul_add, QuadraticMap.add_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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)
⊢ (a + b) • Q = a • Q + b • Q

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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:
simp only [add_apply, smul_apply, add_smul]

Premises used: QuadraticMap.smul_apply, add_smul, QuadraticMap.add_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
H : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((HSMul.hSMul (α := S) 0 Q : (a : M) → N) x : N) ((0 : (a : M) → N) x : N)
⊢ HSMul.hSMul (α := S) 0 Q = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
x : M
⊢ Eq.{u_5 + 1} (α := N) ((HSMul.hSMul (α := S) 0 Q : (a : M) → N) x : N) ((0 : (a : M) → N) x : N)

Tactic:
simp only [zero_apply, smul_apply, zero_smul]

Premises used: QuadraticMap.zero_apply, QuadraticMap.smul_apply, zero_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
a : R
x : M
⊢ (-(⇑Q : (a : M) → N)) (a • x) = HSMul.hSMul (β := N) (a * a) ((-(⇑Q : (a : M) → N)) x : N)

Tactic:
simp only [Pi.neg_apply, Q.map_smul, smul_neg]

Premises used: QuadraticMap.map_smul, smul_neg, Pi.neg_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)
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)

Tactic:
simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]

Premises used: LinearMap.neg_apply, neg_add, Pi.neg_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
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
⊢ Eq (α := (a : M) → N) (⇑(-Q) : (a : M) → N) (-(⇑Q : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
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
x : M
⊢ Eq.{u_5 + 1} (α := N) ((-Q : (a : M) → N) x : N) (-(Q : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
⊢ (⇑(Q - Q') : (a : M) → N) = HSub.hSub (α := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
x : M
⊢ (Q - Q' : (a : M) → N) x = HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R N
Q : QuadraticMap R M N
a : S
x : M
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)

Tactic:
simp [map_smul_of_tower]

Premises used: QuadraticMap.map_smul_of_tower
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S 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))
      ((((LinearMap.restrictScalars₁₂ S S B : (a : M) → M →ₗ[S] N) x : M →ₗ[S] N) : (a : M) → N) y : N)

Tactic:
simp only [LinearMap.restrictScalars₁₂_apply_apply, h]

Premises used: LinearMap.restrictScalars₁₂_apply_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
a : R
x : M
⊢ (Q : (a : N) → P) ((f : (a : M) → N) (a • x) : N) =
    HSMul.hSMul (β := P) (a * a) ((Q : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
simp only [Q.map_smul, map_smul]

Premises used: QuadraticMap.map_smul, map_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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)
⊢ (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)

Tactic:
simp_rw [f.map_add]

Premises used: LinearMap.map_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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) (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:
h (f x) (f y)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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) (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:
exact h (f x) (f y)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
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
x : M
⊢ Eq.{u_6 + 1} (α := P) ((Q.comp f : (a : M) → P) x : P) ((Q : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
f : N →ₗ[R] P
Q : QuadraticMap R M N
b : R
x : M
⊢ (f : (a : N) → P) ((Q : (a : M) → N) (b • x) : N) =
    HSMul.hSMul (β := P) (b * b) ((f : (a : N) → P) ((Q : (a : M) → N) x : N) : P)

Tactic:
simp only [Q.map_smul, map_smul]

Premises used: QuadraticMap.map_smul, map_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
f : N →ₗ[R] P
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
⊢ (f : (a : N) → P) ((Q : (a : M) → N) (x + y) : N) =
    HAdd.hAdd (β := P)
      (HAdd.hAdd (α := P) (β := P) ((f : (a : N) → P) ((Q : (a : M) → N) x : N) : P)
        ((f : (a : N) → P) ((Q : (a : M) → N) y : N) : P))
      ((((LinearMap.compr₂ B f : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) : (a : M) → P) y : P)

Tactic:
simp only [h, map_add, LinearMap.compr₂_apply]

Premises used: LinearMap.compr₂_apply, map_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Eq (α := QuadraticMap R M N ≃ₗ[R] QuadraticMap R M N) (LinearEquiv.congrQuadraticMap (LinearEquiv.refl R N))
    (LinearEquiv.refl R (QuadraticMap R M N))

Tactic:
rfl

Premises used: LinearMap.compQuadraticMap, LinearEquiv.congrQuadraticMap, LinearEquiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
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
e : N ≃ₗ[R] P
⊢ Eq (α := QuadraticMap R M P ≃ₗ[R] QuadraticMap R M N) (LinearEquiv.symm e.congrQuadraticMap) e.symm.congrQuadraticMap

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearMap.compQuadraticMap, LinearEquiv.congrQuadraticMap, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
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
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₄ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
      HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₅ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) * HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₆ :
  a • HMul.hMul (α := A) ((f : (a : M) → A) x : A) (HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A)) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₇ :
  a • a • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₈ :
  (a • a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₉ rw₁₀ :
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ 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

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]

Premises used: Pi.mul_apply, RingHom.id_apply, smul_assoc, MulActionSemiHomClass.map_smulₛₗ, smul_mul_assoc, mul_smul_comm, smul_eq_mul