awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
rw : ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
⊢ (s₁ ∪ s₂).lcm = @GCDMonoid.lcm _ inst _ s₁.lcm s₂.lcm

Tactic:
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.lcm_add, Multiset.lcm_dedup
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
a : α
s : Multiset α
rw : ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
⊢ (ndinsert a s).lcm = @GCDMonoid.lcm _ inst _ a s.lcm

Tactic:
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.lcm_dedup, Multiset.lcm_cons
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
⊢ Eq.{u_1 + 1} (α := α) (gcd 0) 0

Tactic:
fold_zero _ _

Premises used: Multiset.gcd, Multiset.fold_zero
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (a ::ₘ s).gcd = @GCDMonoid.gcd _ inst _ a s.gcd

Tactic:
fold_cons_left _ _ _ _

Premises used: Multiset.fold_cons_left, Multiset.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ Eq (α := α) (gcd {a} : α) ((normalize : (a : α) → α) a : α)

Tactic:
(fold_singleton _ _ _).trans <| gcd_zero_right _

Premises used: Multiset.gcd, gcd_zero_right, Multiset.fold_singleton, Eq.trans
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).gcd = fold (@GCDMonoid.gcd _ inst _) (@GCDMonoid.gcd _ inst _ 0 0) (s₁ + s₂)

Tactic:
simp [gcd]

Premises used: Multiset.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ a ∣ gcd 0 ↔ ∀ (b : α), Membership.mem (γ := Multiset α) 0 b → a ∣ b

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (a ∣ s.gcd ↔ ∀ (b : α), b ∈ s → a ∣ b) → (a ∣ (a_1 ::ₘ s).gcd ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ∣ b)

Tactic:
simp +contextual [or_imp, forall_and, dvd_gcd_iff]

Premises used: or_imp, forall_and, dvd_gcd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
a : α
h : a ∈ s
⊢ s.gcd ∣ a

Tactic:
dvd_gcd.1 dvd_rfl _ h

Premises used: Multiset.dvd_gcd, Iff.mp, dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
h : s₁ ⊆ s₂
⊢ s₂.gcd ∣ s₁.gcd

Tactic:
dvd_gcd.2 fun _ hb ↦ gcd_dvd (h hb)

Premises used: Iff.mpr, Multiset.dvd_gcd, Multiset.gcd_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) (gcd 0) : α) (gcd 0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Multiset α
a : α
s : Multiset α
h : (normalize : (a : α) → α) s.gcd = s.gcd
⊢ (normalize : (a : α) → α) (a ::ₘ s).gcd = (a ::ₘ s).gcd

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
mp : s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0
mpr : (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
mp : 0 ∣ x
⊢ x = 0

Tactic:
apply eq_zero_of_zero_dvd

Premises used: eq_zero_of_zero_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
mp : s.gcd ∣ x
⊢ 0 ∣ x

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ s.gcd ∣ x

Tactic:
apply gcd_dvd hx

Premises used: Multiset.gcd_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0

Tactic:
s.induction_on ?_ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
mpr : (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x = 0) → Eq.{u_1 + 1} (α := α) (gcd 0) 0
mpr₁ :
  ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → x = 0) → s.gcd = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → (a ::ₘ s).gcd = 0
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0

Tactic:
refine s.induction_on ?_ ?_
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x = 0) → Eq.{u_1 + 1} (α := α) (gcd 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Multiset α
a : α
s : Multiset α
sgcd : (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
h : ∀ (x : α), x ∈ a ::ₘ s → x = 0
⊢ (a ::ₘ s).gcd = 0

Tactic:
simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]

Premises used: Multiset.mem_cons_of_mem, Multiset.mem_cons_self
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd ≠ 0 ↔ ∃ (x : α), x ∈ s ∧ x ≠ 0

Tactic:
simp [gcd_eq_zero_iff]

Premises used: Multiset.gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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

Tactic:
s.induction_on ?_ fun b s ih ↦ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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 : α)
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
⊢ gcd (map (fun (x : α) ↦ a * x) s) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd

Tactic:
refine s.induction_on ?_ fun b s ih ↦ ?_
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
s : Multiset α
refine_1 : gcd 0 = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)
refine_1₁ : 0 = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (0 : α)
⊢ gcd (map (fun (x : α) ↦ a * x) 0) = HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (gcd 0 : α)

Tactic:
simp_rw [map_zero, gcd_zero, mul_zero]

Premises used: Multiset.map_zero, MulZeroClass.mul_zero, Multiset.gcd_zero
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
refine_2 :
  @GCDMonoid.gcd _ inst _ (a * b) (gcd (map (fun (x : α) ↦ a * x) s)) = @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)
⊢ gcd (map (fun (x : α) ↦ a * x) (b ::ₘ s)) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (b ::ₘ s).gcd

Tactic:
simp_rw [map_cons, gcd_cons, ← gcd_mul_left]

Premises used: gcd_mul_left, Multiset.map_cons, Multiset.gcd_cons
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
refine_2 :
  @GCDMonoid.gcd _ inst _ (a * b) (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd) =
    @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)
⊢ @GCDMonoid.gcd _ inst _ (a * b) (gcd (map (fun (x : α) ↦ a * x) s)) = @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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) (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) s.gcd) =
    @GCDMonoid.gcd _ inst _ (a * b) (a * s.gcd)

Tactic:
apply ((normalize_associated a).mul_right _).gcd_eq_right

Premises used: Associated.gcd_eq_right, Associated.mul_right, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s : Multiset α
⊢ Eq.{u_1 + 1} (α := α) (gcd (dedup 0)) (gcd 0)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg : ∀ (h : ¬a ∈ s), (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
simp [IH, h]
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
pos : fold (@GCDMonoid.gcd _ inst _) 0 s = @GCDMonoid.gcd _ inst _ a (fold (@GCDMonoid.gcd _ inst _) 0 s)
⊢ s.gcd = @GCDMonoid.gcd _ inst _ a s.gcd

Tactic:
unfold gcd

Premises used: Multiset.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
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))
⊢ fold (@GCDMonoid.gcd _ inst _) 0 s = @GCDMonoid.gcd _ inst _ a (fold (@GCDMonoid.gcd _ inst _) 0 s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]

Premises used: Multiset.fold_cons_left, gcd_assoc, gcd_same, Multiset.cons_erase
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
⊢ @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:
apply (associated_normalize _).gcd_eq_left

Premises used: Associated.gcd_eq_left, associated_normalize
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
rw : ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
⊢ (s₁.ndunion s₂).gcd = @GCDMonoid.gcd _ inst _ s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.gcd_dedup, Multiset.gcd_add
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
rw : ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
⊢ (s₁ ∪ s₂).gcd = @GCDMonoid.gcd _ inst _ s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.gcd_dedup, Multiset.gcd_add
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
a : α
s : Multiset α
rw : ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
⊢ (ndinsert a s).gcd = @GCDMonoid.gcd _ inst _ a s.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.gcd_dedup, Multiset.gcd_cons
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
rw : s.gcd
| s.gcd * t.gcd

Tactic:
rw [← normalize_gcd, ← gcd_map_mul, ← ht]

Premises used: Multiset.normalize_gcd, Multiset.gcd_map_mul
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
conv_lhs₁ : s.gcd = s.gcd
⊢ s.gcd * t.gcd = s.gcd

Tactic:
conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]

Premises used: Multiset.normalize_gcd, Multiset.gcd_map_mul
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
contrapose! : ∀ (hs : s.gcd = 0) (x : α) (_ : x ∈ s), x = 0
⊢ ¬s.gcd = 0

Tactic:
contrapose! hs
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map (fun (x : α) ↦ s.gcd * x) t
hs : s.gcd = 0
⊢ ∀ (x : α) (_ : x ∈ s), x = 0

Tactic:
s.gcd_eq_zero_iff.1 hs

Premises used: Iff.mp, Multiset.gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map (fun (x : α) ↦ s.gcd * x) t
hs : s.gcd = 0
⊢ ∀ (x : α) (_ : x ∈ s), x = 0

Tactic:
exact s.gcd_eq_zero_iff.1 hs

Premises used: Iff.mp, Multiset.gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1

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

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
h₁ : s = map (fun (x : α) ↦ s.gcd * x) (replicate s.card 1) ∧ Eq.{u_1 + 1} (α := α) (gcd (replicate s.card 1)) 1
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
use replicate (card s) 1

Premises used: Multiset.card, Multiset.replicate, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
h₁ : (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = 0) ∧ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (1 : α)
⊢ s = map (fun (x : α) ↦ s.gcd * x) (replicate s.card 1) ∧ Eq.{u_1 + 1} (α := α) (gcd (replicate s.card 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]

Premises used: Iff.mpr, Multiset.gcd_dedup, Multiset.dedup_nsmul, Multiset.gcd_singleton, Multiset.map_replicate, LT.lt.ne', Multiset.eq_replicate, Multiset.card_pos, Multiset.nsmul_singleton, mul_one, Multiset.gcd_eq_zero_iff, Multiset.dedup_singleton
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = 0) ∧ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (1 : α)

Tactic:
⟨⟨rfl, h⟩, normalize_one⟩

Premises used: normalize_one, And.intro, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = 0) ∧ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (1 : α)

Tactic:
exact ⟨⟨rfl, h⟩, normalize_one⟩
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ (x : α), x ∈ s ∧ x ≠ 0
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
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1

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

Premises used: Multiset.gcd_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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

Tactic:
⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩

Premises used: Multiset.extract_gcd', id, Multiset.pmap, And.intro, Exists.intro
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg neg₁ : s = map (fun (x : α) ↦ s.gcd * x) (pmap (p := Membership.mem s) (@f) s ⋯)
⊢ ∃ (t : Multiset α), s = map (fun (x : α) ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg : s = pmap (p := Membership.mem s) (fun (a : α) (h : a ∈ s) ↦ s.gcd * f h) s ⋯
⊢ s = map (fun (x : α) ↦ s.gcd * x) (pmap (p := Membership.mem s) (@f) s ⋯)

Tactic:
rw [map_pmap]

Premises used: Multiset.map_pmap
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
rw : pmap (p := Membership.mem s) (fun (a : α) (x : a ∈ s) ↦ id a) s ⋯
| s

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

Premises used: Multiset.map_id, Multiset.pmap_eq_map, id
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg :
  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 ⋯)
⊢ s = pmap (p := Membership.mem s) (fun (a : α) (h : a ∈ s) ↦ s.gcd * f h) s ⋯

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

Premises used: Multiset.map_id, Multiset.pmap_eq_map, id
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg : ∀ (x : α) (hx : x ∈ s), id x = s.gcd * f hx
⊢ 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 ⋯)

Tactic:
congr with (x hx)
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg₁ neg₂ : x = x
⊢ id x = s.gcd * f hx

Tactic:
rw [id, ← hf hx]

Premises used: id
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
neg₂ neg₃ : ∀ (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

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]

Premises used: Iff.mpr, Multiset.map_id, Multiset.pmap_eq_map, Multiset.gcd_dedup, Multiset.dedup_nsmul, id, Multiset.gcd_singleton, Multiset.map_replicate, LT.lt.ne', Multiset.map_pmap, Multiset.eq_replicate, Multiset.card_pos, Multiset.nsmul_singleton, Multiset.card, Multiset.gcd_dvd, mul_one, Multiset.replicate, OfNat.ofNat, Multiset.dedup_singleton
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℕ
rw : Associated (a * b) (a * b)
⊢ Associated (a.gcd b * a.lcm b) (a * b)

Tactic:
rw [Nat.gcd_mul_lcm]

Premises used: Nat.gcd_mul_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℕ
⊢ Associated (a * b) (a * b)

Tactic:
rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
m n : ℕ
⊢ @gcd _ Nat.instCommMonoidWithZero _ m n = m.gcd n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
m n : ℕ
⊢ @lcm _ Nat.instCommMonoidWithZero _ m n = m.lcm n

Tactic:
rfl

Premises used: rfl