-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem extract_gcd (s : Multiset α) (hs : s ≠ 0) :
    ∃ t : Multiset α, s = t.map (s.gcd * ·) ∧ t.gcd = 1

Proof state:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
⊢ s = pmap (fun a h => s.gcd * f h) s ⋯

Tactic:
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]

Result:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
⊢ pmap (fun a x => id a) s ⋯ = pmap (fun a h => s.gcd * f h) s ⋯

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ x ∈ s, x = 0
⊢ (s.card = s.card ∧ ∀ b ∈ s, b = 0) ∧ normalize 1 = 1

Tactic:
exact ⟨⟨rfl, h⟩, normalize_one⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ x ∈ s, x = 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ ∃ t, s = map (fun x => s.gcd * x) t ∧ t.gcd = 1

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
⊢ ∃ t, s = map (fun x => s.gcd * x) t ∧ t.gcd = 1

Proof state:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
⊢ pmap (fun a x => id a) s ⋯ = pmap (fun a h => s.gcd * f h) s ⋯

Tactic:
congr with (x hx)

Result:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
⊢ id x = s.gcd * f hx

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

Tactic:
choose f hf using @gcd_dvd _ _ _ s

Result:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ x ∈ s, x = 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ ∃ t, s = map (fun x => s.gcd * x) t ∧ t.gcd = 1

Proof state:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
⊢ id x = s.gcd * f hx

Tactic:
rw [id, ← hf hx]

Result:
no goals

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

Tactic:
use replicate (card s) 1

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ x ∈ s, x = 0
⊢ s = map (fun x => s.gcd * x) (replicate s.card 1) ∧ (replicate s.card 1).gcd = 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ t, s = map (fun x => s.gcd * x) t ∧ t.gcd = 1

Tactic:
by_cases h : ∀ x ∈ s, x = (0 : α)

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

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

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ x ∈ s, x = 0
⊢ s = map (fun x => s.gcd * x) (replicate s.card 1) ∧ (replicate s.card 1).gcd = 1

Tactic:
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]

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ x ∈ s, x = 0
⊢ (s.card = s.card ∧ ∀ b ∈ s, b = 0) ∧ normalize 1 = 1

Proof state:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
⊢ s = map (fun x => s.gcd * x) (pmap f s ⋯)

Tactic:
rw [map_pmap]

Result:
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 = s.gcd * f h
h : ∃ x ∈ s, x ≠ 0
⊢ s = pmap (fun a h => s.gcd * f h) s ⋯