[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ lcm (s₁ + s₂) = fold GCDMonoid.lcm (GCDMonoid.lcm 1 1) (s₁ + s₂)
[PROOFSTEP]
simp [lcm]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ lcm 0 ∣ a ↔ ∀ (b : α), b ∈ 0 → b ∣ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (lcm s ∣ a ↔ ∀ (b : α), b ∈ s → b ∣ a) → (lcm (a_1 ::ₘ s) ∣ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ∣ a)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and, lcm_dvd_iff]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ↑normalize (lcm 0) = lcm 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : ↑normalize (lcm s) = lcm s
⊢ ↑normalize (lcm (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
s : Multiset α
⊢ lcm s = 0 ↔ 0 ∈ s
[PROOFSTEP]
induction' s using Multiset.induction_on with a s ihs
[GOAL]
case empty
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
⊢ lcm 0 = 0 ↔ 0 ∈ 0
[PROOFSTEP]
simp only [lcm_zero, one_ne_zero, not_mem_zero]
[GOAL]
case cons
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
a : α
s : Multiset α
ihs : lcm s = 0 ↔ 0 ∈ s
⊢ lcm (a ::ₘ s) = 0 ↔ 0 ∈ a ::ₘ s
[PROOFSTEP]
simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ lcm (dedup 0) = lcm 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
⊢ lcm (dedup (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ lcm (dedup (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : ¬a ∈ s
⊢ lcm (dedup (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ lcm s = GCDMonoid.lcm a (lcm s)
[PROOFSTEP]
unfold lcm
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)
[PROOFSTEP]
rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (erase s a)) = GCDMonoid.lcm (↑normalize a) (fold GCDMonoid.lcm 1 (erase s a))
[PROOFSTEP]
apply lcm_eq_of_associated_left (associated_normalize _)
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ lcm (ndunion s₁ s₂) = GCDMonoid.lcm (lcm s₁) (lcm s₂)
[PROOFSTEP]
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ lcm (s₁ ∪ s₂) = GCDMonoid.lcm (lcm s₁) (lcm s₂)
[PROOFSTEP]
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ lcm (ndinsert a s) = GCDMonoid.lcm a (lcm s)
[PROOFSTEP]
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ gcd (s₁ + s₂) = fold GCDMonoid.gcd (GCDMonoid.gcd 0 0) (s₁ + s₂)
[PROOFSTEP]
simp [gcd]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ a ∣ gcd 0 ↔ ∀ (b : α), b ∈ 0 → a ∣ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (a ∣ gcd s ↔ ∀ (b : α), b ∈ s → a ∣ b) → (a ∣ gcd (a_1 ::ₘ s) ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ∣ b)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and, dvd_gcd_iff]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ↑normalize (gcd 0) = gcd 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : ↑normalize (gcd s) = gcd s
⊢ ↑normalize (gcd (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ gcd s = 0 ↔ ∀ (x : α), x ∈ s → x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ gcd s = 0 → ∀ (x : α), x ∈ s → x = 0
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ x = 0
[PROOFSTEP]
apply eq_zero_of_zero_dvd
[GOAL]
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x
[PROOFSTEP]
rw [← h]
[GOAL]
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ gcd s ∣ x
[PROOFSTEP]
apply gcd_dvd hx
[GOAL]
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case mpr.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0
[PROOFSTEP]
simp
[GOAL]
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → x = 0) → gcd s = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → gcd (a ::ₘ s) = 0
[PROOFSTEP]
intro a s sgcd h
[GOAL]
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
sgcd : (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
h : ∀ (x : α), x ∈ a ::ₘ s → x = 0
⊢ gcd (a ::ₘ s) = 0
[PROOFSTEP]
simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
[PROOFSTEP]
refine' s.induction_on _ fun b s ih ↦ _
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) 0) = ↑normalize a * gcd 0
[PROOFSTEP]
simp_rw [map_zero, gcd_zero, mul_zero]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ gcd (map ((fun x x_1 => x * x_1) a) (b ::ₘ s)) = ↑normalize a * gcd (b ::ₘ s)
[PROOFSTEP]
simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (gcd (map (fun x => a * x) s)) = GCDMonoid.gcd (a * b) (a * gcd s)
[PROOFSTEP]
rw [ih]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (↑normalize a * gcd s) = GCDMonoid.gcd (a * b) (a * gcd s)
[PROOFSTEP]
apply ((normalize_associated a).mul_right _).gcd_eq_right
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ gcd (dedup 0) = gcd 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : ¬a ∈ s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ gcd s = GCDMonoid.gcd a (gcd s)
[PROOFSTEP]
unfold gcd
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)
[PROOFSTEP]
rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (erase s a)) = GCDMonoid.gcd (↑normalize a) (fold GCDMonoid.gcd 0 (erase s a))
[PROOFSTEP]
apply (associated_normalize _).gcd_eq_left
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd (ndunion s₁ s₂) = GCDMonoid.gcd (gcd s₁) (gcd s₂)
[PROOFSTEP]
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd (s₁ ∪ s₂) = GCDMonoid.gcd (gcd s₁) (gcd s₂)
[PROOFSTEP]
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ gcd (ndinsert a s) = GCDMonoid.gcd a (gcd s)
[PROOFSTEP]
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
⊢ gcd s * gcd t = gcd s
[PROOFSTEP]
conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
| gcd s * gcd t
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
| gcd s * gcd t
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
| gcd s * gcd t
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
⊢ ¬gcd s = 0
[PROOFSTEP]
contrapose! hs
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
hs : gcd s = 0
⊢ ∀ (x : α), x ∈ s → x = 0
[PROOFSTEP]
exact s.gcd_eq_zero_iff.1 hs
[GOAL]
α : 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
[PROOFSTEP]
classical
by_cases h : ∀ x ∈ s, x = (0 : α)
· use replicate (card s) 1
  simp only
  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]
  exact ⟨⟨rfl, h⟩, normalize_one⟩
· choose f hf using @gcd_dvd _ _ _ s
  push_neg at h 
  refine' ⟨s.pmap @f fun _ ↦ id, _, extract_gcd' s _ h _⟩ <;>
    · rw [map_pmap]
      conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
      congr with (x hx)
      simp only
      rw [id]
      rw [← hf hx]
[GOAL]
α : 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
[PROOFSTEP]
by_cases h : ∀ x ∈ s, x = (0 : α)
[GOAL]
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
[PROOFSTEP]
use replicate (card s) 1
[GOAL]
case h
α : 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
[PROOFSTEP]
simp only
[GOAL]
case h
α : 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
[PROOFSTEP]
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]
[GOAL]
case h
α : 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
[PROOFSTEP]
exact ⟨⟨rfl, h⟩, normalize_one⟩
[GOAL]
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
[PROOFSTEP]
choose f hf using @gcd_dvd _ _ _ s
[GOAL]
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
[PROOFSTEP]
push_neg at h 
[GOAL]
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
[PROOFSTEP]
refine' ⟨s.pmap @f fun _ ↦ id, _, extract_gcd' s _ h _⟩
[GOAL]
case neg.refine'_1
α : 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))
[PROOFSTEP]
rw [map_pmap]
[GOAL]
case neg.refine'_1
α : 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)
[PROOFSTEP]
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : 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
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : 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
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : 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
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
case neg.refine'_1
α : 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)
[PROOFSTEP]
congr with (x hx)
[GOAL]
case neg.refine'_1.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)
[PROOFSTEP]
simp only
[GOAL]
case neg.refine'_1.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
[PROOFSTEP]
rw [id]
[GOAL]
case neg.refine'_1.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
[PROOFSTEP]
rw [← hf hx]
[GOAL]
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))
[PROOFSTEP]
rw [map_pmap]
[GOAL]
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)
[PROOFSTEP]
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : 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
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : 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
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : 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
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
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)
[PROOFSTEP]
congr with (x hx)
[GOAL]
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)
[PROOFSTEP]
simp only
[GOAL]
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
[PROOFSTEP]
rw [id]
[GOAL]
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
[PROOFSTEP]
rw [← hf hx]
