awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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')
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'
⊢ ∃ (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:
use x', y', hu
-- 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
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')
right : mk' A (y' * x) (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) = (algebraMap R A : (a : R) → A) x'
⊢ 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:
rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]

Premises used: mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul
-- 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
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 ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) * x') (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) =
    (algebraMap R A : (a : R) → A) x'

Tactic:
IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _

Premises used: IsLocalization.mk'_mul_cancel_left
-- 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
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')
h : y' * x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) * x'
⊢ mk' A (y' * x) (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) = (algebraMap R A : (a : R) → A) x'

Tactic:
convert! IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2

Premises used: IsLocalization.mk'_mul_cancel_left
-- 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
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')
⊢ y' * x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) * x'

Tactic:
grind
-- 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
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
intro : ∀ (val : GCDMonoid R), ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X

Tactic:
cases h
-- 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
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
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
⊢ ∃ (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

Premises used: nonZeroDivisors, IsLocalization.surj_of_gcd_domain
-- 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
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
rw₁ 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)
⊢ 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

Tactic:
rw [mul_comm, he]

Premises used: mul_comm
-- 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
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 ∣ 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])
-- 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
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
rw₁ : ℕ
⊢ IsUnit y

Tactic:
rw [isUnit_iff_dvd_one, ← one_pow]

Premises used: one_pow, isUnit_iff_dvd_one
-- 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
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 ∣ HPow.hPow (α := R) 1 p.natDegree

Tactic:
(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) _)

Premises used: pow_dvd_pow_of_dvd, GCDMonoid.dvd_gcd, Iff.mp, gcd_pow_left_dvd_pow_gcd, dvd_refl, isUnit_iff_dvd_one, 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
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

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) _)
-- 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
X : FractionRing R
h_1 : 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
h : (algebraMap R (FractionRing R) : (a : R) → FractionRing R) (x * (↑this.unit⁻¹ : R)) = X
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = X

Tactic:
use x * (this.unit⁻¹ :)

Premises used: Inv.inv, IsUnit.unit
-- 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
X : FractionRing R
h_1 : 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
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
⊢ (algebraMap R (FractionRing R) : (a : R) → FractionRing R) (x * (↑this.unit⁻¹ : R)) = X

Tactic:
rw [map_mul]

Premises used: map_mul
-- 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
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
⊢ 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
-- 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
X : FractionRing R
h_1 : 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)
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
⊢ 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 [← coe_map_inv, eq_comm, Units.eq_mul_inv_iff_mul_eq]

Premises used: eq_comm, Units.eq_mul_inv_iff_mul_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
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)
⊢ 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:
he

Premises used: Set.Mem, Quotient.mk', OreLocalization.oreDiv
-- 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
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)
⊢ 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:
exact he
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
⊢ Eq.{u_1 + 1} (α := α) (lcm 0) 1

Tactic:
fold_zero _ _

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

Tactic:
fold_cons_left _ _ _ _

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

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

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

Tactic:
simp [lcm]

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

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

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

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

Tactic:
lcm_dvd.1 dvd_rfl _ h

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

Tactic:
lcm_dvd.2 fun _ hb ↦ dvd_lcm (h hb)

Premises used: Iff.mpr, Multiset.dvd_lcm, Multiset.lcm_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Multiset α
⊢ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) (lcm 0) : α) (lcm 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.lcm = s.lcm
⊢ (normalize : (a : α) → α) (a ::ₘ s).lcm = (a ::ₘ s).lcm

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Nontrivial α
⊢ Eq.{u_1 + 1} (α := α) (lcm 0) 0 ↔ Membership.mem (γ := Multiset α) 0 0

Tactic:
simp only [lcm_zero, one_ne_zero, notMem_zero]

Premises used: Multiset.notMem_zero, Multiset.lcm_zero, one_ne_zero
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Nontrivial α
a : α
s : Multiset α
ihs : s.lcm = 0 ↔ 0 ∈ s
⊢ (a ::ₘ s).lcm = 0 ↔ 0 ∈ a ::ₘ s

Tactic:
simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]

Premises used: Multiset.lcm_eq_zero_iff, eq_comm, Multiset.lcm_cons, Multiset.mem_cons
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
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
cons : ∀ (a : α) (s : Multiset α) (ihs : s.lcm = 0 ↔ 0 ∈ s), (a ::ₘ s).lcm = 0 ↔ 0 ∈ a ::ₘ s
⊢ s.lcm = 0 ↔ 0 ∈ 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]

Premises used: Multiset.lcm_eq_zero_iff, Multiset.notMem_zero, Multiset.cons, Multiset.lcm_zero, Multiset.lcm_cons, Multiset.mem_cons, one_ne_zero
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Nontrivial α
s : Multiset α
⊢ s.lcm ≠ 0 ↔ ¬0 ∈ s

Tactic:
not_congr (lcm_eq_zero_iff s)

Premises used: Multiset.lcm_eq_zero_iff, not_congr
-- Module: Mathlib.Algebra.GCDMonoid.Multiset
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : DecidableEq α
s : Multiset α
⊢ Eq.{u_1 + 1} (α := α) (lcm (dedup 0)) (lcm 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.lcm = s.lcm
pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
neg : ∀ (h : ¬a ∈ s), (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

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.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

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.lcm = s.lcm
h : a ∈ s
pos : s.lcm = @GCDMonoid.lcm _ inst _ a s.lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
simp only [h, dedup_cons_of_mem, IH, lcm_cons]

Premises used: Multiset.lcm_cons, Multiset.dedup_cons_of_mem
-- 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.lcm = s.lcm
h : a ∈ s
pos : fold (@GCDMonoid.lcm _ inst _) 1 s = @GCDMonoid.lcm _ inst _ a (fold (@GCDMonoid.lcm _ inst _) 1 s)
⊢ s.lcm = @GCDMonoid.lcm _ inst _ a s.lcm

Tactic:
unfold lcm

Premises used: Multiset.lcm
-- 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.lcm = s.lcm
h : a ∈ s
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))
⊢ fold (@GCDMonoid.lcm _ inst _) 1 s = @GCDMonoid.lcm _ inst _ a (fold (@GCDMonoid.lcm _ inst _) 1 s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]

Premises used: Multiset.fold_cons_left, lcm_same, Multiset.cons_erase, lcm_assoc
-- 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.lcm = s.lcm
h : a ∈ s
⊢ @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:
apply lcm_eq_of_associated_left (associated_normalize _)

Premises used: lcm_eq_of_associated_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₂).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₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp