simp [*]
case intro.val.Cp.intro
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✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) +
        ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) +
      BilinForm.bilin B (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝)
        (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
case intro.val.Cp.intro
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✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A Q) x✝ + ↑(baseChange A Q) y✝ +
      BilinForm.bilin B (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝)
        (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)