Theorem: QuadraticForm.baseChange.Equivalent (AntLorentz/BaseChange.lean)

State before:
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₂
h : QuadraticForm.Equivalent Q S
⊢ QuadraticForm.Equivalent (baseChange A Q) (baseChange A S)
Tactic:
cases' h with val
State after:
case 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
⊢ QuadraticForm.Equivalent (baseChange A Q) (baseChange A S)

State before:
case 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
⊢ QuadraticForm.Equivalent (baseChange A Q) (baseChange A S)
Tactic:
constructor
State after:
case intro.val
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
⊢ Isometry (baseChange A Q) (baseChange A S)

State before:
case intro.val
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
⊢ Isometry (baseChange A Q) (baseChange A S)
Tactic:
use (LinearEquiv.baseChange val.toLinearEquiv)
State after:
case intro.val
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
⊢ ∀ (m : A ⊗[R] M),
    ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m

State before:
case intro.val
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
⊢ ∀ (m : A ⊗[R] M),
    ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m
Tactic:
intro m
State after:
case intro.val
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
m : A ⊗[R] M
⊢ ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m

State before:
case intro.val
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
m : A ⊗[R] M
⊢ ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m
Tactic:
simp
State after:
case intro.val
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
m : A ⊗[R] M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) m) = ↑(baseChange A Q) m

State before:
case intro.val
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
m : A ⊗[R] M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) m) = ↑(baseChange A Q) m
Tactic:
induction m using TensorProduct.induction_on
State after:
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✝)

State before:
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✝)
Tactic:
. simp
State after:
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✝)

State before:
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✝)
Tactic:
. simp
State after:
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✝)

State before:
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✝)
Tactic:
. simp [map_add, *]
  obtain ⟨B, hB⟩ := (baseChange A S).exists_companion
  rw [hB] at *
  simp [*]
  sorry
State after:
no goals

State before:
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
Tactic:
simp
State after:
no goals

State before:
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✝)
Tactic:
simp
State after:
no goals

State before:
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✝)
Tactic:
simp [map_add, *]
State after:
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✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)

State before:
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✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Tactic:
obtain ⟨B, hB⟩ := (baseChange A S).exists_companion
State after:
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✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)

State before:
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✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Tactic:
rw [hB] at *
State after:
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✝)

State before:
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✝)
Tactic:
simp [*]
State after:
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✝)

State before:
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✝)
Tactic:
sorry
State after:
no goals