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

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
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
obtain rfl | hs := Finset.eq_empty_or_nonempty s
no goals
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
simp [ht]
no goals
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
exact sum_lt hs hF