[GOAL]
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)
[PROOFSTEP]
simp [hq, padicNorm]
[GOAL]
p : ℕ
q : ℚ
hq : q = 0
⊢ 0 ≤ padicNorm p q
[PROOFSTEP]
simp [hq, padicNorm]
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ padicNorm p q
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)
[PROOFSTEP]
split_ifs
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)
[PROOFSTEP]
apply zpow_nonneg
[GOAL]
case ha
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
p : ℕ
⊢ padicNorm p 0 = 0
[PROOFSTEP]
simp [padicNorm]
[GOAL]
p : ℕ
⊢ padicNorm p 1 = 1
[PROOFSTEP]
simp [padicNorm]
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p = (↑p)⁻¹
[PROOFSTEP]
simp [padicNorm, (pos_of_gt hp).ne', padicValNat.self hp]
[GOAL]
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicNorm p ↑q = 1
[PROOFSTEP]
have p : padicValRat p q = 0 := by exact_mod_cast padicValNat_primes neq
[GOAL]
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicValRat p ↑q = 0
[PROOFSTEP]
exact_mod_cast padicValNat_primes neq
[GOAL]
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1
[PROOFSTEP]
rw [padicNorm, p]
[GOAL]
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1
[PROOFSTEP]
simp [q_prime.1.ne_zero]
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p < 1
[PROOFSTEP]
rw [padicNorm_p hp, inv_lt_one_iff]
[GOAL]
p : ℕ
hp : 1 < p
⊢ ↑p ≤ 0 ∨ 1 < ↑p
[PROOFSTEP]
exact_mod_cast Or.inr hp
[GOAL]
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)
[PROOFSTEP]
simp [padicNorm, hq]
[GOAL]
p : ℕ
q : ℚ
hq : q = 0
⊢ padicNorm p (-q) = padicNorm p q
[PROOFSTEP]
simp [hq]
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ padicNorm p (-q) = padicNorm p q
[PROOFSTEP]
simp [padicNorm, hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q ≠ 0
[PROOFSTEP]
rw [padicNorm.eq_zpow_of_nonzero hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0
[PROOFSTEP]
apply zpow_ne_zero_of_ne_zero
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast ne_of_gt hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ q = 0
[PROOFSTEP]
apply by_contradiction
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ ¬q = 0 → False
[PROOFSTEP]
intro hq
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
hq : ¬q = 0
⊢ False
[PROOFSTEP]
unfold padicNorm at h 
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ False
[PROOFSTEP]
rw [if_neg hq] at h 
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ False
[PROOFSTEP]
apply absurd h
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ¬↑p ^ (-padicValRat p q) = 0
[PROOFSTEP]
apply zpow_ne_zero_of_ne_zero
[GOAL]
case a.ha
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
simp [hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
simp [hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ ↑p ≠ 0
[PROOFSTEP]
simp [hp.1.ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
this : ↑p ≠ 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : r = 0
⊢ padicNorm p (q / r) = padicNorm p q / padicNorm p r
[PROOFSTEP]
simp [hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q
[PROOFSTEP]
rw [← padicNorm.mul, div_mul_cancel _ hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z = 0
⊢ padicNorm p ↑z ≤ 1
[PROOFSTEP]
simp [hz, zero_le_one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ padicNorm p ↑z ≤ 1
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ 1
[PROOFSTEP]
rw [if_neg _]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ ↑p ^ (-padicValRat p ↑z) ≤ 1
[PROOFSTEP]
refine' zpow_le_one_of_nonpos _ _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ 1 ≤ ↑p
[PROOFSTEP]
exact_mod_cast le_of_lt hp.1.one_lt
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ -padicValRat p ↑z ≤ 0
[PROOFSTEP]
rw [padicValRat.of_int, neg_nonpos]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ 0 ≤ ↑(padicValInt p z)
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ 0 ≤ padicValInt p z
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ ¬↑z = 0
[PROOFSTEP]
exact_mod_cast hz
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : q = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
simp [hq, max_eq_right hnrp, le_max_right]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
simp [hr, max_eq_left hnqp, le_max_left]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : q + r = 0
⊢ padicNorm p (q + r) ≤ padicNorm p q
[PROOFSTEP]
simpa [hqr] using hnqp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ (if q + r = 0 then 0 else ↑p ^ (-padicValRat p (q + r))) ≤
    max (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) (if r = 0 then 0 else ↑p ^ (-padicValRat p r))
[PROOFSTEP]
split_ifs
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ max (↑p ^ (-padicValRat p q)) (↑p ^ (-padicValRat p r))
[PROOFSTEP]
apply le_max_iff.2
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q) ∨ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p r)
[PROOFSTEP]
left
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q)
[PROOFSTEP]
apply zpow_le_of_le
[GOAL]
case h.ha
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ 1 ≤ ↑p
[PROOFSTEP]
exact_mod_cast le_of_lt hp.1.one_lt
[GOAL]
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q
[PROOFSTEP]
apply neg_le_neg
[GOAL]
case h.h.a
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have : padicValRat p q = min (padicValRat p q) (padicValRat p r) := (min_eq_left h).symm
[GOAL]
case h.h.a
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
rw [this]
[GOAL]
case h.h.a
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
[PROOFSTEP]
exact min_le_padicValRat_add hqr
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r
[GOAL]
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)
[PROOFSTEP]
rw [add_comm, max_comm]
[GOAL]
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)
[PROOFSTEP]
exact this (le_of_not_le hle)
[GOAL]
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)
[PROOFSTEP]
exact nonarchimedean_aux hle
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
rw [sub_eq_add_neg, ← padicNorm.neg r]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))
[PROOFSTEP]
exact padicNorm.nonarchimedean
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
wlog hlt : padicNorm p r < padicNorm p q
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r →
      padicNorm p r < padicNorm p q → padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
rw [add_comm, max_comm]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r →
      padicNorm p r < padicNorm p q → padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (r + q) = max (padicNorm p r) (padicNorm p q)
[PROOFSTEP]
exact this hne.symm (hne.lt_or_lt.resolve_right hlt)
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
have : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r) :=
  calc
    padicNorm p q = padicNorm p (q + r + (-r)) := by ring_nf
    _ ≤ max (padicNorm p (q + r)) (padicNorm p (-r)) := padicNorm.nonarchimedean
    _ = max (padicNorm p (q + r)) (padicNorm p r) := by simp
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p q = padicNorm p (q + r + -r)
[PROOFSTEP]
ring_nf
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ max (padicNorm p (q + r)) (padicNorm p (-r)) = max (padicNorm p (q + r)) (padicNorm p r)
[PROOFSTEP]
simp
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
have hnge : padicNorm p r ≤ padicNorm p (q + r) :=
  by
  apply le_of_not_gt
  intro hgt
  rw [max_eq_right_of_lt hgt] at this 
  exact not_lt_of_ge this hlt
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
⊢ padicNorm p r ≤ padicNorm p (q + r)
[PROOFSTEP]
apply le_of_not_gt
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
⊢ ¬padicNorm p r > padicNorm p (q + r)
[PROOFSTEP]
intro hgt
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False
[PROOFSTEP]
rw [max_eq_right_of_lt hgt] at this 
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p r
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False
[PROOFSTEP]
exact not_lt_of_ge this hlt
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
have : padicNorm p q ≤ padicNorm p (q + r) := by rwa [max_eq_left hnge] at this 
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p q ≤ padicNorm p (q + r)
[PROOFSTEP]
rwa [max_eq_left hnge] at this 
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
apply _root_.le_antisymm
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
apply padicNorm.nonarchimedean
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ max (padicNorm p q) (padicNorm p r) ≤ padicNorm p (q + r)
[PROOFSTEP]
rwa [max_eq_left_of_lt hlt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ℚ
hx : x✝ = 0
⊢ padicNorm p x✝ = 0
[PROOFSTEP]
simp [hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ ↑p ^ (-↑n)
[PROOFSTEP]
split_ifs with hz
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)
[PROOFSTEP]
norm_cast at hz 
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)
[PROOFSTEP]
simp [hz]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)
[PROOFSTEP]
rw [zpow_le_iff_le, neg_le_neg_iff, padicValRat.of_int, padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z))
[PROOFSTEP]
norm_cast
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ n ≤ Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
[PROOFSTEP]
rw [← PartENat.coe_le_coe, PartENat.natCast_get, ← multiplicity.pow_dvd_iff_le_multiplicity, Nat.cast_pow]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0
p : ℕ hp : Fact (Nat.Prime p) n : ℕ z : ℤ hz : ¬↑z = 0 ⊢ z ≠ 0
[PROOFSTEP]
exact_mod_cast hz
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑p ∣ m
[PROOFSTEP]
nth_rw 2 [← pow_one p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑(p ^ 1) ∣ m
[PROOFSTEP]
simp only [dvd_iff_norm_le, Int.cast_ofNat, Nat.cast_one, zpow_neg, zpow_one, not_le]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ (↑p)⁻¹ < padicNorm p ↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 → (↑p)⁻¹ < padicNorm p ↑m
[PROOFSTEP]
intro h
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ (↑p)⁻¹ < padicNorm p ↑m
[PROOFSTEP]
rw [h, inv_lt_one_iff_of_pos]
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < ↑p
[PROOFSTEP]
norm_cast
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < ↑p
[PROOFSTEP]
norm_cast
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p
[PROOFSTEP]
exact Nat.Prime.one_lt Fact.out
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos Fact.out
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ (↑p)⁻¹ < padicNorm p ↑m → padicNorm p ↑m = 1
[PROOFSTEP]
simp only [padicNorm]
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ((↑p)⁻¹ < if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) → (if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) = 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1
[PROOFSTEP]
rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ p < 0 → ↑0 = 1
[PROOFSTEP]
intro h
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
h : p < 0
⊢ ↑0 = 1
[PROOFSTEP]
exact (Nat.not_lt_zero p h).elim
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
have : 1 < (p : ℚ) := by norm_cast; exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ 1 < ↑p
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ 1 < p
[PROOFSTEP]
exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
rw [← zpow_neg_one, zpow_lt_iff_lt this]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
have : 0 ≤ padicValRat p m
[GOAL]
case this
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ 0 ≤ padicValRat p ↑m
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
simp only [of_int, Nat.cast_nonneg]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
intro h
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
rw [← zpow_zero (p : ℚ), zpow_inj]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ -padicValRat p ↑m = 0
[PROOFSTEP]
linarith
[GOAL]
case neg.h₀
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ 0 < ↑p
[PROOFSTEP]
linarith
[GOAL]
case neg.h₁
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ≠ 1
[PROOFSTEP]
linarith
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m < 1 ↔ ↑p ∣ m
[PROOFSTEP]
rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ¬padicNorm p ↑m < 1 ↔ padicNorm p ↑m ≤ 1 ∧ ¬padicNorm p ↑m < 1
[PROOFSTEP]
simp only [padicNorm.of_int, true_and_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ ¬p ∣ m
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← int_eq_one_iff, Int.cast_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ p ∣ m
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← int_lt_one_iff, Int.cast_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
classical
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
rintro a S haS IH - ht
by_cases hs : S.Nonempty
· rw [Finset.sum_insert haS]
  exact
    lt_of_le_of_lt padicNorm.nonarchimedean
      (max_lt (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
· simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty ∅ → (∀ (i : α), i ∈ ∅ → padicNorm p (F i) < t) → padicNorm p (∑ i in ∅, F i) < t
[PROOFSTEP]
rintro ⟨-, ⟨⟩⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t) →
        Finset.Nonempty (insert a s) →
          (∀ (i : α), i ∈ insert a s → padicNorm p (F i) < t) → padicNorm p (∑ i in insert a s, F i) < t
[PROOFSTEP]
rintro a S haS IH - ht
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
⊢ padicNorm p (∑ i in insert a S, F i) < t
[PROOFSTEP]
by_cases hs : S.Nonempty
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
hs : Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) < t
[PROOFSTEP]
rw [Finset.sum_insert haS]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
hs : Finset.Nonempty S
⊢ padicNorm p (F a + ∑ x in S, F x) < t
[PROOFSTEP]
exact
  lt_of_le_of_lt padicNorm.nonarchimedean
    (max_lt (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
hs : ¬Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) < t
[PROOFSTEP]
simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
classical
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
rintro a S haS IH - ht
by_cases hs : S.Nonempty
· rw [Finset.sum_insert haS]
  exact
    padicNorm.nonarchimedean.trans
      (max_le (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
· simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty ∅ → (∀ (i : α), i ∈ ∅ → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in ∅, F i) ≤ t
[PROOFSTEP]
rintro ⟨-, ⟨⟩⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t) →
        Finset.Nonempty (insert a s) →
          (∀ (i : α), i ∈ insert a s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in insert a s, F i) ≤ t
[PROOFSTEP]
rintro a S haS IH - ht
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i in insert a S, F i) ≤ t
[PROOFSTEP]
by_cases hs : S.Nonempty
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
hs : Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) ≤ t
[PROOFSTEP]
rw [Finset.sum_insert haS]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
hs : Finset.Nonempty S
⊢ padicNorm p (F a + ∑ x in S, F x) ≤ t
[PROOFSTEP]
exact
  padicNorm.nonarchimedean.trans
    (max_le (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
hs : ¬Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) ≤ t
[PROOFSTEP]
simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) < t
ht : 0 < t
⊢ padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
obtain rfl | hs := Finset.eq_empty_or_nonempty s
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ (i : α), i ∈ ∅ → padicNorm p (F i) < t
⊢ padicNorm p (∑ i in ∅, F i) < t
[PROOFSTEP]
simp [ht]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) < t
ht : 0 < t
hs : Finset.Nonempty s
⊢ padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
exact sum_lt hs hF
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t
ht : 0 ≤ t
⊢ padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
obtain rfl | hs := Finset.eq_empty_or_nonempty s
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ (i : α), i ∈ ∅ → padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i in ∅, F i) ≤ t
[PROOFSTEP]
simp [ht]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : Finset.Nonempty s
⊢ padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
exact sum_le hs hF
