R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) a ≤ ↑(addVal R) b ↔ a ∣ b
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
⊢ ↑(addVal R) a ≤ ↑(addVal R) b ↔ a ∣ b
have hp := Classical.choose_spec (exists_prime R)
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
⊢ a ∣ b

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : a ∣ b
⊢ ↑(addVal R) a ≤ ↑(addVal R) b
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) a ≤ ↑(addVal R) b ↔ a ∣ b
constructor <;> intro h
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
ha0 : a = 0
⊢ a ∣ b

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
ha0 : ¬a = 0
⊢ a ∣ b
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
⊢ a ∣ b
by_cases ha0 : a = 0
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ a ∣ b
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
ha0 : ¬a = 0
⊢ a ∣ b
obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ∀ (n : ℕ), choose (_ : ∃ ϖ, Prime ϖ) ^ n ∣ a → choose (_ : ∃ ϖ, Prime ϖ) ^ n ∣ b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ a ∣ b
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ a ∣ b
rw [addVal, addValuation_apply, addValuation_apply, multiplicity_le_multiplicity_iff] at h
no goals
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ∀ (n : ℕ), choose (_ : ∃ ϖ, Prime ϖ) ^ n ∣ a → choose (_ : ∃ ϖ, Prime ϖ) ^ n ∣ b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ a ∣ b
exact ha.dvd.trans (h n ha.symm.dvd)
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : b = 0
ha0 : a = 0
⊢ a ∣ b
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : ↑(addVal R) a ≤ ↑(addVal R) b
ha0 : a = 0
⊢ a ∣ b
rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : b = 0
ha0 : a = 0
⊢ a ∣ 0
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : b = 0
ha0 : a = 0
⊢ a ∣ b
rw [h]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : b = 0
ha0 : a = 0
⊢ a ∣ 0
apply dvd_zero
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : a ∣ b
⊢ multiplicity (choose (_ : ∃ ϖ, Prime ϖ)) a ≤ multiplicity (choose (_ : ∃ ϖ, Prime ϖ)) b
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : a ∣ b
⊢ ↑(addVal R) a ≤ ↑(addVal R) b
rw [addVal, addValuation_apply, addValuation_apply]
no goals
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
hp : Prime (choose (_ : ∃ ϖ, Prime ϖ))
h : a ∣ b
⊢ multiplicity (choose (_ : ∃ ϖ, Prime ϖ)) a ≤ multiplicity (choose (_ : ∃ ϖ, Prime ϖ)) b
exact multiplicity_le_multiplicity_of_dvd_right h