case intro.inl
α : Type ?u.198898
R✝ : Type ?u.198901
k : Type ?u.198904
S✝ : Type ?u.198907
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.198916
ι : Type ?u.198919
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ ↑f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • ↑f x

case intro.inr
α : Type ?u.198898
R✝ : Type ?u.198901
k : Type ?u.198904
S✝ : Type ?u.198907
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.198916
ι : Type ?u.198919
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ ↑f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • ↑f x
α : Type ?u.198898
R✝ : Type ?u.198901
k : Type ?u.198904
S✝ : Type ?u.198907
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.198916
ι : Type ?u.198919
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
z : ℤ
x : M
⊢ ↑f ((↑z)⁻¹ • x) = (↑z)⁻¹ • ↑f x
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
no goals
case intro.inl
α : Type ?u.198898
R✝ : Type ?u.198901
k : Type ?u.198904
S✝ : Type ?u.198907
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.198916
ι : Type ?u.198919
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ ↑f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • ↑f x
rw [Int.cast_Nat_cast, Int.cast_Nat_cast, map_inv_nat_cast_smul _ R S]
no goals
case intro.inr
α : Type ?u.198898
R✝ : Type ?u.198901
k : Type ?u.198904
S✝ : Type ?u.198907
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.198916
ι : Type ?u.198919
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ ↑f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • ↑f x
simp_rw [Int.cast_neg, Int.cast_Nat_cast, inv_neg, neg_smul, map_neg,
  map_inv_nat_cast_smul _ R S]