case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
exact nonarchimedean_aux hle
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
rw [add_comm, max_comm]
no goals
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)
exact this (le_of_not_le hle)