case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) ≤ multiplicity p b

case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p (a + b)
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = multiplicity p b
apply le_antisymm
case a.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) < multiplicity p b + 1
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) ≤ multiplicity p b
apply PartENat.le_of_lt_add_one
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p (a + b) < multiplicity p b + 1
case a.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) < multiplicity p b + 1
cases' PartENat.ne_top_iff.mp (PartENat.ne_top_of_lt h) with k hk
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p (a + b) < ↑k + 1
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p (a + b) < multiplicity p b + 1
rw [hk]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ ¬p ^ (k + 1) ∣ b

case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ p ^ (k + 1) ∣ a
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p (a + b) < ↑k + 1
rw_mod_cast [multiplicity_lt_iff_neg_dvd, dvd_add_right]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ False

case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ p ^ (k + 1) ∣ a
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ ¬p ^ (k + 1) ∣ b

case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ p ^ (k + 1) ∣ a
intro h_dvd
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ multiplicity p b < ↑(k + 1)
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ False
apply multiplicity.is_greatest _ h_dvd
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ ↑k < ↑(succ k)
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ multiplicity p b < ↑(k + 1)
rw [hk, ←Nat.succ_eq_add_one]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ k < succ k
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ ↑k < ↑(succ k)
norm_cast
no goals
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ k < succ k
apply Nat.lt_succ_self k
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p b + 1 ≤ multiplicity p a
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ p ^ (k + 1) ∣ a
rw [pow_dvd_iff_le_multiplicity, Nat.cast_add, ← hk, Nat.cast_one]
no goals
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p b + 1 ≤ multiplicity p a
exact PartENat.add_one_le_of_lt h
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
this : min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
⊢ multiplicity p b ≤ multiplicity p (a + b)
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p (a + b)
have := @min_le_multiplicity_add α _ _ p a b
no goals
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
this : min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
⊢ multiplicity p b ≤ multiplicity p (a + b)
rwa [← min_eq_right (le_of_lt h)]