-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem zero_mem_smul_iff :
    (0 : β) ∈ s • t ↔ (0 : α) ∈ s ∧ t.Nonempty ∨ (0 : β) ∈ t ∧ s.Nonempty

Proof state:
case mpr
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty → 0 ∈ s • t

Tactic:
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)

Result:
case mpr.inl.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
hs : 0 ∈ s
b : β
hb : b ∈ t
⊢ 0 ∈ s • t

case mpr.inr.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
ht : 0 ∈ t
a : α
ha : a ∈ s
⊢ 0 ∈ s • t

Proof state:
case mpr.inl.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
hs : 0 ∈ s
b : β
hb : b ∈ t
⊢ 0 ∈ s • t

Tactic:
exact ⟨0, hs, b, hb, zero_smul _ _⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
constructor

Result:
case mp
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
⊢ 0 ∈ s • t → 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

case mpr
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty → 0 ∈ s • t

Proof state:
case mp.intro.intro.intro.intro.inr
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ∈ s
hb : 0 ∈ t
h : (fun x1 x2 => x1 • x2) a 0 = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
exact Or.inr ⟨hb, a, ha⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : (fun x1 x2 => x1 • x2) a b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
obtain rfl | rfl := eq_zero_or_eq_zero_of_smul_eq_zero h

Result:
case mp.intro.intro.intro.intro.inl
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
b : β
hb : b ∈ t
ha : 0 ∈ s
h : (fun x1 x2 => x1 • x2) 0 b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

case mp.intro.intro.intro.intro.inr
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ∈ s
hb : 0 ∈ t
h : (fun x1 x2 => x1 • x2) a 0 = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Proof state:
case mpr.inr.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
ht : 0 ∈ t
a : α
ha : a ∈ s
⊢ 0 ∈ s • t

Tactic:
exact ⟨a, ha, 0, ht, smul_zero _⟩

Result:
no goals

Proof state:
case mp
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
⊢ 0 ∈ s • t → 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
rintro ⟨a, ha, b, hb, h⟩

Result:
case mp.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : (fun x1 x2 => x1 • x2) a b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Proof state:
case mp.intro.intro.intro.intro.inl
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
b : β
hb : b ∈ t
ha : 0 ∈ s
h : (fun x1 x2 => x1 • x2) 0 b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
exact Or.inl ⟨ha, b, hb⟩

Result:
no goals