case intro.intro.intro.intro
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.158165
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
w✝¹ w✝ : α
left✝¹ : w✝¹ ∈ ↑m ⁻¹' s
left✝ : w✝ ∈ ↑m ⁻¹' t
⊢ (fun x x_1 => x / x_1) w✝¹ w✝ ∈ ↑m ⁻¹' (s / t)
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.158165
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
⊢ ↑m ⁻¹' s / ↑m ⁻¹' t ⊆ ↑m ⁻¹' (s / t)
rintro _ ⟨_, _, _, _, rfl⟩
no goals
case intro.intro.intro.intro
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.158165
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
w✝¹ w✝ : α
left✝¹ : w✝¹ ∈ ↑m ⁻¹' s
left✝ : w✝ ∈ ↑m ⁻¹' t
⊢ (fun x x_1 => x / x_1) w✝¹ w✝ ∈ ↑m ⁻¹' (s / t)
exact ⟨_, _, ‹_›, ‹_›, (map_div m _ _).symm⟩