case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : gcd k m = 0
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
by_cases h0 : gcd k m = 0
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : k = 0 ∧ m = 0
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : gcd k m = 0
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
rw [gcd_eq_zero_iff] at h0
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
n : α
H : 0 ∣ 0 * n
⊢ ∃ d₁ d₂, d₁ ∣ 0 ∧ d₂ ∣ n ∧ 0 = d₁ * d₂
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : k = 0 ∧ m = 0
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
rcases h0 with ⟨rfl, rfl⟩
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
n : α
H : 0 ∣ 0 * n
⊢ 0 = 0 * n
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
n : α
H : 0 ∣ 0 * n
⊢ ∃ d₁ d₂, d₁ ∣ 0 ∧ d₂ ∣ n ∧ 0 = d₁ * d₂
refine' ⟨0, n, dvd_refl 0, dvd_refl n, _⟩
no goals
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
n : α
H : 0 ∣ 0 * n
⊢ 0 = 0 * n
simp
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
obtain ⟨a, ha⟩ := gcd_dvd_left k m
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ a ∣ n
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
refine' ⟨gcd k m, a, gcd_dvd_right _ _, _, ha⟩
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
h : gcd k m * a ∣ gcd k m * n
⊢ a ∣ n

case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ gcd k m * a ∣ gcd k m * n
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ a ∣ n
suffices h : gcd k m * a ∣ gcd k m * n
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ k ∣ gcd k m * n
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ gcd k m * a ∣ gcd k m * n
rw [← ha]
no goals
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ k ∣ gcd k m * n
exact dvd_gcd_mul_of_dvd_mul H
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
b : α
hb : gcd k m * n = gcd k m * a * b
⊢ a ∣ n
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
h : gcd k m * a ∣ gcd k m * n
⊢ a ∣ n
cases' h with b hb
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
b : α
hb : gcd k m * n = gcd k m * a * b
⊢ n = a * b
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
b : α
hb : gcd k m * n = gcd k m * a * b
⊢ a ∣ n
use b
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
b : α
hb : gcd k m * n = gcd k m * (a * b)
⊢ n = a * b
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
b : α
hb : gcd k m * n = gcd k m * a * b
⊢ n = a * b
rw [mul_assoc] at hb
no goals
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
b : α
hb : gcd k m * n = gcd k m * (a * b)
⊢ n = a * b
apply mul_left_cancel₀ h0 hb