case empty
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
f : ι → ℤ
⊢ Int.natAbs (∑ i in ∅, f i) ≤ ∑ i in ∅, Int.natAbs (f i)

case insert
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
f : ι → ℤ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : Int.natAbs (∑ i in s, f i) ≤ ∑ i in s, Int.natAbs (f i)
⊢ Int.natAbs (∑ i in insert i s, f i) ≤ ∑ i in insert i s, Int.natAbs (f i)
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ Int.natAbs (∑ i in s, f i) ≤ ∑ i in s, Int.natAbs (f i)
induction' s using Finset.induction_on with i s his IH
no goals
case empty
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
f : ι → ℤ
⊢ Int.natAbs (∑ i in ∅, f i) ≤ ∑ i in ∅, Int.natAbs (f i)
simp only [Finset.sum_empty, Int.natAbs_zero]
case insert
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
f : ι → ℤ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : Int.natAbs (∑ i in s, f i) ≤ ∑ i in s, Int.natAbs (f i)
⊢ Int.natAbs (f i + ∑ i in s, f i) ≤ Int.natAbs (f i) + ∑ i in s, Int.natAbs (f i)
case insert
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
f : ι → ℤ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : Int.natAbs (∑ i in s, f i) ≤ ∑ i in s, Int.natAbs (f i)
⊢ Int.natAbs (∑ i in insert i s, f i) ≤ ∑ i in insert i s, Int.natAbs (f i)
simp only [his, Finset.sum_insert, not_false_iff]
no goals
case insert
ι✝ : Type ?u.986696
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
ι : Type u_1
f : ι → ℤ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : Int.natAbs (∑ i in s, f i) ≤ ∑ i in s, Int.natAbs (f i)
⊢ Int.natAbs (f i + ∑ i in s, f i) ≤ Int.natAbs (f i) + ∑ i in s, Int.natAbs (f i)
exact (Int.natAbs_add_le _ _).trans (add_le_add le_rfl IH)