case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
⊢ ‖z‖ = 1
rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ 1 ≤ ‖z‖
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1
refine' le_antisymm (norm_le_one _) _
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1
⊢ 1 ≤ ‖z‖
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ 1 ≤ ‖z‖
have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z)
no goals
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1
⊢ 1 ≤ ‖z‖
rwa [mul_one, ← norm_mul, ← eq, norm_one] at this