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

State before:
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ ↑associated (baseChange A F) = BilinForm.baseChange A (↑associated F)
Tactic:
simp only [baseChange]
State after:
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ ↑associated (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R₁) F))) =
    BilinForm.baseChange A (↑associated F)

State before:
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ ↑associated (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R₁) F))) =
    BilinForm.baseChange A (↑associated F)
Tactic:
apply associated_left_inverse
State after:
case h
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R₁) F))

State before:
case h
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R₁) F))
Tactic:
apply BilinForm.baseChangeSymm
State after:
case h.hF
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (↑(associatedHom R₁) F)

State before:
case h.hF
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (↑(associatedHom R₁) F)
Tactic:
exact associated_isSymm R₁ F
State after:
no goals