F : Type ?u.94503
α : Type u_1
β : Type u_2
γ : Type ?u.94512
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t
F : Type ?u.94503
α : Type u_1
β : Type u_2
γ : Type ?u.94512
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
refine' ⟨_, zero_mem_smul_set⟩
case intro.intro
F : Type ?u.94503
α : Type u_1
β : Type u_2
γ : Type ?u.94512
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x => a • x) b = 0
⊢ 0 ∈ t
F : Type ?u.94503
α : Type u_1
β : Type u_2
γ : Type ?u.94512
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t
rintro ⟨b, hb, h⟩
no goals
case intro.intro
F : Type ?u.94503
α : Type u_1
β : Type u_2
γ : Type ?u.94512
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x => a • x) b = 0
⊢ 0 ∈ t
rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb