case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
by_cases h : ∀ x ∈ s, x = (0 : α)
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map ((fun x x_1 => x * x_1) (gcd s)) (replicate (↑card s) 1) ∧ gcd (replicate (↑card s) 1) = 1
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
use replicate (card s) 1
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map (fun x => gcd s * x) (replicate (↑card s) 1) ∧ gcd (replicate (↑card s) 1) = 1
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map ((fun x x_1 => x * x_1) (gcd s)) (replicate (↑card s) 1) ∧ gcd (replicate (↑card s) 1) = 1
simp only
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (↑card s = ↑card s ∧ ∀ (b : α), b ∈ s → b = 0) ∧ ↑normalize 1 = 1
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map (fun x => gcd s * x) (replicate (↑card s) 1) ∧ gcd (replicate (↑card s) 1) = 1
rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton,
← gcd_dedup, dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
no goals
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (↑card s = ↑card s ∧ ∀ (b : α), b ∈ s → b = 0) ∧ ↑normalize 1 = 1
exact ⟨⟨rfl, h⟩, normalize_one⟩
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ (x : α), x ∈ s → x = 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
choose f hf using @gcd_dvd _ _ _ s
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ (x : α), x ∈ s → x = 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
push_neg  at h
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = map ((fun x x_1 => x * x_1) (gcd s)) (pmap f s (_ : ∀ (x : α), x ∈ s → x ∈ s))
rw [map_pmap]
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ pmap (fun a x => id a) s (_ : ∀ (x : α), x ∈ s → x ∈ s) =
    pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = (fun x x_1 => x * x_1) (gcd s) (f hx)
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ pmap (fun a x => id a) s (_ : ∀ (x : α), x ∈ s → x ∈ s) =
    pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
congr with (x hx)
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = gcd s * f hx
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = (fun x x_1 => x * x_1) (gcd s) (f hx)
simp only
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ x = gcd s * f hx
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = gcd s * f hx
rw [id]
no goals
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ x = gcd s * f hx
rw [← hf hx]