awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
ha₁ : s.gcd f ≠ 0
⊢ f a / s.gcd f = g a

Tactic:
rw [he a ha, mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ s.gcd f ≠ 0

Tactic:
mt Finset.gcd_eq_zero_iff.1 fun h ↦ hfi <| h i his

Premises used: Finset.gcd_eq_zero_iff, mt, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ s.gcd f ≠ 0

Tactic:
exact mt Finset.gcd_eq_zero_iff.1 fun h ↦ hfi <| h i his

Premises used: Finset.gcd_eq_zero_iff, mt, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
s : Finset α
a : α
has : a ∈ s
ha : a ≠ 0
⊢ Eq (α := α) (s.gcd fun (b : α) ↦ b / s.gcd id) 1

Tactic:
gcd_div_eq_one has ha

Premises used: Finset.gcd_div_eq_one
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
revert :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)

Tactic:
revert h
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)

Tactic:
s.induction_on ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
refine_1 :
  ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
refine_2 :
  ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (∀ (h : ∀ x ∈ s, a ∣ f x - g x),
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
            @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)) →
        ∀ (h : ∀ x ∈ insert a_1 s, a ∣ f x - g x),
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert a_1 s).gcd f) =
            @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert a_1 s).gcd g)
⊢ ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)

Tactic:
refine s.induction_on ?_ ?_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f g : β → α
a : α
b : β
s : Finset β
refine_2 :
  b ∉ s →
    (∀ (h : ∀ x ∈ s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)) →
      ∀ (h : ∀ x ∈ insert b s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd g)
⊢ b ∉ s →
    (∀ (h : ∀ x ∈ s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)) →
      ∀ (h : ∀ x ∈ insert b s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd g)

Tactic:
_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f g : β → α
a : α
b : β
s : Finset β
h_1 : b ∉ s
hi :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
refine_2 :
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
      (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (f b)) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
      (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (g b))
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd g)

Tactic:
rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]

Premises used: gcd_assoc, gcd_comm, GCDMonoid.gcd, Finset.mem_insert_of_mem, Finset.gcd_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f g : β → α
a : α
b : β
s : Finset β
h_1 : b ∉ s
hi :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
      (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (f b)) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
      (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (g b))

Tactic:
congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))

Premises used: Finset.mem_insert_self, congr_arg, gcd_eq_of_dvd_sub_right
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f g : β → α
a : α
b : β
s : Finset β
h_1 : b ∉ s
hi :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
      (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (f b)) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
      (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (g b))

Tactic:
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))

Premises used: Finset.mem_insert_self, congr_arg, gcd_eq_of_dvd_sub_right
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
revert :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
refine_1 :
  ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
refine_2 refine_2₁ refine_2₂ :
  ∀ (b : β) (s : Finset β),
    b ∉ s →
      ∀
        (hi :
          ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
            @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
              @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g))
        (h : ∀ x ∈ insert b s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd g)
refine_2₃ :
  ∀ (b : β) (s : Finset β),
    b ∉ s →
      ∀
        (hi :
          ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
            @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
              @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g))
        (h : ∀ x ∈ insert b s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
            (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (f b)) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
            (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (g b))
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)

Tactic:
classical
    revert h
    refine s.induction_on ?_ ?_
    · simp
    intro b s _ hi h
    rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
    exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))

Premises used: gcd_assoc, gcd_comm, congr_arg, GCDMonoid.gcd, gcd_eq_of_dvd_sub_right, Finset.gcd_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ gcd ∅ f

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
s_1 : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
cons : LE.le (α := ℤ) 0 (↑((f a).gcd (s.gcd f)) : ℤ)
⊢ 0 ≤ (Finset.cons a s has).gcd f

Tactic:
rw [gcd_cons, ← Int.coe_gcd]

Premises used: Finset.gcd_cons, Int.coe_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
s_1 : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ LE.le (α := ℤ) 0 (↑((f a).gcd (s.gcd f)) : ℤ)

Tactic:
grind
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
empty : 0 ≤ gcd ∅ f
cons : ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : 0 ≤ s.gcd f), 0 ≤ (Finset.cons a s has).gcd f
⊢ 0 ≤ s.gcd f

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [gcd_cons, ← Int.coe_gcd]
    grind

Premises used: Finset.cons, Finset.gcd_cons, Int.coe_gcd
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset ι
f : ι → α
⊢ s.lcm f ∣ s.prod f

Tactic:
lcm_dvd fun _ ↦ dvd_prod_of_mem _

Premises used: Finset.dvd_prod_of_mem, Finset.lcm_dvd
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset ι
f : ι → α
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
⊢ Associated (s.lcm f) (s.prod f)

Tactic:
associated_of_dvd_dvd (s.lcm_dvd_prod f) (s.prod_dvd_of_isRelPrime h fun _ ↦ dvd_lcm)

Premises used: associated_of_dvd_dvd, Finset.lcm_dvd_prod, Finset.prod_dvd_of_isRelPrime, Finset.dvd_lcm
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun Nat.Coprime f)
h₁ : ∀ (x x_1 : ℕ), x.Coprime x_1 ↔ IsRelPrime x x_1
⊢ Nat.Coprime = IsRelPrime

Tactic:
ext
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun Nat.Coprime f)
x x_1 : ℕ
⊢ x.Coprime x_1 ↔ IsRelPrime x x_1

Tactic:
Nat.coprime_iff_isRelPrime

Premises used: Nat.coprime_iff_isRelPrime
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun Nat.Coprime f)
x x_1 : ℕ
⊢ x.Coprime x_1 ↔ IsRelPrime x x_1

Tactic:
exact Nat.coprime_iff_isRelPrime

Premises used: Nat.coprime_iff_isRelPrime
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun Nat.Coprime f)
⊢ (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)

Tactic:
rw [show Nat.Coprime = IsRelPrime by ext; exact Nat.coprime_iff_isRelPrime] at h
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
⊢ s.lcm f = s.prod f

Tactic:
associated_lcm_prod h |>.eq_of_normalized (normalize_eq _) (normalize_eq _)

Premises used: Associated.eq_of_normalized, Finset.associated_lcm_prod, normalize_eq
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
⊢ s.lcm f = s.prod f

Tactic:
exact associated_lcm_prod h |>.eq_of_normalized (normalize_eq _) (normalize_eq _)

Premises used: Associated.eq_of_normalized, Finset.associated_lcm_prod, normalize_eq
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
f : ι → ℕ
p : ℕ
hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0
⊢ Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
f : ι → ℕ
p : ℕ
a : ι
s : Finset ι
h : a ∉ s
h_1 :
  ∀ (hf : ∀ k ∈ s, f k ≠ 0),
    Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
      (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
hf : ∀ k ∈ insert a s, f k ≠ 0
⊢ Eq (α := ℕ) ((((insert a s).lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((insert a s).sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]

Premises used: Nat.factorization_lcm, lcm_eq_nat_lcm
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
empty :
  ∀ (hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0),
    Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
      (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (hf : ∀ k ∈ s, f k ≠ 0),
          Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
            (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)) →
        ∀ (hf : ∀ k ∈ Insert.insert a s, f k ≠ 0),
          Eq (α := ℕ) ((((Insert.insert a s).lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
            ((Insert.insert a s).sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]

Premises used: Insert.insert, Nat.factorization_lcm, lcm_eq_nat_lcm
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
empty :
  ∀ (hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0),
    Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
      (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (hf : ∀ k ∈ s, f k ≠ 0),
          Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
            (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)) →
        ∀ (hf : ∀ k ∈ Insert.insert a s, f k ≠ 0),
          Eq (α := ℕ) ((((Insert.insert a s).lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
            ((Insert.insert a s).sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]

Premises used: Insert.insert, Nat.factorization_lcm, lcm_eq_nat_lcm
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
⊢ Rat.den (∑ i ∈ ∅, f i) ∣ lcm ∅ fun (i : ι) ↦ (f i).den

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
insert :
  (f a + ∑ x ∈ s, f x).den ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (f a).den (s.lcm fun (i : ι) ↦ (f i).den)
⊢ Rat.den (∑ i ∈ Insert.insert a s, f i) ∣ (Insert.insert a s).lcm fun (i : ι) ↦ (f i).den

Tactic:
rw [Finset.sum_insert has, Finset.lcm_insert]

Premises used: Finset.sum_insert, Finset.lcm_insert
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
⊢ (f a + ∑ x ∈ s, f x).den ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (f a).den (s.lcm fun (i : ι) ↦ (f i).den)

Tactic:
(Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)

Premises used: Rat.add_den_dvd_lcm, lcm_dvd_lcm, dvd_rfl, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
⊢ (f a + ∑ x ∈ s, f x).den ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (f a).den (s.lcm fun (i : ι) ↦ (f i).den)

Tactic:
exact (Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)

Premises used: Rat.add_den_dvd_lcm, lcm_dvd_lcm, dvd_rfl, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∑ i ∈ ∅, f i) ∣ lcm ∅ fun (i : ι) ↦ (f i).den
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den),
    Rat.den (∑ i ∈ Insert.insert a s, f i) ∣ (Insert.insert a s).lcm fun (i : ι) ↦ (f i).den
⊢ Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    rw [Finset.sum_insert has, Finset.lcm_insert]
    exact (Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)

Premises used: Insert.insert, Finset.lcm_insert
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∑ i ∈ ∅, f i) ∣ lcm ∅ fun (i : ι) ↦ (f i).den
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den),
    Rat.den (∑ i ∈ Insert.insert a s, f i) ∣ (Insert.insert a s).lcm fun (i : ι) ↦ (f i).den
⊢ Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    rw [Finset.sum_insert has, Finset.lcm_insert]
    exact (Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)

Premises used: Insert.insert, Finset.lcm_insert
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ Rat.den (∑ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den

Tactic:
(den_sum_dvd_lcm_den s f).trans <| s.lcm_dvd_prod _

Premises used: Finset.lcm_dvd_prod, Dvd.dvd.trans, Finset.Rat.den_sum_dvd_lcm_den
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
⊢ Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (f i).den

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
insert : (f a * ∏ i ∈ s, f i).den ∣ (f a).den * ∏ i ∈ s, (f i).den
⊢ Rat.den (∏ i ∈ Insert.insert a s, f i) ∣ ∏ i ∈ Insert.insert a s, (f i).den

Tactic:
simp_rw [Finset.prod_insert has]

Premises used: Finset.prod_insert
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
⊢ (f a * ∏ i ∈ s, f i).den ∣ (f a).den * ∏ i ∈ s, (f i).den

Tactic:
(Rat.mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

Premises used: Rat.mul_den_dvd, mul_dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
⊢ (f a * ∏ i ∈ s, f i).den ∣ (f a).den * ∏ i ∈ s, (f i).den

Tactic:
exact (Rat.mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

Premises used: Rat.mul_den_dvd, mul_dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (f i).den
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den),
    Rat.den (∏ i ∈ Insert.insert a s, f i) ∣ ∏ i ∈ Insert.insert a s, (f i).den
⊢ Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    simp_rw [Finset.prod_insert has]
    exact (Rat.mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

Premises used: Rat.mul_den_dvd, Insert.insert, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (f i).den
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den),
    Rat.den (∏ i ∈ Insert.insert a s, f i) ∣ ∏ i ∈ Insert.insert a s, (f i).den
⊢ Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    simp_rw [Finset.prod_insert has]
    exact (Rat.mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

Premises used: Rat.mul_den_dvd, Insert.insert, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : GCDMonoid R
M : Submonoid R
inst_4 : IsLocalization M A
z : A
obtain :
  ∀ (x y : R) (hy : y ∈ M),
    ∃ (a : R) (b : R),
      IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ a b) ∧
        HMul.hMul (β := A) (mk' A x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy))
            ((algebraMap R A : (a : R) → A) b : A) =
          (algebraMap R A : (a : R) → A) a
⊢ ∃ (a : R) (b : R),
    IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ a b) ∧
      HMul.hMul (β := A) z ((algebraMap R A : (a : R) → A) b : A) = (algebraMap R A : (a : R) → A) a

Tactic:
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.exists_mk'_eq M z

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : GCDMonoid R
M : Submonoid R
inst_4 : IsLocalization M A
x y : R
hy : y ∈ M
obtain :
  ∀ (x' y' : R) (hx' : x = @gcd _ CommSemiring.toCommMonoidWithZero _ x y * x')
    (hy' : y = @gcd _ CommSemiring.toCommMonoidWithZero _ x y * y')
    (hu : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x' y')),
    ∃ (a : R) (b : R),
      IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ a b) ∧
        HMul.hMul (β := A) (mk' A x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy))
            ((algebraMap R A : (a : R) → A) b : A) =
          (algebraMap R A : (a : R) → A) a
⊢ ∃ (a : R) (b : R),
    IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ a b) ∧
      HMul.hMul (β := A) (mk' A x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy)) ((algebraMap R A : (a : R) → A) b : A) =
        (algebraMap R A : (a : R) → A) a

Tactic:
obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y

Premises used: extract_gcd