p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
⊢ ↑(↑padicNormE (q + r)) = max ↑(↑padicNormE q) ↑(↑padicNormE r)
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ‖q‖ ≠ ‖r‖
⊢ ‖q + r‖ = max ‖q‖ ‖r‖
dsimp [norm] at h⊢
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
this : ↑padicNormE q ≠ ↑padicNormE r
⊢ ↑(↑padicNormE (q + r)) = max ↑(↑padicNormE q) ↑(↑padicNormE r)
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
⊢ ↑(↑padicNormE (q + r)) = max ↑(↑padicNormE q) ↑(↑padicNormE r)
have : padicNormE q ≠ padicNormE r := by exact_mod_cast h
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
this : ↑padicNormE q ≠ ↑padicNormE r
⊢ ↑(↑padicNormE (q + r)) = max ↑(↑padicNormE q) ↑(↑padicNormE r)
exact_mod_cast add_eq_max_of_ne' this
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
⊢ ↑padicNormE q ≠ ↑padicNormE r
exact_mod_cast h