Theorem: QuadraticForm.baseChange_eval (AntLorentz/BaseChange.lean)

State before:
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ↑(baseChange A F) (a ⊗ₜ[R] m) = a * a * ↑(algebraMap R A) (↑F m)
Tactic:
rw [baseChange, BilinForm.toQuadraticForm_apply, BilinForm.baseChange_eval, associated_apply,
    ← two_smul R m, QuadraticForm.map_smul]
State after:
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ a * a * ↑(algebraMap R A) (⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m)) = a * a * ↑(algebraMap R A) (↑F m)

State before:
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ a * a * ↑(algebraMap R A) (⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m)) = a * a * ↑(algebraMap R A) (↑F m)
Tactic:
congr
State after:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m) = ↑F m

State before:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m) = ↑F m
Tactic:
rw [mul_assoc, invOf_mul_eq_iff_eq_mul_left]
State after:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ 2 * (2 * ↑F m) - ↑F m - ↑F m = 2 * ↑F m

State before:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ 2 * (2 * ↑F m) - ↑F m - ↑F m = 2 * ↑F m
Tactic:
ring
State after:
no goals