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 : 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
x y : M
simp :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) x : A) +
      (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) y : A)) =
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) y : A) +
      (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) x : A))
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (x + y) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x +
        HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) y)
      ((((LinearMap.compl₁₂ (LinearMap.mul R A) f g + LinearMap.compl₁₂ (LinearMap.flip (LinearMap.mul R A)) g f :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          y :
        A)

Tactic:
simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply,
        LinearMap.compl₁₂_apply, LinearMap.mul_apply', LinearMap.flip_apply]

Premises used: Pi.mul_apply, LinearMap.mul_apply', LinearMap.add_apply, map_add, LinearMap.flip_apply, LinearMap.compl₁₂_apply, right_distrib, left_distrib
-- 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
x y : M
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) x : A) +
      (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) y : A)) =
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) y : A) +
      (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) x : A))

Tactic:
abel_nf
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
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
x : M
⊢ (linMulLin f g : (a : M) → A) x = HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
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 h : M →ₗ[R] A
⊢ linMulLin (f + g) h = linMulLin f h + linMulLin g h

Tactic:
ext fun _ => add_mul _ _ _

Premises used: add_mul, QuadraticMap.ext, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
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 h : M →ₗ[R] A
⊢ linMulLin f (g + h) = linMulLin f g + linMulLin f h

Tactic:
ext fun _ => mul_add _ _ _

Premises used: QuadraticMap.ext, mul_add, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
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
N' : Type u_8
inst_7 : AddCommMonoid N'
inst_8 : Module R N'
f g : M →ₗ[R] A
h : N' →ₗ[R] M
⊢ (linMulLin f g).comp h = linMulLin (f ∘ₗ h) (g ∘ₗ h)

Tactic:
rfl

Premises used: QuadraticMap.comp, QuadraticMap.linMulLin, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
A : Type u_7
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
n : Type u_9
i j : n
x : n → A
⊢ (proj i j : (a : n → A) → A) x = x i * x j

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
N' : Type u_8
inst_5 : AddCommMonoid N'
inst_6 : Module R N'
B : BilinMap R M N
a : R
x : M
⊢ (((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) (a • x) =
    HSMul.hSMul (β := N) (a * a) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x : N)

Tactic:
simp only [map_smul, LinearMap.smul_apply, smul_smul]

Premises used: LinearMap.smul_apply, smul_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
N' : Type u_8
inst_5 : AddCommMonoid N'
inst_6 : Module R N'
B : BilinMap R M N
x y : M
⊢ (((B : (a : M) → M →ₗ[R] N) (x + y) : M →ₗ[R] N) : (a : M) → N) (x + y) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x : N)
        ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) y : N))
      ((((B + flip B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)

Tactic:
simp [add_add_add_comm, add_comm]

Premises used: add_comm, add_add_add_comm
-- 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
B : BilinMap R M N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((B.toQuadraticMap : (a : M) → N) x : N)
    ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (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
N' : Type u_8
inst_5 : AddCommMonoid N'
inst_6 : Module R N'
B : BilinMap R M N
f : N' →ₗ[R] M
⊢ toQuadraticMap (compl₁₂ B f f) = B.toQuadraticMap.comp f

Tactic:
rfl

Premises used: QuadraticMap.comp, LinearMap.BilinMap.toQuadraticMap, 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
⊢ Eq (α := QuadraticMap R M N) (toQuadraticMap 0) 0

Tactic:
rfl

Premises used: LinearMap.BilinMap.toQuadraticMap, 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
B₁ B₂ : BilinMap R M N
⊢ (B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap

Tactic:
rfl

Premises used: LinearMap.BilinMap.toQuadraticMap, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass S R N
inst_8 : SMulCommClass R S N
a : S
B : BilinMap R M N
⊢ (a • B).toQuadraticMap = a • B.toQuadraticMap

Tactic:
rfl

Premises used: LinearMap.BilinMap.toQuadraticMap, 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
B : List (BilinMap R M N)
⊢ B.sum.toQuadraticMap = (List.map toQuadraticMap B).sum

Tactic:
map_list_sum (toQuadraticMapAddMonoidHom R M) B

Premises used: map_list_sum, LinearMap.BilinMap.toQuadraticMap, LinearMap.BilinMap.toQuadraticMapAddMonoidHom
-- 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
B : Multiset (BilinMap R M N)
⊢ B.sum.toQuadraticMap = (Multiset.map toQuadraticMap B).sum

Tactic:
map_multiset_sum (toQuadraticMapAddMonoidHom R M) B

Premises used: map_multiset_sum, LinearMap.BilinMap.toQuadraticMap, LinearMap.BilinMap.toQuadraticMapAddMonoidHom
-- 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_9
s : Finset ι
B : ι → BilinMap R M N
⊢ Eq (α := QuadraticMap R M N) (toQuadraticMap (∑ i ∈ s, B i)) (∑ i ∈ s, (B i).toQuadraticMap)

Tactic:
map_sum (toQuadraticMapAddMonoidHom R M) B s

Premises used: map_sum, LinearMap.BilinMap.toQuadraticMap, LinearMap.BilinMap.toQuadraticMapAddMonoidHom
-- 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
B : BilinMap R M N
⊢ B.toQuadraticMap = 0 ↔ IsAlt B

Tactic:
QuadraticMap.ext_iff

Premises used: QuadraticMap.ext_iff, LinearMap.IsAlt
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
B : BilinMap R M N
⊢ (-B).toQuadraticMap = -B.toQuadraticMap

Tactic:
rfl

Premises used: LinearMap.BilinMap.toQuadraticMap, 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
B₁ B₂ : BilinMap R M N
⊢ (B₁ - B₂).toQuadraticMap = B₁.toQuadraticMap - B₂.toQuadraticMap

Tactic:
rfl

Premises used: QuadraticMap.copy, LinearMap.BilinMap.toQuadraticMap, 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
B : BilinMap R M N
x y : M
⊢ polar (⇑B.toQuadraticMap : (a : M) → N) x y =
    HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)

Tactic:
simp only [polar, toQuadraticMap_apply, map_add, add_apply, add_assoc, add_comm (B y x) _,
    add_sub_cancel_left, sub_eq_add_neg _ (B y y), add_neg_cancel_left]

Premises used: add_neg_cancel_left, add_sub_cancel_left, LinearMap.add_apply, add_assoc, sub_eq_add_neg, map_add, QuadraticMap.polar, add_comm, LinearMap.BilinMap.toQuadraticMap_apply, DFunLike.coe
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
B : BilinMap R M N
⊢ B.toQuadraticMap.polarBilin = B + flip B

Tactic:
LinearMap.ext₂ polar_toQuadraticMap

Premises used: LinearMap.BilinMap.polar_toQuadraticMap, LinearMap.ext₂
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
⊢ HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N) = (HSMul.hSMul (α := ℕ) 2 Q : (a : M) → N) x

Tactic:
simp
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
apply : HSMul.hSMul (α := R) 2 Q₁ = HSMul.hSMul (α := R) 2 Q₂
⊢ Q₁ = Q₂

Tactic:
apply h.smul_left_cancel.mp

Premises used: IsUnit.smul_left_cancel, Iff.mp
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Eq.{u_3 + 1} (α := R) 2 (↑2 : R)

Tactic:
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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
rw : HSMul.hSMul (α := R) (↑2 : R) Q₁ = HSMul.hSMul (α := R) (↑2 : R) Q₂
⊢ HSMul.hSMul (α := R) 2 Q₁ = HSMul.hSMul (α := R) 2 Q₂

Tactic:
rw [show (2 : R) = (2 : ℕ) by 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
simp_rw : Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap
⊢ HSMul.hSMul (α := R) (↑2 : R) Q₁ = HSMul.hSMul (α := R) (↑2 : R) Q₂

Tactic:
simp_rw [Nat.cast_smul_eq_nsmul R, ← QuadraticMap.toQuadraticMap_polarBilin]

Premises used: QuadraticMap.toQuadraticMap_polarBilin, Nat.cast_smul_eq_nsmul
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap

Tactic:
congrArg toQuadraticMap h₁₂

Premises used: congrArg, LinearMap.BilinMap.toQuadraticMap
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap

Tactic:
exact congrArg toQuadraticMap h₁₂

Premises used: congrArg, LinearMap.BilinMap.toQuadraticMap
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
N' : Type u_8
inst_5 : AddCommGroup N'
inst_6 : Module R N'
Q : QuadraticMap R N' N
f : M →ₗ[R] N'
x y : M
⊢ Eq.{u_5 + 1} (α := N) (((((Q.comp f).polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
    ((((compl₁₂ Q.polarBilin f f : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)

Tactic:
simp [polar]

Premises used: QuadraticMap.polar
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
N' : Type u_8
inst_5 : AddCommGroup N'
inst_6 : CommSemiring S
inst_7 : Algebra S R
inst_8 : Module S N
inst_9 : Module S N'
inst_10 : IsScalarTower S R N
inst_11 : Module S M
inst_12 : IsScalarTower S R M
f : N →ₗ[S] N'
Q : QuadraticMap R M N
x y : M
⊢ Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x y : N')
    ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x y) : N')

Tactic:
simp [polar]

Premises used: QuadraticMap.polar
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
N' : Type u_8
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
h :
  ∀ (x x_1 : M),
    Eq.{u_8 + 1} (α := N')
      ((((polarBilin (f.compQuadraticMap' Q) : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
      ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
⊢ polarBilin (f.compQuadraticMap' Q) = compr₂ Q.polarBilin f

Tactic:
ext
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
N' : Type u_8
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x x_1 : M
h :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
h₁ :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((f : (a : N) → N') ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N) : N')
h₂ :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
h₃ h₄ :
  Eq.{u_8 + 1} (α := N') ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
    ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
⊢ Eq.{u_8 + 1} (α := N')
    ((((polarBilin (f.compQuadraticMap' Q) : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
    ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')

Tactic:
rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply,
    LinearMap.compQuadraticMap_polar]

Premises used: LinearMap.compr₂_apply, LinearMap.compQuadraticMap_polar, QuadraticMap.polarBilin_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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
h :
  ∀ (m : M),
    Eq (α := M)
      ((HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                  (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
                1 *
              2 :
            (a : M) → M)
          m :
        M)
      ((1 : (a : M) → M) m : M)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
        1 *
      2 =
    1

Tactic:
ext m
-- 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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 m) =
    m
⊢ Eq (α := M)
    ((HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
              1 *
            2 :
          (a : M) → M)
        m :
      M)
    ((1 : (a : M) → M) m : M)

Tactic:
dsimp [Submonoid.smul_def]

Premises used: Submonoid.smul_def
-- 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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) 2 m) =
    m
h₁ h₂ : m = m
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 m) =
    m

Tactic:
rw [← ofNat_smul_eq_nsmul R, invOf_smul_smul (2 : R) m]

Premises used: ofNat_smul_eq_nsmul, invOf_smul_smul, OfNat.ofNat
-- 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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
h :
  ∀ (m : M),
    Eq (α := M)
      ((2 *
              HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
                (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                  (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
                1 :
            (a : M) → M)
          m :
        M)
      ((1 : (a : M) → M) m : M)
⊢ 2 *
      HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
        1 =
    1

Tactic:
ext m
-- 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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
h :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
    m
⊢ Eq (α := M)
    ((2 *
            HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
              1 :
          (a : M) → M)
        m :
      M)
    ((1 : (a : M) → M) m : M)

Tactic:
dsimp [Submonoid.smul_def]

Premises used: Submonoid.smul_def
-- 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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) 2
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
    m
h₁ h₂ : m = m
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
    m

Tactic:
rw [← ofNat_smul_eq_nsmul R, smul_invOf_smul (2 : R) m]

Premises used: ofNat_smul_eq_nsmul, smul_invOf_smul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
x : M
⊢ (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : M) → M) x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) x

Tactic:
rfl

Premises used: rfl