Theorem: BilinForm.baseChangeSymm
Proof state before:
case C0
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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 : BilinForm R M
hF : ∀ (x y : M), bilin F x y = bilin F y x
y : A ⊗[R] M
⊢ bilin (baseChange A F) 0 y = bilin (baseChange A F) y 0

case C1
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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 : BilinForm R M
hF : ∀ (x y : M), bilin F x y = bilin F y x
x✝ : A
y✝ : M
y : A ⊗[R] M
⊢ bilin (baseChange A F) (x✝ ⊗ₜ[R] y✝) y = bilin (baseChange A F) y (x✝ ⊗ₜ[R] y✝)

case Cp
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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 : BilinForm R M
hF : ∀ (x y : M), bilin F x y = bilin F y x
x✝ y✝ : A ⊗[R] M
a✝¹ : ∀ (y : A ⊗[R] M), bilin (baseChange A F) x✝ y = bilin (baseChange A F) y x✝
a✝ : ∀ (y : A ⊗[R] M), bilin (baseChange A F) y✝ y = bilin (baseChange A F) y y✝
y : A ⊗[R] M
⊢ bilin (baseChange A F) (x✝ + y✝) y = bilin (baseChange A F) y (x✝ + y✝)
Tactic:
. simp
Proof state after:
case C1
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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 : BilinForm R M
hF : ∀ (x y : M), bilin F x y = bilin F y x
x✝ : A
y✝ : M
y : A ⊗[R] M
⊢ bilin (baseChange A F) (x✝ ⊗ₜ[R] y✝) y = bilin (baseChange A F) y (x✝ ⊗ₜ[R] y✝)

case Cp
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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 : BilinForm R M
hF : ∀ (x y : M), bilin F x y = bilin F y x
x✝ y✝ : A ⊗[R] M
a✝¹ : ∀ (y : A ⊗[R] M), bilin (baseChange A F) x✝ y = bilin (baseChange A F) y x✝
a✝ : ∀ (y : A ⊗[R] M), bilin (baseChange A F) y✝ y = bilin (baseChange A F) y y✝
y : A ⊗[R] M
⊢ bilin (baseChange A F) (x✝ + y✝) y = bilin (baseChange A F) y (x✝ + y✝)