-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem sum_le {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} :
    s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
hs : S.Nonempty
⊢ padicNorm p (∑ i ∈ insert a S, F i) ≤ t

Tactic:
rw [Finset.sum_insert haS]

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
hs : S.Nonempty
⊢ padicNorm p (F a + ∑ x ∈ S, F x) ≤ t

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
hs : S.Nonempty
⊢ padicNorm p (F a + ∑ x ∈ S, F x) ≤ t

Tactic:
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)))

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
hs : ¬S.Nonempty
⊢ padicNorm p (∑ i ∈ insert a S, F i) ≤ t

Tactic:
simp_all

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∅.Nonempty → (∀ i ∈ ∅, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ ∅, F i) ≤ t

Tactic:
rintro ⟨-, ⟨⟩⟩

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t) →
        (insert a s).Nonempty → (∀ i ∈ insert a s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ insert a s, F i) ≤ t

Tactic:
rintro a S haS IH - ht

Result:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ insert a S, F i) ≤ t

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
refine s.induction_on (by rintro ⟨-, ⟨⟩⟩) ?_

Result:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t) →
        (insert a s).Nonempty → (∀ i ∈ insert a s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ insert a s, F i) ≤ t

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ insert a S, F i) ≤ t

Tactic:
by_cases hs : S.Nonempty

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : a ∉ S
IH : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
hs : S.Nonempty
⊢ padicNorm p (∑ i ∈ 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 : S.Nonempty → (∀ i ∈ S, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ S, F i) ≤ t
ht : ∀ i ∈ insert a S, padicNorm p (F i) ≤ t
hs : ¬S.Nonempty
⊢ padicNorm p (∑ i ∈ insert a S, F i) ≤ t