case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
by_cases h : a = 0 ∨ b = 0
no goals
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
rcases h with (rfl | rfl) <;>
  simp (config := { contextual := true }) only [iff_def, lcm_zero_left, lcm_zero_right,
    zero_dvd_iff, dvd_zero, eq_self_iff_true, and_true_iff, imp_true_iff]
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
obtain ⟨h1, h2⟩ := not_or.1 h
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
no goals
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
  (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
  mul_dvd_mul_iff_right h2, and_comm]