internlm/Lean-Github huggingface dataset:
Theorem: LinearMap.baseChange_id
Proof state before:
R✝ : Type ?u.384027
M✝ : Type ?u.384030
inst✝¹² : CommRing R✝
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : Module R✝ M✝
M₂ : Type ?u.384791
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R✝ M₂
A✝ : Type ?u.385494
inst✝⁷ : Semiring A✝
inst✝⁶ : Algebra R✝ A✝
inst✝⁵ : Invertible 2
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A id = id
Tactic:
ext
Proof state after:
case a.h.h
R✝ : Type ?u.384027
M✝ : Type ?u.384030
inst✝¹² : CommRing R✝
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : Module R✝ M✝
M₂ : Type ?u.384791
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R✝ M₂
A✝ : Type ?u.385494
inst✝⁷ : Semiring A✝
inst✝⁶ : Algebra R✝ A✝
inst✝⁵ : Invertible 2
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (baseChange A id)) 1) x✝ = ↑(↑(AlgebraTensorModule.curry id) 1) x✝
Theorem: LinearMap.baseChange_id
Proof state before:
case a.h.h
R✝ : Type ?u.384027
M✝ : Type ?u.384030
inst✝¹² : CommRing R✝
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : Module R✝ M✝
M₂ : Type ?u.384791
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R✝ M₂
A✝ : Type ?u.385494
inst✝⁷ : Semiring A✝
inst✝⁶ : Algebra R✝ A✝
inst✝⁵ : Invertible 2
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (baseChange A id)) 1) x✝ = ↑(↑(AlgebraTensorModule.curry id) 1) x✝
Tactic:
simp only [AlgebraTensorModule.curry_apply, curry_apply, coe_restrictScalars, baseChange_tmul, id_coe, id_eq]
Proof state after:
no goals
Theorem: LinearMap.baseChange_comp
Proof state before:
R✝ : Type ?u.401799
M✝ : Type ?u.401802
inst✝¹⁶ : CommRing R✝
inst✝¹⁵ : AddCommGroup M✝
inst✝¹⁴ : Module R✝ M✝
M₂ : Type ?u.402563
inst✝¹³ : AddCommGroup M₂
inst✝¹² : Module R✝ M₂
A✝ : Type ?u.403266
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : Algebra R✝ A✝
inst✝⁹ : Invertible 2
B : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid B
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R B
f : M →ₗ[R] N
g : N →ₗ[R] B
⊢ comp (baseChange A g) (baseChange A f) = baseChange A (comp g f)
Tactic:
ext
Proof state after:
case a.h.h
R✝ : Type ?u.401799
M✝ : Type ?u.401802
inst✝¹⁶ : CommRing R✝
inst✝¹⁵ : AddCommGroup M✝
inst✝¹⁴ : Module R✝ M✝
M₂ : Type ?u.402563
inst✝¹³ : AddCommGroup M₂
inst✝¹² : Module R✝ M₂
A✝ : Type ?u.403266
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : Algebra R✝ A✝
inst✝⁹ : Invertible 2
B : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid B
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R B
f : M →ₗ[R] N
g : N →ₗ[R] B
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (baseChange A g) (baseChange A f))) 1) x✝ =
    ↑(↑(AlgebraTensorModule.curry (baseChange A (comp g f))) 1) x✝
Theorem: LinearMap.baseChange_comp
Proof state before:
case a.h.h
R✝ : Type ?u.401799
M✝ : Type ?u.401802
inst✝¹⁶ : CommRing R✝
inst✝¹⁵ : AddCommGroup M✝
inst✝¹⁴ : Module R✝ M✝
M₂ : Type ?u.402563
inst✝¹³ : AddCommGroup M₂
inst✝¹² : Module R✝ M₂
A✝ : Type ?u.403266
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : Algebra R✝ A✝
inst✝⁹ : Invertible 2
B : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid B
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R B
f : M →ₗ[R] N
g : N →ₗ[R] B
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (baseChange A g) (baseChange A f))) 1) x✝ =
    ↑(↑(AlgebraTensorModule.curry (baseChange A (comp g f))) 1) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
h : QuadraticForm.Equivalent Q S
⊢ QuadraticForm.Equivalent (baseChange A Q) (baseChange A S)
Tactic:
cases' h with val
Proof state after:
case intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ QuadraticForm.Equivalent (baseChange A Q) (baseChange A S)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ QuadraticForm.Equivalent (baseChange A Q) (baseChange A S)
Tactic:
constructor
Proof state after:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ Isometry (baseChange A Q) (baseChange A S)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ Isometry (baseChange A Q) (baseChange A S)
Tactic:
use (LinearEquiv.baseChange val.toLinearEquiv)
Proof state after:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ ∀ (m : A ⊗[R] M),
    ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ ∀ (m : A ⊗[R] M),
    ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m
Tactic:
intro m
Proof state after:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
m : A ⊗[R] M
⊢ ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
m : A ⊗[R] M
⊢ ↑(baseChange A S) (AddHom.toFun (↑(LinearEquiv.baseChange val.toLinearEquiv)).toAddHom m) = ↑(baseChange A Q) m
Tactic:
simp
Proof state after:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
m : A ⊗[R] M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) m) = ↑(baseChange A Q) m
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
m : A ⊗[R] M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) m) = ↑(baseChange A Q) m
Tactic:
induction m using TensorProduct.induction_on
Proof state after:
case intro.val.C0
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) 0) = ↑(baseChange A Q) 0

case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)

case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.C0
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) 0) = ↑(baseChange A Q) 0

case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)

case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Tactic:
. simp
Proof state after:
case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)

case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)

case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Tactic:
. simp
Proof state after:
case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Tactic:
. simp [map_add, *]
  obtain ⟨B, hB⟩ := (baseChange A S).exists_companion
  rw [hB] at *
  simp [*]
  sorry
Proof state after:
no goals
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.C0
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) 0) = ↑(baseChange A Q) 0
Tactic:
simp
Proof state after:
no goals
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.C1
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ : A
y✝ : M
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ ⊗ₜ[R] y✝)) = ↑(baseChange A Q) (x✝ ⊗ₜ[R] y✝)
Tactic:
simp
Proof state after:
no goals
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) (x✝ + y✝)) = ↑(baseChange A Q) (x✝ + y✝)
Tactic:
simp [map_add, *]
Proof state after:
case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.Cp
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Tactic:
obtain ⟨B, hB⟩ := (baseChange A S).exists_companion
Proof state after:
case intro.val.Cp.intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.Cp.intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝ + ↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Tactic:
rw [hB] at *
Proof state after:
case intro.val.Cp.intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) +
        ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) +
      BilinForm.bilin B (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝)
        (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)