Theorem: ENat.indicator_support_le (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
⊢ (support f).indicator 1 i ≤ f i
Tactic:
by_cases hi : i ∈ support f
State after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∈ support f
⊢ (support f).indicator 1 i ≤ f i

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ (support f).indicator 1 i ≤ f i

State before:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ (support f).indicator 1 i ≤ f i
Tactic:
rw [indicator_apply_eq_zero.2 (fun h ↦ (hi h).elim)]
State after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ 0 ≤ f i

State before:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ 0 ≤ f i
Tactic:
apply zero_le
State after:
no goals

State before:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∈ support f
⊢ (support f).indicator 1 i ≤ f i
Tactic:
rwa [indicator_apply_eq_self.2 (fun h ↦ (h hi).elim), Pi.one_apply, ENat.one_le_iff_ne_zero]
State after:
no goals