Theorem: LinearMap.baseChange_id (AntLorentz/BaseChange.lean)

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
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✝

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]
State after:
no goals