awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
have empty : Rat.den (∑ i ∈ ∅, f i) ∣ 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∑ i ∈ ∅, f i) ∣ lcm ∅ fun (i : ι) ↦ (f i).den
⊢ Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
have 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 a s, f i) ∣ (insert a 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
⊢ Rat.den (∏ i ∈ insert a s, f i) ∣ ∏ i ∈ insert a s, (f i).den
have insert : (f a * ∏ i ∈ s, f i).den ∣ (f a).den * ∏ i ∈ s, (f i).den
Tactic: simp_rw [Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
have empty : Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (f i).den
⊢ Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den),
  Rat.den (∏ i ∈ insert a s, f i) ∣ ∏ i ∈ insert a 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
have empty : Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, (f i).den
⊢ Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∏ i ∈ s, f i) ∣ ∏ i ∈ s, (f i).den),
  Rat.den (∏ i ∈ insert a s, f i) ∣ ∏ i ∈ insert a 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.exists_mk'_eq M z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
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
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
have right : HMul.hMul (β := A) (mk' A x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy)) ((algebraMap R A : (a : R) → A) y' : A) =
  (algebraMap R A : (a : R) → A) x'
Tactic: use x', y', hu
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
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
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')
⊢ HMul.hMul (β := A) (mk' A x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy)) ((algebraMap R A : (a : R) → A) y' : A) =
    (algebraMap R A : (a : R) → A) x'
have right : mk' A (y' * x) (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) = (algebraMap R A : (a : R) → A) x'
Tactic: rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
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
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')
⊢ mk' A (y' * x) (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) = (algebraMap R A : (a : R) → A) x'
have h : y' * x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) * x'
Tactic: convert! IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : Nonempty.{u_1 + 1} (GCDMonoid R)
X : FractionRing R
h_1 : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
have intro : ∀ (val : GCDMonoid R), ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
have intro : ∀ (x y : R) (hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y))
  (he :
    HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
      (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x),
  ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
Tactic: obtain ⟨x, y, hg, he⟩ := IsLocalization.surj_of_gcd_domain (nonZeroDivisors R) X
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
rw :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
⊢ HMul.hMul (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) X =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
have rw₁ : Eq (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) x : FractionRing R)
  ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) x : FractionRing R)
Tactic: rw [mul_comm, he]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
have this : y ∣ x ^ p.natDegree
Tactic: have :=
      Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R <| FractionRing R)
        hp₁ y x _ hp₂ (by rw [mul_comm, he])
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this : y ∣ x ^ p.natDegree
⊢ IsUnit y
have rw : y ∣ HPow.hPow (α := R) 1 p.natDegree
Tactic: rw [isUnit_iff_dvd_one, ← one_pow]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this : y ∣ x ^ p.natDegree
rw : y ∣ HPow.hPow (α := R) 1 p.natDegree
⊢ IsUnit y
have rw₁ : ℕ
Tactic: rw [isUnit_iff_dvd_one, ← one_pow]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this : y ∣ x ^ p.natDegree
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
have this₁ : IsUnit y
Tactic: have : IsUnit y := by
      rw [isUnit_iff_dvd_one, ← one_pow]
      exact
        (dvd_gcd this <| dvd_refl y).trans
          (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this_1 : y ∣ x ^ p.natDegree
this : IsUnit y
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
have h : (algebraMap R (FractionRing R) : (a : R) → FractionRing R) (x * (↑this.unit⁻¹ : R)) = X
Tactic: use x * (this.unit⁻¹ :)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this_1 : y ∣ x ^ p.natDegree
this : IsUnit y
⊢ (algebraMap R (FractionRing R) : (a : R) → FractionRing R) (x * (↑this.unit⁻¹ : R)) = X
have h : HMul.hMul (α := FractionRing R) (β := FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) x : FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑this.unit⁻¹ : R) : FractionRing R) =
  X
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this_1 : y ∣ x ^ p.natDegree
this : IsUnit y
⊢ HMul.hMul (α := FractionRing R) (β := FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) x : FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑this.unit⁻¹ : R) : FractionRing R) =
    X
have coe_map_inv : Eq (α := FractionRing R)
  ((↑((Units.map (↑(algebraMap R (FractionRing R)) : R →* FractionRing R) : (a : Rˣ) → (FractionRing R)ˣ) this.unit)⁻¹ :
      FractionRing R) :
    FractionRing R)
  (((↑(algebraMap R (FractionRing R)) : R →* FractionRing R) : (a : R) → FractionRing R) (↑this.unit⁻¹ : R) :
    FractionRing R)
Tactic: have coe_map_inv :=
      Units.coe_map_inv ((algebraMap R (FractionRing R) : R →* FractionRing R)) this.unit
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
X : FractionRing R
h : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
val : GCDMonoid R
x y : R
hg : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y)
he :
  HMul.hMul (β := FractionRing R) X ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) y : FractionRing R) =
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
this_1 : y ∣ x ^ p.natDegree
this : IsUnit y
coe_map_inv :
  Eq (α := FractionRing R)
    ((↑((Units.map (↑(algebraMap R (FractionRing R)) : R →* FractionRing R) : (a : Rˣ) → (FractionRing R)ˣ)
              this.unit)⁻¹ :
        FractionRing R) :
      FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑this.unit⁻¹ : R) : FractionRing R)
⊢ HMul.hMul (α := FractionRing R) (β := FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) x : FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑this.unit⁻¹ : R) : FractionRing R) =
    X
have h : X *
    (↑((Units.map (↑(algebraMap R (FractionRing R)) : R →* FractionRing R) : (a : Rˣ) → (FractionRing R)ˣ) this.unit) :
      FractionRing R) =
  (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x
Tactic: rw [← coe_map_inv, eq_comm, Units.eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Nontrivial α
s : Multiset α
⊢ s.lcm = 0 ↔ 0 ∈ s
have empty : Eq.{u_1 + 1} (α := α) (lcm 0) 0 ↔ Membership.mem (γ := Multiset α) 0 0
Tactic: induction s using Multiset.induction_on with
  | empty => simp only [lcm_zero, one_ne_zero, notMem_zero]
  | cons a s ihs => simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Nontrivial α
s : Multiset α
empty : Eq.{u_1 + 1} (α := α) (lcm 0) 0 ↔ Membership.mem (γ := Multiset α) 0 0
⊢ s.lcm = 0 ↔ 0 ∈ s
have cons : ∀ (a : α) (s : Multiset α) (ihs : s.lcm = 0 ↔ 0 ∈ s), (a ::ₘ s).lcm = 0 ↔ 0 ∈ a ::ₘ s
Tactic: induction s using Multiset.induction_on with
  | empty => simp only [lcm_zero, one_ne_zero, notMem_zero]
  | cons a s ihs => simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]
Cleared hypotheses: 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.lcm = s.lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
have pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
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.lcm = s.lcm
pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
have neg : ∀ (h : ¬a ∈ s), (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
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.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
have pos : s.lcm = @GCDMonoid.lcm _ inst _ a s.lcm
Tactic: simp only [h, dedup_cons_of_mem, IH, lcm_cons]
-- 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.lcm = s.lcm
h : a ∈ s
⊢ s.lcm = @GCDMonoid.lcm _ inst _ a s.lcm
have pos : fold (@GCDMonoid.lcm _ inst _) 1 s = @GCDMonoid.lcm _ inst _ a (fold (@GCDMonoid.lcm _ inst _) 1 s)
Tactic: unfold lcm
-- 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.lcm = s.lcm
h : a ∈ s
⊢ fold (@GCDMonoid.lcm _ inst _) 1 s = @GCDMonoid.lcm _ inst _ a (fold (@GCDMonoid.lcm _ inst _) 1 s)
have pos : @GCDMonoid.lcm _ inst _ a (fold (@GCDMonoid.lcm _ inst _) 1 (s.erase a)) =
  @GCDMonoid.lcm _ inst _ ((normalize : (a : α) → α) a) (fold (@GCDMonoid.lcm _ inst _) 1 (s.erase a))
Tactic: rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_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₂).lcm = @GCDMonoid.lcm _ inst _ s₁.lcm s₂.lcm
have rw : ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
Tactic: rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_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₂).lcm = @GCDMonoid.lcm _ inst _ s₁.lcm s₂.lcm
have rw : ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
Tactic: rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_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).lcm = @GCDMonoid.lcm _ inst _ a s.lcm
have rw : ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
Tactic: rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0
have mp : s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
mp : s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0
have mpr : (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ x = 0
have mp : 0 ∣ x
Tactic: apply eq_zero_of_zero_dvd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x
have mp : s.gcd ∣ x
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
have mpr : (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x = 0) → Eq.{u_1 + 1} (α := α) (gcd 0) 0
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Multiset (goal)
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
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
have mpr₁ : ∀ (a : α) (s : Multiset α),
  ((∀ (x : α), x ∈ s → x = 0) → s.gcd = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → (a ::ₘ s).gcd = 0
Tactic: refine s.induction_on ?_ ?_