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

State before:
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ ↑(associatedHom R) (baseChange A F) = BilinForm.baseChange A (↑(associatedHom R) F)
Tactic:
simp only [baseChange]
State after:
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ ↑(associatedHom R) (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R) F))) =
    BilinForm.baseChange A (↑(associatedHom R) F)

State before:
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ ↑(associatedHom R) (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R) F))) =
    BilinForm.baseChange A (↑(associatedHom R) F)
Tactic:
apply associated_left_inverse
State after:
case h
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R) F))

State before:
case h
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R) F))
Tactic:
apply BilinForm.baseChangeSymm
State after:
case h.hF
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (↑(associatedHom R) F)

State before:
case h.hF
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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
F : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (↑(associatedHom R) F)
Tactic:
exact associated_isSymm R F
State after:
no goals