awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map (fun (x : α) ↦ a * x) s) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd
have refine_1 : gcd (map (fun (x : α) ↦ a * x) 0) = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
Tactic: refine s.induction_on ?_ fun b s ih ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s : Multiset α
refine_1 : gcd (map (fun (x : α) ↦ a * x) 0) = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
⊢ gcd (map (fun (x : α) ↦ a * x) s) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd
have refine_2 : ∀ (b : α) (s : Multiset α)
  (ih : gcd (map (fun (x : α) ↦ a * x) s) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd),
  gcd (map (fun (x : α) ↦ a * x) (b ::ₘ s)) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (b ::ₘ s).gcd
Tactic: refine s.induction_on ?_ fun b s ih ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map (fun (x : α) ↦ a * x) 0) = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
have refine_1 : gcd 0 = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
Tactic: simp_rw [map_zero, gcd_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s : Multiset α
refine_1 : gcd 0 = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
⊢ gcd (map (fun (x : α) ↦ a * x) 0) = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
have refine_1₁ : 0 = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (0 : α)
Tactic: simp_rw [map_zero, gcd_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s_1 : Multiset α
b : α
s : Multiset α
ih : gcd (map (fun (x : α) ↦ a * x) s) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd
⊢ gcd (map (fun (x : α) ↦ a * x) (b ::ₘ s)) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (b ::ₘ s).gcd
have refine_2 : @GCDMonoid.gcd _ inst _ (a * b) (gcd (map (fun (x : α) ↦ a * x) s)) = @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)
Tactic: simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s_1 : Multiset α
b : α
s : Multiset α
ih : gcd (map (fun (x : α) ↦ a * x) s) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd
⊢ @GCDMonoid.gcd _ inst _ (a * b) (gcd (map (fun (x : α) ↦ a * x) s)) = @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)
have refine_2 : @GCDMonoid.gcd _ inst _ (a * b) (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd) =
  @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s_1 : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
have pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s_1 : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
have neg : ∀ (h : ¬a ∈ s), (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s_1 : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ s.gcd = @GCDMonoid.gcd _ inst _ a s.gcd
have pos : fold (@GCDMonoid.gcd _ inst _) 0 s = @GCDMonoid.gcd _ inst _ a (fold (@GCDMonoid.gcd _ inst _) 0 s)
Tactic: unfold gcd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s_1 : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ fold (@GCDMonoid.gcd _ inst _) 0 s = @GCDMonoid.gcd _ inst _ a (fold (@GCDMonoid.gcd _ inst _) 0 s)
have pos : @GCDMonoid.gcd _ inst _ a (fold (@GCDMonoid.gcd _ inst _) 0 (s.erase a)) =
  @GCDMonoid.gcd _ inst _ ((normalize : (a : α) → α) a) (fold (@GCDMonoid.gcd _ inst _) 0 (s.erase a))
Tactic: rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).gcd = @GCDMonoid.gcd _ inst _ s₁.gcd s₂.gcd
have rw : ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
Tactic: rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).gcd = @GCDMonoid.gcd _ inst _ s₁.gcd s₂.gcd
have rw : ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
Tactic: rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).gcd = @GCDMonoid.gcd _ inst _ a s.gcd
have rw : ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
Tactic: rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ (x : α), x ∈ s ∧ x ≠ 0
ht : s = map (fun (x : α) ↦ s.gcd * x) t
| s.gcd * t.gcd
have rw : s.gcd
Tactic: rw [← normalize_gcd, ← gcd_map_mul, ← ht]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ (x : α), x ∈ s ∧ x ≠ 0
ht : s = map (fun (x : α) ↦ s.gcd * x) t
⊢ s.gcd * t.gcd = s.gcd
have conv_lhs : s.gcd * t.gcd = s.gcd
Tactic: conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ (x : α), x ∈ s ∧ x ≠ 0
ht : s = map (fun (x : α) ↦ s.gcd * x) t
conv_lhs : s.gcd * t.gcd = s.gcd
⊢ s.gcd * t.gcd = s.gcd
have conv_lhs₁ : s.gcd = s.gcd
Tactic: conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ (x : α), x ∈ s ∧ x ≠ 0
ht : s = map (fun (x : α) ↦ s.gcd * x) t
⊢ ¬s.gcd = 0
have contrapose! : ∀ (hs : s.gcd = 0) (x : α) (_ : x ∈ s), x = 0
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have pos : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
Tactic: by_cases! h : ∀ x ∈ s, x = (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
pos : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have neg : ∀ (h : ∃ (x : α), x ∈ s ∧ x ≠ 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
Tactic: by_cases! h : ∀ x ∈ s, x = (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have h₁ : s = map (fun (x : α) ↦ s.gcd * x) (replicate s.card 1) ∧ Eq.{u_1 + 1} (α := α) (gcd (replicate s.card 1)) 1
Tactic: use replicate (card s) 1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map (fun (x : α) ↦ s.gcd * x) (replicate s.card 1) ∧ Eq.{u_1 + 1} (α := α) (gcd (replicate s.card 1)) 1
have h₁ : (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = 0) ∧ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have neg : ∀ (f : {a : α} → (h : a ∈ s) → α) (hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h),
  ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
Tactic: choose f hf using @gcd_dvd _ _ _ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have neg : s = map (fun (x : α) ↦ s.gcd * x) (pmap (p := Membership.mem s) (@f) s sorry)
Tactic: refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun (x : α) ↦ s.gcd * x) (pmap (p := Membership.mem s) (@f) s ⋯)
have neg : s = pmap (p := Membership.mem s) (fun (a : α) (h : a ∈ s) ↦ s.gcd * f h) s sorry
Tactic: rw [map_pmap]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
| s
have rw : pmap (p := Membership.mem s) (fun (a : α) (x : a ∈ s) ↦ id a) s sorry
Tactic: rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = pmap (p := Membership.mem s) (fun (a : α) (h : a ∈ s) ↦ s.gcd * f h) s ⋯
have neg : Eq (α := Multiset α) (pmap (p := Membership.mem s) (fun (a : α) (x : a ∈ s) ↦ id a) s sorry)
  (pmap (p := Membership.mem s) (fun (a : α) (h : a ∈ s) ↦ s.gcd * f h) s sorry)
Tactic: conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ Eq (α := Multiset α) (pmap (p := Membership.mem s) (fun (a : α) (x : a ∈ s) ↦ id a) s ⋯)
    (pmap (p := Membership.mem s) (fun (a : α) (h : a ∈ s) ↦ s.gcd * f h) s ⋯)
have neg : ∀ (x : α) (hx : x ∈ s), id x = s.gcd * f hx
Tactic: congr with (x hx)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
⊢ id x = s.gcd * f hx
have neg : x = s.gcd * f hx
Tactic: rw [id, ← hf hx]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
f : {a : α} → (h : a ∈ s) → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
neg : x = s.gcd * f hx
⊢ id x = s.gcd * f hx
have neg₁ : x = x
Tactic: rw [id, ← hf hx]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have pos : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
Tactic: classical
    by_cases! h : ∀ x ∈ s, x = (0 : α)
    · use replicate (card s) 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]
      exact ⟨⟨rfl, h⟩, normalize_one⟩
    · choose f hf using @gcd_dvd _ _ _ s
      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)
        rw [id, ← hf hx]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
pos : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have neg : ∀ (h : ¬∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
Tactic: classical
    by_cases! h : ∀ x ∈ s, x = (0 : α)
    · use replicate (card s) 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]
      exact ⟨⟨rfl, h⟩, normalize_one⟩
    · choose f hf using @gcd_dvd _ _ _ s
      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)
        rw [id, ← hf hx]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
pos : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
neg : ∀ (h : ¬∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
pos₁ : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
neg₁ : ∀ (h : ¬∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
pos₂ : ∀ (h : ∀ (x : α), x ∈ s → x = 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
have neg₂ : ∀ (h : ∃ (x : α), x ∈ s ∧ x ≠ 0), ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1
Tactic: classical
    by_cases! h : ∀ x ∈ s, x = (0 : α)
    · use replicate (card s) 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]
      exact ⟨⟨rfl, h⟩, normalize_one⟩
    · choose f hf using @gcd_dvd _ _ _ s
      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)
        rw [id, ← hf hx]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℕ
⊢ Associated (a.gcd b * a.lcm b) (a * b)
have rw : Associated (a * b) (a * b)
Tactic: rw [Nat.gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
have inl : ∀ (ha : a < 0), (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
Tactic: rcases hna.lt_or_gt with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
inl :
  ∀ (ha : a < 0),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
have inr : ∀ (ha : 0 < a), (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
Tactic: rcases hna.lt_or_gt with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
have inl : ∀ (hb : b < 0), (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
Tactic: rcases hnb.lt_or_gt with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
inl :
  ∀ (hb : b < 0),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
have inl₁ : ∀ (hb : 0 < b), (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
Tactic: rcases hnb.lt_or_gt with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
have inr : ∀ (hb : b < 0), (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
Tactic: rcases hnb.lt_or_gt with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
inr :
  ∀ (hb : b < 0),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
have inr₁ : ∀ (hb : 0 < b), (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
Tactic: rcases hnb.lt_or_gt with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : 0 ≤ z
⊢ (normalize : (a : ℤ) → ℤ) z = z
have rw : z * (↑(normUnit z) : ℤ) = z
Tactic: rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : 0 ≤ z
rw : z * (↑(normUnit z) : ℤ) = z
⊢ (normalize : (a : ℤ) → ℤ) z = z
have rw₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = z
Tactic: rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : 0 ≤ z
rw : z * (↑(normUnit z) : ℤ) = z
rw₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = z
⊢ (normalize : (a : ℤ) → ℤ) z = z
have rw₂ : z * (↑1 : ℤ) = z
Tactic: rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : 0 ≤ z
rw : z * (↑(normUnit z) : ℤ) = z
rw₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = z
rw₂ : z * (↑1 : ℤ) = z
⊢ (normalize : (a : ℤ) → ℤ) z = z
have rw₃ : z * 1 = z
Tactic: rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : 0 ≤ z
rw : z * (↑(normUnit z) : ℤ) = z
rw₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = z
rw₂ : z * (↑1 : ℤ) = z
rw₃ : z * 1 = z
⊢ (normalize : (a : ℤ) → ℤ) z = z
have rw₄ : z = z
Tactic: rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : z ≤ 0
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inl : ∀ (h : LE.le (α := ℤ) 0 0), Eq (α := ℤ) ((normalize : (a : ℤ) → ℤ) 0 : ℤ) (-0 : ℤ)
Tactic: obtain rfl | h := h.eq_or_lt
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h : z ≤ 0
inl : ∀ (h : LE.le (α := ℤ) 0 0), Eq (α := ℤ) ((normalize : (a : ℤ) → ℤ) 0 : ℤ) (-0 : ℤ)
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr : ∀ (h : z < 0), (normalize : (a : ℤ) → ℤ) z = -z
Tactic: obtain rfl | h := h.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr : z * (↑(normUnit z) : ℤ) = -z
Tactic: rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
inr : z * (↑(normUnit z) : ℤ) = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = -z
Tactic: rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
inr : z * (↑(normUnit z) : ℤ) = -z
inr₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr₂ : z * (↑(-1) : ℤ) = -z
Tactic: rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
inr : z * (↑(normUnit z) : ℤ) = -z
inr₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = -z
inr₂ : z * (↑(-1) : ℤ) = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr₃ : z * -(↑1 : ℤ) = -z
Tactic: rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
inr : z * (↑(normUnit z) : ℤ) = -z
inr₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = -z
inr₂ : z * (↑(-1) : ℤ) = -z
inr₃ : z * -(↑1 : ℤ) = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr₄ : z * -1 = -z
Tactic: rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
inr : z * (↑(normUnit z) : ℤ) = -z
inr₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = -z
inr₂ : z * (↑(-1) : ℤ) = -z
inr₃ : z * -(↑1 : ℤ) = -z
inr₄ : z * -1 = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z
have inr₅ : -z = -z
Tactic: rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
⊢ |z| = (normalize : (a : ℤ) → ℤ) z
have inl : 0 ≤ z → |z| = (normalize : (a : ℤ) → ℤ) z
Tactic: cases le_total 0 z
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
inl : 0 ≤ z → |z| = (normalize : (a : ℤ) → ℤ) z
⊢ |z| = (normalize : (a : ℤ) → ℤ) z
have inr : z ≤ 0 → |z| = (normalize : (a : ℤ) → ℤ) z
Tactic: cases le_total 0 z
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
⊢ 0 ≤ z
have pos : ∀ (h : 0 ≤ z), 0 ≤ z
Tactic: by_cases! h : 0 ≤ z