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

case inr.inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

case inr.inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | hab | hab)
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
rw [add_comm, multiplicity_add_of_gt hab, min_eq_left]
no goals
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b
exact le_of_lt hab
no goals
case inr.inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
contradiction
case inr.inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a
case inr.inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
rw [multiplicity_add_of_gt hab, min_eq_right]
no goals
case inr.inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a
exact le_of_lt hab