internlm/Lean-Github huggingface dataset:
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
⊢ bilin (baseChange A F) x y = bilin (baseChange A F) y x
Tactic:
induction x using TensorProduct.induction_on generalizing y
Proof state after:
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✝)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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:
. rename_i t z
  induction y using TensorProduct.induction_on
  . simp
  . rename_i e r
    simp [hF, mul_comm t]
  . rename_i e r he hr 
    simp [*]
Proof state after:
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✝)
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
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:
. rename_i t z ht hz
  induction y using TensorProduct.induction_on
  . simp
  . rename_i e r
    simp [*]
  . rename_i e r _ _
    simp only [add_right, add_left, *]
    ac_rfl
Proof state after:
no goals
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
Tactic:
simp
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
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✝)
Tactic:
rename_i t z
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
t : A
z : M
y : A ⊗[R] M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) y = bilin (baseChange A F) y (t ⊗ₜ[R] z)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
t : A
z : M
y : A ⊗[R] M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) y = bilin (baseChange A F) y (t ⊗ₜ[R] z)
Tactic:
induction y using TensorProduct.induction_on
Proof state after:
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)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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:
. rename_i e r
  simp [hF, mul_comm t]
Proof state after:
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)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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:
. rename_i e r he hr 
  simp [*]
Proof state after:
no goals
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)
Tactic:
simp
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
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)
Tactic:
rename_i e r
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
e : A
r : M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (e ⊗ₜ[R] r) = bilin (baseChange A F) (e ⊗ₜ[R] r) (t ⊗ₜ[R] z)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
e : A
r : M
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (e ⊗ₜ[R] r) = bilin (baseChange A F) (e ⊗ₜ[R] r) (t ⊗ₜ[R] z)
Tactic:
simp [hF, mul_comm t]
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
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:
rename_i e r he hr
Proof state after:
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
e r : A ⊗[R] M
he : bilin (baseChange A F) (t ⊗ₜ[R] z) e = bilin (baseChange A F) e (t ⊗ₜ[R] z)
hr : bilin (baseChange A F) (t ⊗ₜ[R] z) r = bilin (baseChange A F) r (t ⊗ₜ[R] z)
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (e + r) = bilin (baseChange A F) (e + r) (t ⊗ₜ[R] z)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
e r : A ⊗[R] M
he : bilin (baseChange A F) (t ⊗ₜ[R] z) e = bilin (baseChange A F) e (t ⊗ₜ[R] z)
hr : bilin (baseChange A F) (t ⊗ₜ[R] z) r = bilin (baseChange A F) r (t ⊗ₜ[R] z)
⊢ bilin (baseChange A F) (t ⊗ₜ[R] z) (e + r) = bilin (baseChange A F) (e + r) (t ⊗ₜ[R] z)
Tactic:
simp [*]
Proof state after:
no goals
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
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:
rename_i t z ht hz
Proof state after:
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)