case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x

case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x

case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x

case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
by_cases hR : (n : R) = 0 <;> by_cases hS : (n : S) = 0
no goals
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
simp [hR, hS, map_zero f]
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), ↑f y = 0
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), ↑f y = 0
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), ↑f y = 0
clear x
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ ↑f x = 0
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), ↑f y = 0
intro x
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • ↑f (↑n • x) = 0
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ ↑f x = 0
rw [← inv_smul_smul₀ hS (f x), ← map_nat_cast_smul f R S]
no goals
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • ↑f (↑n • x) = 0
simp [hR, map_zero f]
no goals
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
this : ∀ (y : M), ↑f y = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
rw [this, this, smul_zero]
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), ↑f y = 0
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
suffices ∀ y, f y = 0 by simp [this]
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), ↑f y = 0
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), ↑f y = 0
clear x
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ ↑f x = 0
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), ↑f y = 0
intro x
no goals
case pos
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ ↑f x = 0
rw [← smul_inv_smul₀ hR x, map_nat_cast_smul f R S, hS, zero_smul]
no goals
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
this : ∀ (y : M), ↑f y = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
simp [this]
no goals
case neg
α : Type ?u.178772
R✝ : Type ?u.178775
k : Type ?u.178778
S✝ : Type ?u.178781
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.178790
ι : Type ?u.178793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
rw [← inv_smul_smul₀ hS (f _), ← map_nat_cast_smul f R S, smul_inv_smul₀ hR]