. simp
case intro.val.C0
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) 0) = ↑(baseChange A Q) 0

case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)

case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)

case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)