Theorem: BilinForm.baseChangeSymm
Proof state before:
case C1.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
t : A
z : M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) 0 = bilin (baseChange A F) 0 (t ⊗ₜ[R] z)

case C1.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
t : A
z : M
x✝ : A
y✝ : M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (x✝ ⊗ₜ[R] y✝) = bilin (baseChange A F) (x✝ ⊗ₜ[R] y✝) (t ⊗ₜ[R] z)

case C1.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
t : A
z : M
x✝ y✝ : A ⊗[R] M
a✝¹ : bilin (baseChange A F) (t ⊗ₜ[R] z) x✝ = bilin (baseChange A F) x✝ (t ⊗ₜ[R] z)
a✝ : bilin (baseChange A F) (t ⊗ₜ[R] z) y✝ = bilin (baseChange A F) y✝ (t ⊗ₜ[R] z)
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (x✝ + y✝) = bilin (baseChange A F) (x✝ + y✝) (t ⊗ₜ[R] z)
Tactic:
. simp
Proof state after:
case C1.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
t : A
z : M
x✝ : A
y✝ : M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (x✝ ⊗ₜ[R] y✝) = bilin (baseChange A F) (x✝ ⊗ₜ[R] y✝) (t ⊗ₜ[R] z)

case C1.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
t : A
z : M
x✝ y✝ : A ⊗[R] M
a✝¹ : bilin (baseChange A F) (t ⊗ₜ[R] z) x✝ = bilin (baseChange A F) x✝ (t ⊗ₜ[R] z)
a✝ : bilin (baseChange A F) (t ⊗ₜ[R] z) y✝ = bilin (baseChange A F) y✝ (t ⊗ₜ[R] z)
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (x✝ + y✝) = bilin (baseChange A F) (x✝ + y✝) (t ⊗ₜ[R] z)