internlm/Lean-Github huggingface dataset:
Theorem: BilinForm.baseChangeSymm
Proof state before:
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)
Tactic:
. rename_i e r
  simp [*]
Proof state after:
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)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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)
Tactic:
. rename_i e r _ _
  simp only [add_right, add_left, *]
  ac_rfl
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
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)
Tactic:
simp
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
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)
Tactic:
rename_i e r
Proof state after:
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
e : A
r : M
⊢ bilin (baseChange A F) (t + z) (e ⊗ₜ[R] r) = bilin (baseChange A F) (e ⊗ₜ[R] r) (t + z)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
e : A
r : M
⊢ bilin (baseChange A F) (t + z) (e ⊗ₜ[R] r) = bilin (baseChange A F) (e ⊗ₜ[R] r) (t + z)
Tactic:
simp [*]
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
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)
Tactic:
rename_i e r _ _
Proof state after:
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
e r : A ⊗[R] M
a✝¹ : bilin (baseChange A F) (t + z) e = bilin (baseChange A F) e (t + z)
a✝ : bilin (baseChange A F) (t + z) r = bilin (baseChange A F) r (t + z)
⊢ bilin (baseChange A F) (t + z) (e + r) = bilin (baseChange A F) (e + r) (t + z)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
e r : A ⊗[R] M
a✝¹ : bilin (baseChange A F) (t + z) e = bilin (baseChange A F) e (t + z)
a✝ : bilin (baseChange A F) (t + z) r = bilin (baseChange A F) r (t + z)
⊢ bilin (baseChange A F) (t + z) (e + r) = bilin (baseChange A F) (e + r) (t + z)
Tactic:
simp only [add_right, add_left, *]
Proof state after:
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
e r : A ⊗[R] M
a✝¹ : bilin (baseChange A F) (t + z) e = bilin (baseChange A F) e (t + z)
a✝ : bilin (baseChange A F) (t + z) r = bilin (baseChange A F) r (t + z)
⊢ bilin (baseChange A F) e t + bilin (baseChange A F) e z + (bilin (baseChange A F) r t + bilin (baseChange A F) r z) =
    bilin (baseChange A F) e t + bilin (baseChange A F) r t + (bilin (baseChange A F) e z + bilin (baseChange A F) r z)
Theorem: BilinForm.baseChangeSymm
Proof state before:
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
e r : A ⊗[R] M
a✝¹ : bilin (baseChange A F) (t + z) e = bilin (baseChange A F) e (t + z)
a✝ : bilin (baseChange A F) (t + z) r = bilin (baseChange A F) r (t + z)
⊢ bilin (baseChange A F) e t + bilin (baseChange A F) e z + (bilin (baseChange A F) r t + bilin (baseChange A F) r z) =
    bilin (baseChange A F) e t + bilin (baseChange A F) r t + (bilin (baseChange A F) e z + bilin (baseChange A F) r z)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: QuadraticForm.baseChange_associatedHom
Proof state before:
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ ↑(associatedHom R) (baseChange A F) = BilinForm.baseChange A (↑(associatedHom R) F)
Tactic:
simp only [baseChange]
Proof state after:
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ ↑(associatedHom R) (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R) F))) =
    BilinForm.baseChange A (↑(associatedHom R) F)
Theorem: QuadraticForm.baseChange_associatedHom
Proof state before:
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ ↑(associatedHom R) (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R) F))) =
    BilinForm.baseChange A (↑(associatedHom R) F)
Tactic:
apply associated_left_inverse
Proof state after:
case h
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R) F))
Theorem: QuadraticForm.baseChange_associatedHom
Proof state before:
case h
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R) F))
Tactic:
apply BilinForm.baseChangeSymm
Proof state after:
case h.hF
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (↑(associatedHom R) F)
Theorem: QuadraticForm.baseChange_associatedHom
Proof state before:
case h.hF
R✝ : Type ?u.271123
M✝ : Type ?u.271126
A✝ : Type ?u.271350
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 : QuadraticForm R M
inst✝¹ : Invertible 2
inst✝ : Invertible 2
⊢ BilinForm.IsSymm (↑(associatedHom R) F)
Tactic:
exact associated_isSymm R F
Proof state after:
no goals
Theorem: QuadraticForm.baseChange_associated
Proof state before:
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ ↑associated (baseChange A F) = BilinForm.baseChange A (↑associated F)
Tactic:
simp only [baseChange]
Proof state after:
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ ↑associated (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R₁) F))) =
    BilinForm.baseChange A (↑associated F)
Theorem: QuadraticForm.baseChange_associated
Proof state before:
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ ↑associated (BilinForm.toQuadraticForm (BilinForm.baseChange A (↑(associatedHom R₁) F))) =
    BilinForm.baseChange A (↑associated F)
Tactic:
apply associated_left_inverse
Proof state after:
case h
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R₁) F))
Theorem: QuadraticForm.baseChange_associated
Proof state before:
case h
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (BilinForm.baseChange A (↑(associatedHom R₁) F))
Tactic:
apply BilinForm.baseChangeSymm
Proof state after:
case h.hF
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (↑(associatedHom R₁) F)
Theorem: QuadraticForm.baseChange_associated
Proof state before:
case h.hF
R✝ : Type ?u.346845
M✝ : Type ?u.346848
A✝¹ : Type ?u.347072
R₁ : Type
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
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₁ M
inst✝³ : Invertible 2
A : Type
inst✝² : CommRing A
inst✝¹ : Algebra R₁ A
inst✝ : Invertible 2
F✝ F : QuadraticForm R₁ M
⊢ BilinForm.IsSymm (↑(associatedHom R₁) F)
Tactic:
exact associated_isSymm R₁ F
Proof state after:
no goals