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
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
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
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
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
rintro a S haS IH - ht
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

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
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
by_cases hs : S.Nonempty
no goals
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
rintro ⟨-, ⟨⟩⟩
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
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
rw [Finset.sum_insert haS]
no goals
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
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)))
no goals
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
simp_all