awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
pos : a = 0 ∧ b = 0 → a = 0 ∨ b = 0 → Associated (HMul.hMul (α := G₀) 0 0) (a * b)
neg : a = 0 ∧ b = 0 → ¬(a = 0 ∨ b = 0) → Associated (HMul.hMul (α := G₀) 0 1) (a * b)
⊢ Associated (HMul.hMul (α := G₀) (if a = 0 ∧ b = 0 then 0 else 1) (if a = 0 ∨ b = 0 then 0 else 1)) (a * b)
have pos₁ : ¬(a = 0 ∧ b = 0) → a = 0 ∨ b = 0 → Associated (HMul.hMul (α := G₀) 1 0) (a * b)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
pos : a = 0 ∧ b = 0 → a = 0 ∨ b = 0 → Associated (HMul.hMul (α := G₀) 0 0) (a * b)
neg : a = 0 ∧ b = 0 → ¬(a = 0 ∨ b = 0) → Associated (HMul.hMul (α := G₀) 0 1) (a * b)
pos₁ : ¬(a = 0 ∧ b = 0) → a = 0 ∨ b = 0 → Associated (HMul.hMul (α := G₀) 1 0) (a * b)
⊢ Associated (HMul.hMul (α := G₀) (if a = 0 ∧ b = 0 then 0 else 1) (if a = 0 ∨ b = 0 then 0 else 1)) (a * b)
have neg₁ : ¬(a = 0 ∧ b = 0) → ¬(a = 0 ∨ b = 0) → Associated (HMul.hMul (α := G₀) 1 1) (a * b)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ Associated
    (HMul.hMul (α := Associates α)
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)))
    (HMul.hMul (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
have mk : HMul.hMul (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) sorry
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) sorry
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)) =
  HMul.hMul (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)
Tactic: rw [associated_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a
have apply : (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
Tactic: apply Iff.trans Multiset.lcm_dvd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
have simp : (∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
Tactic: simp only [Multiset.mem_map, and_imp, exists_imp]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
have pos : ∀ (h : b ∈ s), (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
Tactic: by_cases h : b ∈ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
pos : ∀ (h : b ∈ s), (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
have neg : ∀ (h : b ∉ s), (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
Tactic: by_cases h : b ∈ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
have pos : s.lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
Tactic: rw [insert_eq_of_mem h,
      (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∈ s
pos : s.lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
have pos₁ : s.lcm f = s.lcm f
Tactic: rw [insert_eq_of_mem h,
      (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
⊢ (∅ ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
have rw : s₂.lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
Tactic: rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
⊢ (∅ ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
have rw₁ : s₂.lcm f = @GCDMonoid.lcm _ inst _ 1 (s₂.lcm f)
Tactic: rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
rw₁ : s₂.lcm f = @GCDMonoid.lcm _ inst _ 1 (s₂.lcm f)
⊢ (∅ ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
have rw₂ : s₂.lcm f = (normalize : (a : α) → α) (s₂.lcm f)
Tactic: rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
rw₁ : s₂.lcm f = @GCDMonoid.lcm _ inst _ 1 (s₂.lcm f)
rw₂ : s₂.lcm f = (normalize : (a : α) → α) (s₂.lcm f)
⊢ (∅ ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
have rw₃ : s₂.lcm f = s₂.lcm f
Tactic: rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
have rw : (insert a (s ∪ s₂)).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
Tactic: rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)
rw : (insert a (s ∪ s₂)).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
have rw₁ : @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
Tactic: rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)
rw : (insert a (s ∪ s₂)).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₁ : @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
have rw₂ : @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) =
  @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
Tactic: rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)
rw : (insert a (s ∪ s₂)).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₁ : @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₂ :
  @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) =
    @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
have rw₃ : @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)) =
  @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
Tactic: rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)
rw : (insert a (s ∪ s₂)).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₁ : @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₂ :
  @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) =
    @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
rw₃ :
  @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)) =
    @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
have rw₄ : @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)) =
  @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f))
Tactic: rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.lcm f = s₂.lcm g
have subst : ∀ (hfg : ∀ a ∈ s₁, f a = g a), s₁.lcm f = s₁.lcm g
Tactic: subst hs
Cleared hypotheses: s₂, hs, hfg
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).lcm f = s.lcm (f ∘ g)
have empty : (image g ∅).lcm f = lcm ∅ (f ∘ g)
Tactic: induction s using Finset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).lcm f = lcm ∅ (f ∘ g)
⊢ (image g s).lcm f = s.lcm (f ∘ g)
have insert : ∀ (a : γ) (s : Finset γ),
  a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (insert a s)).lcm f = (insert a s).lcm (f ∘ g)
Tactic: induction s using Finset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).lcm f = s.lcm (f ∘ g)
have empty : (image g ∅).lcm f = lcm ∅ (f ∘ g)
Tactic: classical induction s using Finset.induction <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).lcm f = lcm ∅ (f ∘ g)
⊢ (image g s).lcm f = s.lcm (f ∘ g)
have insert : ∀ (a : γ) (s : Finset γ),
  a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (insert a s)).lcm f = (insert a s).lcm (f ∘ g)
Tactic: classical induction s using Finset.induction <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b
have apply : (∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
Tactic: apply Iff.trans Multiset.dvd_gcd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
have simp : (∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
Tactic: simp only [Multiset.mem_map, and_imp, exists_imp]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
have pos : ∀ (h : b ∈ s), (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
Tactic: by_cases h : b ∈ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
pos : ∀ (h : b ∈ s), (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
have neg : ∀ (h : b ∉ s), (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
Tactic: by_cases h : b ∈ s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
have pos : s.gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
Tactic: rw [insert_eq_of_mem h,
      (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∈ s
pos : s.gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
have pos₁ : s.gcd f = s.gcd f
Tactic: rw [insert_eq_of_mem h,
      (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
⊢ (∅ ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
have rw : s₂.gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
Tactic: rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
⊢ (∅ ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
have rw₁ : s₂.gcd f = @GCDMonoid.gcd _ inst _ 0 (s₂.gcd f)
Tactic: rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
rw₁ : s₂.gcd f = @GCDMonoid.gcd _ inst _ 0 (s₂.gcd f)
⊢ (∅ ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
have rw₂ : s₂.gcd f = (normalize : (a : α) → α) (s₂.gcd f)
Tactic: rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
rw₁ : s₂.gcd f = @GCDMonoid.gcd _ inst _ 0 (s₂.gcd f)
rw₂ : s₂.gcd f = (normalize : (a : α) → α) (s₂.gcd f)
⊢ (∅ ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
have rw₃ : s₂.gcd f = s₂.gcd f
Tactic: rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
have rw : (insert a (s ∪ s₂)).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
Tactic: rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)
rw : (insert a (s ∪ s₂)).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
have rw₁ : @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
Tactic: rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)
rw : (insert a (s ∪ s₂)).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₁ : @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
have rw₂ : @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) =
  @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
Tactic: rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)
rw : (insert a (s ∪ s₂)).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₁ : @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₂ :
  @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) =
    @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
have rw₃ : @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)) =
  @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
Tactic: rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)
rw : (insert a (s ∪ s₂)).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₁ : @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₂ :
  @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) =
    @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
rw₃ :
  @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)) =
    @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
have rw₄ : @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)) =
  @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f))
Tactic: rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.gcd f = s₂.gcd g
have subst : ∀ (hfg : ∀ a ∈ s₁, f a = g a), s₁.gcd f = s₁.gcd g
Tactic: subst hs
Cleared hypotheses: s₂, hs, hfg
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).gcd f = s.gcd (f ∘ g)
have empty : (image g ∅).gcd f = gcd ∅ (f ∘ g)
Tactic: induction s using Finset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).gcd f = gcd ∅ (f ∘ g)
⊢ (image g s).gcd f = s.gcd (f ∘ g)
have insert : ∀ (a : γ) (s : Finset γ),
  a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (insert a s)).gcd f = (insert a s).gcd (f ∘ g)
Tactic: induction s using Finset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).gcd f = s.gcd (f ∘ g)
have empty : (image g ∅).gcd f = gcd ∅ (f ∘ g)
Tactic: classical induction s using Finset.induction <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).gcd f = gcd ∅ (f ∘ g)
⊢ (image g s).gcd f = s.gcd (f ∘ g)
have insert : ∀ (a : γ) (s : Finset γ),
  a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (insert a s)).gcd f = (insert a s).gcd (f ∘ g)
Tactic: classical induction s using Finset.induction <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
have empty : gcd ∅ f = 0 ↔ ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → f x = 0
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s h ih => grind [gcd_cons, _root_.gcd_eq_zero_iff]