Theorem: BilinForm.baseChangeSymm
Proof state before:
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
t z : A ⊗[R] M
ht : ∀ (y : A ⊗[R] M), bilin (baseChange A F) t y = bilin (baseChange A F) y t
hz : ∀ (y : A ⊗[R] M), bilin (baseChange A F) z y = bilin (baseChange A F) y z
y : A ⊗[R] M
⊢ bilin (baseChange A F) (t + z) y = bilin (baseChange A F) y (t + z)
Tactic:
induction y using TensorProduct.induction_on
Proof state after:
case Cp.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 z : A ⊗[R] M
ht : ∀ (y : A ⊗[R] M), bilin (baseChange A F) t y = bilin (baseChange A F) y t
hz : ∀ (y : A ⊗[R] M), bilin (baseChange A F) z y = bilin (baseChange A F) y z
⊢ bilin (baseChange A F) (t + z) 0 = bilin (baseChange A F) 0 (t + z)

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

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