case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type ?u.12908
E : Type ?u.12911
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a✝ : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : ↑f a * ↑f b = ↑f c * ↑f c
⊢ ↑f a = ↑f b
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type ?u.12908
E : Type ?u.12911
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
⊢ MulSalemSpencer (↑f '' s)
rintro _ _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ habc
no goals
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type ?u.12908
E : Type ?u.12911
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a✝ : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : ↑f a * ↑f b = ↑f c * ↑f c
⊢ ↑f a = ↑f b
rw [h ha hb hc (hf (mul_mem_mul ha hb) (mul_mem_mul hc hc) <| by rwa [map_mul, map_mul])]
no goals
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type ?u.12908
E : Type ?u.12911
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a✝ : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : ↑f a * ↑f b = ↑f c * ↑f c
⊢ ↑f (a * b) = ↑f (c * c)
rwa [map_mul, map_mul]