R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) a = ⊤ ↔ a = 0
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
⊢ ↑(addVal R) a = ⊤ ↔ a = 0
have hi := (Classical.choose_spec (exists_prime R)).irreducible
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) a = ⊤ → a = 0

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ a = 0 → ↑(addVal R) a = ⊤
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) a = ⊤ ↔ a = 0
constructor
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ¬a = 0 → ¬↑(addVal R) a = ⊤
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) a = ⊤ → a = 0
contrapose
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
h : ¬a = 0
⊢ ¬↑(addVal R) a = ⊤
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ¬a = 0 → ¬↑(addVal R) a = ⊤
intro h
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
h : ¬a = 0
n : ℕ
ha : Associated a (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ ¬↑(addVal R) a = ⊤
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
h : ¬a = 0
⊢ ¬↑(addVal R) a = ⊤
obtain ⟨n, ha⟩ := associated_pow_irreducible h hi
case mp.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
n : ℕ
u : Rˣ
h : ¬choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u = 0
ha : Associated (choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u) (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ ¬↑(addVal R) (choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u) = ⊤
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
h : ¬a = 0
n : ℕ
ha : Associated a (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ ¬↑(addVal R) a = ⊤
obtain ⟨u, rfl⟩ := ha.symm
case mp.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
n : ℕ
u : Rˣ
h : ¬choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u = 0
ha : Associated (choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u) (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ ¬↑n = ⊤
case mp.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
n : ℕ
u : Rˣ
h : ¬choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u = 0
ha : Associated (choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u) (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ ¬↑(addVal R) (choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u) = ⊤
rw [mul_comm, addVal_def' u hi n]
no goals
case mp.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
n : ℕ
u : Rˣ
h : ¬choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u = 0
ha : Associated (choose (_ : ∃ ϖ, Prime ϖ) ^ n * ↑u) (choose (_ : ∃ ϖ, Prime ϖ) ^ n)
⊢ ¬↑n = ⊤
exact PartENat.natCast_ne_top _
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) 0 = ⊤
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a : R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ a = 0 → ↑(addVal R) a = ⊤
rintro rfl
no goals
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
hi : Irreducible (choose (_ : ∃ ϖ, Prime ϖ))
⊢ ↑(addVal R) 0 = ⊤
exact addVal_zero