case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
by_cases hx : x = 0
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min (valuation 0) (valuation y) ≤ valuation y
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
rw [hx, zero_add]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min (valuation 0) (valuation y) ≤ valuation y
exact min_le_right _ _
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
by_cases hy : y = 0
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (valuation x) (valuation 0) ≤ valuation x
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
rw [hy, add_zero]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (valuation x) (valuation 0) ≤ valuation x
exact min_le_left _ _
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
have h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := padicNormE.nonarchimedean x y
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
hp_one : 1 < ↑p
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
have hp_one : (1 : ℝ) < p := by
  rw [← Nat.cast_one, Nat.cast_lt]
  exact Nat.Prime.one_lt hp.elim
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
hp_one : 1 < ↑p
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
rwa [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val hxy,
  zpow_le_max_iff_min_le hp_one] at h_norm
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ 1 < p
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ 1 < ↑p
rw [← Nat.cast_one, Nat.cast_lt]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ 1 < p
exact Nat.Prime.one_lt hp.elim