awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
a b : α
⊢ emultiplicity.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = emultiplicity a b

Tactic:
simp [emultiplicity_eq_emultiplicity_iff, ← map_pow, map_dvd_iff]

Premises used: emultiplicity_eq_emultiplicity_iff, map_dvd_iff, map_pow
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
a b : α
⊢ multiplicity.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = multiplicity a b

Tactic:
multiplicity_eq_of_emultiplicity_eq (emultiplicity_map_eq f)

Premises used: multiplicity_eq_of_emultiplicity_eq, emultiplicity_map_eq
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b c : α
h : b ∣ c
⊢ emultiplicity a b ≤ emultiplicity a c

Tactic:
emultiplicity_le_emultiplicity_iff.2 fun _ hb => hb.trans h

Premises used: Iff.mpr, emultiplicity_le_emultiplicity_iff, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b c : α
h : Associated b c
⊢ emultiplicity a b = emultiplicity a c

Tactic:
le_antisymm (emultiplicity_le_emultiplicity_of_dvd_right h.dvd)
    (emultiplicity_le_emultiplicity_of_dvd_right h.symm.dvd)

Premises used: Associated.dvd, emultiplicity_le_emultiplicity_of_dvd_right, Associated.symm, le_antisymm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b c : α
h : Associated b c
⊢ multiplicity a b = multiplicity a c

Tactic:
multiplicity_eq_of_emultiplicity_eq (emultiplicity_eq_of_associated_right h)

Premises used: emultiplicity_eq_of_associated_right, multiplicity_eq_of_emultiplicity_eq
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : 0 < emultiplicity a b
⊢ a ∣ b

Tactic:
pow_one a ▸ pow_dvd_of_le_emultiplicity (Order.add_one_le_of_lt h)

Premises used: Eq.rec, pow_dvd_of_le_emultiplicity, pow_one, Order.add_one_le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : 0 < multiplicity a b
⊢ a ∣ b

Tactic:
dvd_of_emultiplicity_pos (lt_emultiplicity_of_lt_multiplicity h)

Premises used: lt_emultiplicity_of_lt_multiplicity, dvd_of_emultiplicity_pos
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdvd : a ∣ b
⊢ multiplicity a b ≠ 0

Tactic:
simpa [multiplicity_eq_zero]

Premises used: multiplicity_eq_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ 0 < emultiplicity a b ↔ a ∣ b

Tactic:
emultiplicity_pos_iff.trans dvd_iff_multiplicity_pos

Premises used: Iff.trans, dvd_iff_multiplicity_pos, emultiplicity_pos_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
rw : (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0
⊢ FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

Tactic:
rw [← not_iff_not, FiniteMultiplicity.not_iff_forall, not_and_or, not_ne_iff, not_lt,
    Nat.le_zero]

Premises used: not_iff_not, Nat.le_zero, not_ne_iff, not_lt, FiniteMultiplicity.not_iff_forall, not_and_or
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ ∀ (n : ℕ), HPow.hPow (α := ℕ) 0 n ∣ b

Tactic:
rw [ha] at h
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
h₁ : ∀ (n : ℕ), HPow.hPow (α := ℕ) 0 n ∣ b
⊢ ¬b = 0

Tactic:
rw [ha] at h
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
h₁ : ∀ (n : ℕ), HPow.hPow (α := ℕ) 0 n ∣ b
hb₁ : ¬b = 0
⊢ a = 0

Tactic:
rw [ha] at h
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : ∀ (n : ℕ), HPow.hPow (α := ℕ) 0 n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : ∀ (n : ℕ), HPow.hPow (α := ℕ) 0 n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
exact h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b_1 : ℕ
hb : ¬b_1 = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b_1
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
h_1 : b + 2 ≤ 1
⊢ False

Tactic:
lia
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : a = 1 ∨ b = 0
inl : a = 1 → ∀ (n : ℕ), a ^ n ∣ b
inr : b = 0 → ∀ (n : ℕ), a ^ n ∣ b
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
cases h
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : a = 1
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h : b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0

Tactic:
exact
    ⟨fun h =>
      or_iff_not_imp_right.2 fun hb =>
        have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
        Classical.by_contradiction fun ha1 : a ≠ 1 =>
          have ha_gt_one : 1 < a :=
            lt_of_not_ge fun _ =>
              match a with
              | 0 => ha rfl
              | 1 => ha1 rfl
              | b+2 => by lia
          not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (b.lt_pow_self ha_gt_one),
      fun h => by cases h <;> simp [*]⟩
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ emultiplicity a b = 0

Tactic:
emultiplicity_eq_zero.mpr fun h ↦ ha (isUnit_of_dvd_unit h hb)

Premises used: Iff.mpr, isUnit_of_dvd_unit, emultiplicity_eq_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ multiplicity a b = 0

Tactic:
multiplicity_eq_zero.mpr fun h ↦ ha (isUnit_of_dvd_unit h hb)

Premises used: Iff.mpr, multiplicity_eq_zero, isUnit_of_dvd_unit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a : α
ha : ¬IsUnit a
⊢ emultiplicity a 1 = 0

Tactic:
emultiplicity_of_isUnit_right ha isUnit_one

Premises used: emultiplicity_of_isUnit_right, isUnit_one
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a : α
ha : ¬IsUnit a
⊢ multiplicity a 1 = 0

Tactic:
multiplicity_of_isUnit_right ha isUnit_one

Premises used: isUnit_one, multiplicity_of_isUnit_right
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a : α
ha : ¬IsUnit a
u : αˣ
⊢ emultiplicity a (↑u : α) = 0

Tactic:
emultiplicity_of_isUnit_right ha u.isUnit

Premises used: emultiplicity_of_isUnit_right, Units.isUnit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a : α
ha : ¬IsUnit a
u : αˣ
⊢ multiplicity a (↑u : α) = 0

Tactic:
multiplicity_of_isUnit_right ha u.isUnit

Premises used: Units.isUnit, multiplicity_of_isUnit_right
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a b c : α
hdvd : a ∣ b
⊢ emultiplicity b c ≤ emultiplicity a c

Tactic:
emultiplicity_le_emultiplicity_iff.2 fun n h => (pow_dvd_pow_of_dvd hdvd n).trans h

Premises used: Iff.mpr, pow_dvd_pow_of_dvd, emultiplicity_le_emultiplicity_iff, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a b c : α
h : Associated a b
⊢ emultiplicity b c = emultiplicity a c

Tactic:
le_antisymm (emultiplicity_le_emultiplicity_of_dvd_left h.dvd)
    (emultiplicity_le_emultiplicity_of_dvd_left h.symm.dvd)

Premises used: emultiplicity_le_emultiplicity_of_dvd_left, Associated.dvd, Associated.symm, le_antisymm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a b c : α
h : Associated a b
⊢ multiplicity b c = multiplicity a c

Tactic:
multiplicity_eq_of_emultiplicity_eq (emultiplicity_eq_of_associated_left h)

Premises used: multiplicity_eq_of_emultiplicity_eq, emultiplicity_eq_of_associated_left
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
⊢ emultiplicity (α := Associates α) (Associates.mk a) (Associates.mk b) = emultiplicity a b

Tactic:
simp [emultiplicity_eq_emultiplicity_iff, ← Associates.mk_pow, Associates.mk_dvd_mk]

Premises used: emultiplicity_eq_emultiplicity_iff, Associates.mk_pow, Associates.mk_dvd_mk
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : MonoidWithZero α
a b : α
h : FiniteMultiplicity a b
n : ℕ
hn : ¬a ^ (n + 1) ∣ b
hb : b = 0
⊢ False

Tactic:
simp [hb] at hn
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : MonoidWithZero α
a : α
⊢ emultiplicity a 0 = ⊤

Tactic:
emultiplicity_eq_top.2 (fun v ↦ v.ne_zero rfl)

Premises used: Iff.mpr, FiniteMultiplicity.ne_zero, emultiplicity_eq_top, rfl
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : MonoidWithZero α
a : α
ha : a ≠ 0
⊢ emultiplicity 0 a = 0

Tactic:
emultiplicity_eq_zero.2 <| mt zero_dvd_iff.1 ha

Premises used: Iff.mpr, zero_dvd_iff, mt, emultiplicity_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : MonoidWithZero α
a : α
ha : a ≠ 0
⊢ multiplicity 0 a = 0

Tactic:
multiplicity_eq_zero.2 <| mt zero_dvd_iff.1 ha

Premises used: Iff.mpr, multiplicity_eq_zero, zero_dvd_iff, mt, Iff.mp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
by_contra! : ∀ (nh : (∀ (n : ℕ), p ^ (n + 1) ∣ a) ∧ ∀ (n : ℕ), p ^ (n + 1) ∣ b), False
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
by_contra! nh
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
nh : (∀ (n : ℕ), p ^ (n + 1) ∣ a) ∧ ∀ (n : ℕ), p ^ (n + 1) ∣ b
obtain : ∀ (c : ℕ) (hc : ¬p ^ (c + 1) ∣ a + b), False
⊢ False

Tactic:
obtain ⟨c, hc⟩ := hf
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
nh : (∀ (n : ℕ), p ^ (n + 1) ∣ a) ∧ ∀ (n : ℕ), p ^ (n + 1) ∣ b
c : ℕ
hc : ¬p ^ (c + 1) ∣ a + b
⊢ False

Tactic:
simp_all [dvd_add]

Premises used: dvd_add
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
top : ∀ (hm : min (emultiplicity p a) (emultiplicity p b) = ⊤), ⊤ ≤ emultiplicity p (a + b)
coe :
  ∀ (a_1 : ℕ) (hm : min (emultiplicity p a) (emultiplicity p b) = (↑a_1 : ℕ∞)), (↑a_1 : ℕ∞) ≤ emultiplicity p (a + b)
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Tactic:
cases hm : min (emultiplicity p a) (emultiplicity p b)

Premises used: Min.min, emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
top : ∀ (hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b), ¬FiniteMultiplicity p (a + b)
⊢ ⊤ ≤ emultiplicity p (a + b)

Tactic:
simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢

Premises used: emultiplicity_eq_top, top_le_iff, min_eq_top
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
top : ∀ (hm : FiniteMultiplicity p (a + b)), ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)
⊢ ¬FiniteMultiplicity p (a + b)

Tactic:
contrapose hm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
top : FiniteMultiplicity p a ∨ FiniteMultiplicity p b
⊢ ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)

Tactic:
simp only [not_and_or, not_not] at hm ⊢

Premises used: Classical.not_not, not_and_or
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
hm.or_of_add

Premises used: FiniteMultiplicity.or_of_add
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
exact hm.or_of_add

Premises used: FiniteMultiplicity.or_of_add
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
a_1 : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = (↑a_1 : ℕ∞)
coe : p ^ a_1 ∣ a + b
⊢ (↑a_1 : ℕ∞) ≤ emultiplicity p (a + b)

Tactic:
apply le_emultiplicity_of_pow_dvd

Premises used: le_emultiplicity_of_pow_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Semiring α
p a b : α
a_1 : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = (↑a_1 : ℕ∞)
⊢ p ^ a_1 ∣ a + b

Tactic:
simp [dvd_add, pow_dvd_of_le_emultiplicity, ← hm]

Premises used: pow_dvd_of_le_emultiplicity, dvd_add
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
a b : α
a₁ : ∀ (x : ℕ), a ^ (x + 1) ∣ -b ↔ a ^ (x + 1) ∣ b
⊢ (∃ (n : ℕ), ¬a ^ (n + 1) ∣ -b) ↔ ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b

Tactic:
congr! 3
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
a b : α
x : ℕ
⊢ a ^ (x + 1) ∣ -b ↔ a ^ (x + 1) ∣ b

Tactic:
simp only [dvd_neg]

Premises used: dvd_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
a b : α
rw : ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b
⊢ emultiplicity a (-b) = emultiplicity a b

Tactic:
rw [emultiplicity_eq_emultiplicity_iff]

Premises used: emultiplicity_eq_emultiplicity_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ multiplicity a (-b) = multiplicity a b

Tactic:
multiplicity_eq_of_emultiplicity_eq (emultiplicity_neg a b)

Premises used: multiplicity_eq_of_emultiplicity_eq, emultiplicity_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
inl : ∀ (h : b = (↑b.natAbs : ℤ)), emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
inr : ∀ (h : b = -(↑b.natAbs : ℤ)), emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b

Tactic:
rcases Int.natAbs_eq b with h | h

Premises used: Int.natAbs_eq
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
h : b = (↑b.natAbs : ℤ)
rw : emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
| emultiplicity (↑a : ℤ) b

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
h : b = (↑b.natAbs : ℤ)
inl : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b

Tactic:
conv_rhs => rw [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
rw : emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))
| emultiplicity (↑a : ℤ) b

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
inr : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b

Tactic:
conv_rhs => rw [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
h : b = (↑b.natAbs : ℤ)
inl inl₁ : emultiplicity a b.natAbs = emultiplicity a b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)

Tactic:
rw [Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
inr : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
inr₁ inr₂ : emultiplicity a b.natAbs = emultiplicity a b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))

Tactic:
rw [emultiplicity_neg, Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity, emultiplicity_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a : ℕ
b : ℤ
⊢ multiplicity a b.natAbs = multiplicity (↑a : ℤ) b

Tactic:
multiplicity_eq_of_emultiplicity_eq (Int.emultiplicity_natAbs a b)

Premises used: multiplicity_eq_of_emultiplicity_eq, Int.emultiplicity_natAbs
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ FiniteMultiplicity p b

Tactic:
have : FiniteMultiplicity p b := finiteMultiplicity_iff_emultiplicity_ne_top.2 (by simp [·] at h)
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
this : FiniteMultiplicity p b
rw :
  ∀ (h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a) (this : FiniteMultiplicity p b),
    emultiplicity p (a + b) = (↑(multiplicity p b) : ℕ∞)
⊢ emultiplicity p (a + b) = emultiplicity p b

Tactic:
rw [this.emultiplicity_eq_multiplicity] at *

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hk : p ^ multiplicity p b ∣ a + b
hsucc : ¬p ^ (multiplicity p b + 1) ∣ a + b
⊢ emultiplicity p (a + b) = (↑(multiplicity p b) : ℕ∞)

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

Premises used: emultiplicity_eq_of_dvd_of_not_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hk : p ^ multiplicity p b ∣ a
hk₁ : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p b ∣ a + b

Tactic:
apply dvd_add

Premises used: dvd_add
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hk : (↑(multiplicity p b) : ℕ∞) ≤ emultiplicity p a
⊢ p ^ multiplicity p b ∣ a

Tactic:
apply pow_dvd_of_le_emultiplicity

Premises used: pow_dvd_of_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ (↑(multiplicity p b) : ℕ∞) ≤ emultiplicity p a

Tactic:
h.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ (↑(multiplicity p b) : ℕ∞) ≤ emultiplicity p a

Tactic:
exact h.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ b

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hsucc : ¬p ^ (multiplicity p b + 1) ∣ b
hsucc₁ : p ^ (multiplicity p b + 1) ∣ a
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b

Tactic:
rw [dvd_add_right]

Premises used: dvd_add_right
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hsucc : multiplicity p b < multiplicity p b + 1
⊢ ¬p ^ (multiplicity p b + 1) ∣ b

Tactic:
apply this.not_pow_dvd_of_multiplicity_lt

Premises used: FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p b + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hsucc : (↑(multiplicity p b + 1) : ℕ∞) ≤ emultiplicity p a
⊢ p ^ (multiplicity p b + 1) ∣ a

Tactic:
apply pow_dvd_of_le_emultiplicity

Premises used: pow_dvd_of_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ (↑(multiplicity p b + 1) : ℕ∞) ≤ emultiplicity p a

Tactic:
Order.add_one_le_of_lt h

Premises used: WithTop.map₂, WithTop.some, Order.add_one_le_of_lt, Option.map₂
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ (↑(multiplicity p b + 1) : ℕ∞) ≤ emultiplicity p a

Tactic:
exact Order.add_one_le_of_lt h

Premises used: Order.add_one_le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
hf : FiniteMultiplicity p b
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = multiplicity p b

Tactic:
multiplicity_eq_of_emultiplicity_eq <| emultiplicity_add_of_gt (hf.emultiplicity_eq_multiplicity ▸
      (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity)

Premises used: emultiplicity_add_of_gt, FiniteMultiplicity.emultiplicity_eq_multiplicity, multiplicity_eq_of_emultiplicity_eq, Eq.rec, LT.lt.trans_le, WithTop.coe_strictMono, Eq.symm, multiplicity_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
rw : emultiplicity p (-b) = emultiplicity p b
rw₁ : emultiplicity p (-b) < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b

Tactic:
rw [sub_eq_add_neg, emultiplicity_add_of_gt]

Premises used: emultiplicity_add_of_gt, sub_eq_add_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
rw rw₁ : emultiplicity p b = emultiplicity p b
⊢ emultiplicity p (-b) = emultiplicity p b

Tactic:
rw [emultiplicity_neg]

Premises used: emultiplicity_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h rw : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) < emultiplicity p a

Tactic:
rw [emultiplicity_neg]

Premises used: emultiplicity_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a

Tactic:
assumption
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
rw : multiplicity p (-b) = multiplicity p b
rw₁ : multiplicity p (-b) < multiplicity p a
⊢ multiplicity p (a - b) = multiplicity p b

Tactic:
rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt]

Premises used: sub_eq_add_neg, FiniteMultiplicity.neg, FiniteMultiplicity.multiplicity_add_of_gt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
rw rw₁ : multiplicity p b = multiplicity p b
⊢ multiplicity p (-b) = multiplicity p b

Tactic:
rw [multiplicity_neg]

Premises used: multiplicity_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
rw : multiplicity p b < multiplicity p a
⊢ multiplicity p (-b) < multiplicity p a

Tactic:
rw [multiplicity_neg]

Premises used: multiplicity_neg
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p a

Tactic:
assumption
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
inl :
  ∀ (hab : emultiplicity p a < emultiplicity p b), emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
inr : emultiplicity p a = emultiplicity p b → emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
inr₁ :
  ∀ (hab : emultiplicity p b < emultiplicity p a), emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)

Premises used: lt_trichotomy, emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
inl : emultiplicity p a ≤ emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]

Premises used: emultiplicity_add_of_gt, add_comm, min_eq_left