awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ emultiplicity p a ≤ emultiplicity p b

Tactic:
le_of_lt hab

Premises used: le_of_lt
-- 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
⊢ emultiplicity p a ≤ emultiplicity p b

Tactic:
exact le_of_lt hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h_1 : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
inr : emultiplicity p b ≤ emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
rw [emultiplicity_add_of_gt hab, min_eq_right]

Premises used: emultiplicity_add_of_gt, min_eq_right
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b ≤ emultiplicity p a

Tactic:
le_of_lt hab

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

Tactic:
exact le_of_lt hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
inl : ∀ (hab : multiplicity p a < multiplicity p b), multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
inr : multiplicity p a = multiplicity p b → multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
inr₁ : ∀ (hab : multiplicity p b < multiplicity p a), multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

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

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

Tactic:
rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]

Premises used: add_comm, min_eq_left, FiniteMultiplicity.multiplicity_add_of_gt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b

Tactic:
le_of_lt hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b

Tactic:
exact le_of_lt hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h_1 : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
inr : multiplicity p b ≤ multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
rw [hb.multiplicity_add_of_gt hab, min_eq_right]

Premises used: min_eq_right, FiniteMultiplicity.multiplicity_add_of_gt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a

Tactic:
le_of_lt hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a

Tactic:
exact le_of_lt hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
⊢ a * b = p * (p ^ (n + m) * s)

Tactic:
simp [hs, pow_add, mul_comm, mul_left_comm]

Premises used: pow_add, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : n = 0
⊢ False

Tactic:
simp [hx, hn0] at ha
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
h_2 : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ x = p ^ n * y

Tactic:
rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy

Premises used: Nat.succ_le_of_lt, tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
h_2 : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ n * y
⊢ p * x * p = p ^ (n + 1) * y * p

Tactic:
simp [hy, pow_add, mul_comm, mul_left_comm]

Premises used: pow_add, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this_1 : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
rw : x * b * p = p ^ (n + m) * s * p
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p

Tactic:
rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]

Premises used: Nat.succ_le_of_lt, tsub_add_cancel_of_le, tsub_add_eq_add_tsub
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this_1 : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p

Tactic:
simp_all [mul_comm, mul_left_comm, pow_add]

Premises used: pow_add, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : m = 0
⊢ False

Tactic:
simp [hx, hm0] at hb
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
h_2 : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ x = p ^ m * y

Tactic:
rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy

Premises used: Nat.succ_le_of_lt, tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
h_2 : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ m * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
simp [hy, pow_add, mul_comm, mul_left_comm]

Premises used: pow_add, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
rw : a * x * p = p ^ (n + m) * s * p
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p

Tactic:
rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]

Premises used: Nat.succ_le_of_lt, add_assoc, tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p

Tactic:
simp_all [mul_comm, mul_left_comm, pow_add]

Premises used: pow_add, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
⊢ FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a * b)

Tactic:
fun ⟨n, hn⟩ ⟨m, hm⟩ => ⟨n + m, finiteMultiplicity_mul_aux hp hn hm⟩

Premises used: HMul.hMul, _private.0.Prime.finiteMultiplicity_mul.match_1, HAdd.hAdd, finiteMultiplicity_mul_aux, FiniteMultiplicity, Exists.intro
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
⊢ FiniteMultiplicity p (a * b) ↔ FiniteMultiplicity p a ∧ FiniteMultiplicity p b

Tactic:
⟨fun h => ⟨h.mul_left, h.mul_right⟩, fun h =>
    hp.finiteMultiplicity_mul h.1 h.2⟩

Premises used: Prime.finiteMultiplicity_mul, And.right, And.left, And.intro, Iff.intro, FiniteMultiplicity.mul_right, FiniteMultiplicity.mul_left
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k : ℕ
h : FiniteMultiplicity p a
⊢ ¬p ^ HAdd.hAdd (α := ℕ) 0 1 ∣ HPow.hPow (β := ℕ) a 0

Tactic:
simp [mt isUnit_iff_dvd_one.2 hp.2.1]

Premises used: Iff.mpr, mt, And.right, And.left, isUnit_iff_dvd_one
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k_1 k : ℕ
ha : FiniteMultiplicity p a
rw : FiniteMultiplicity p (a * a ^ k)
⊢ FiniteMultiplicity p (a ^ (k + 1))

Tactic:
rw [_root_.pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k_1 k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)

Tactic:
hp.finiteMultiplicity_mul ha (ha.pow hp)

Premises used: Prime.finiteMultiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k_1 k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)

Tactic:
exact hp.finiteMultiplicity_mul ha (ha.pow hp)

Premises used: Prime.finiteMultiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
pos : ∀ (ha : FiniteMultiplicity a a), multiplicity a a = 1
neg : ∀ (ha : ¬FiniteMultiplicity a a), multiplicity a a = 1
⊢ multiplicity a a = 1

Tactic:
by_cases ha : FiniteMultiplicity a a

Premises used: FiniteMultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
pos : HPow.hPow (β := ℕ) a 1 ∣ a ∧ ¬a ^ HAdd.hAdd (α := ℕ) 1 1 ∣ a
⊢ multiplicity a a = 1

Tactic:
rw [ha.multiplicity_eq_iff]

Premises used: FiniteMultiplicity.multiplicity_eq_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
pos : ¬HPow.hPow (β := ℕ) a 2 ∣ a
⊢ HPow.hPow (β := ℕ) a 1 ∣ a ∧ ¬a ^ HAdd.hAdd (α := ℕ) 1 1 ∣ a

Tactic:
simp only [pow_one, dvd_refl, reduceAdd, true_and]

Premises used: Nat.reduceAdd, pow_one, dvd_refl, true_and
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a = HPow.hPow (β := ℕ) a 2 * v
⊢ a * 1 = HPow.hPow (β := ℕ) a 2 * v

Tactic:
nth_rw 1 [← mul_one a] at hv

Premises used: mul_one
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = HPow.hPow (β := ℕ) a 2 * v
⊢ 1 = a * v ∨ a = 0

Tactic:
simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv

Premises used: mul_assoc, mul_eq_mul_left_iff, sq
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v ∨ a = 0
pos : ∀ (hv : 1 = a * v), False
pos₁ : ∀ (ha : FiniteMultiplicity.{u_1} (α := α) 0 0), False
⊢ False

Tactic:
obtain hv | rfl := hv

Premises used: rfl
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ IsUnit a

Tactic:
have : IsUnit a := .of_mul_eq_one v hv.symm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
this : IsUnit a
⊢ False

Tactic:
simpa [this] using ha.not_unit

Premises used: FiniteMultiplicity.not_unit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
v : α
ha : FiniteMultiplicity.{u_1} (α := α) 0 0
⊢ False

Tactic:
simpa using ha.ne_zero

Premises used: FiniteMultiplicity.ne_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
hfin : FiniteMultiplicity a a
⊢ emultiplicity a a = 1

Tactic:
simp [hfin.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ p ^ multiplicity p a ∣ a

Tactic:
have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
⊢ p ^ multiplicity p b ∣ b

Tactic:
have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
rw : p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b

Tactic:
have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by
    rw [pow_add]; gcongr
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
⊢ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Tactic:
have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b :=
    fun h =>
    not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
rw : p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
rw [hfin.multiplicity_eq_iff]

Premises used: FiniteMultiplicity.multiplicity_eq_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Tactic:
⟨hdiv, hsucc⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Tactic:
exact ⟨hdiv, hsucc⟩
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
pos : ∀ (hfin : FiniteMultiplicity p (a * b)), emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
neg : ∀ (hfin : ¬FiniteMultiplicity p (a * b)), emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
by_cases hfin : FiniteMultiplicity p (a * b)

Premises used: HMul.hMul, FiniteMultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
pos : (↑(multiplicity p (a * b)) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(multiplicity p a) : ℕ∞) (↑(multiplicity p b) : ℕ∞)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, FiniteMultiplicity.mul_right, FiniteMultiplicity.mul_left
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
pos : multiplicity p (a * b) = multiplicity p a + multiplicity p b
⊢ (↑(multiplicity p (a * b)) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(multiplicity p a) : ℕ∞) (↑(multiplicity p b) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
multiplicity_mul hp hfin

Premises used: multiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
exact multiplicity_mul hp hfin

Premises used: multiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
neg : ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
rw [emultiplicity_eq_top.2 hfin, eq_comm, WithTop.add_eq_top, emultiplicity_eq_top,
      emultiplicity_eq_top]

Premises used: Iff.mpr, emultiplicity_eq_top, WithTop.add_eq_top, eq_comm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b

Tactic:
simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

Premises used: not_and_or, FiniteMultiplicity.mul_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
empty : emultiplicity p 1 = 0
⊢ emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)

Tactic:
simp only [Finset.sum_empty, Finset.prod_empty]

Premises used: Finset.prod_empty, Finset.sum_empty
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p 1 = 0

Tactic:
emultiplicity_of_one_right hp.not_unit

Premises used: emultiplicity_of_one_right, Prime.not_unit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p 1 = 0

Tactic:
exact emultiplicity_of_one_right hp.not_unit

Premises used: emultiplicity_of_one_right, Prime.not_unit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : a ∉ s
ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)

Tactic:
simpa [has, ← ih] using emultiplicity_mul hp

Premises used: emultiplicity_mul