-- Mathlib/Algebra/Equiv/TransferInstance.lean
/-- The module instance from `AddEquiv.module` is compatible with the `R`-module structures,
if the `AddEquiv` is induced by an `R`-module isomorphism. -/
lemma LinearEquiv.isScalarTower [Module R α] [Module R β] [IsScalarTower R A β]
    (e : α ≃ₗ[R] β) :
    letI := e.toAddEquiv.module A
    IsScalarTower R A α

Proof state:
case smul_assoc
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
      (x • y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z) =
    x •
      { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
        (y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z)

Tactic:
apply e.symm.map_smul

Result:
no goals

Proof state:
case smul_assoc
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ (x • y) • z = x • y • z

Tactic:
simp only [Equiv.smul_def, AddEquiv.toEquiv_eq_coe, smul_assoc]

Result:
case smul_assoc
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
      (x • y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z) =
    x •
      { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
        (y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z)

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
⊢ IsScalarTower R A α

Tactic:
constructor

Result:
case smul_assoc
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
⊢ ∀ (x : R) (y : A) (z : α), (x • y) • z = x • y • z

Proof state:
case smul_assoc
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
⊢ ∀ (x : R) (y : A) (z : α), (x • y) • z = x • y • z

Tactic:
intro x y z

Result:
case smul_assoc
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ (x • y) • z = x • y • z

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
⊢ IsScalarTower R A α

Tactic:
letI := e.toAddEquiv.module A

Result:
α : Type u
β : Type v
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
⊢ IsScalarTower R A α