internlm/Lean-Github huggingface dataset:
Theorem: ENat.tendsto_mul
Proof state before:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ↑b, 0 < y
Tactic:
rw [nhds_cast_eq, principal_singleton, eventually_pure, Nat.cast_pos,
  ← Nat.ne_zero_iff_zero_lt]
Proof state after:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ b ≠ 0
Theorem: ENat.tendsto_mul
Proof state before:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ b ≠ 0
Tactic:
simpa using hb
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
case inl
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ⊤, 0 < y
Tactic:
apply lt_mem_nhds (by simp)
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ 0 < ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.Tendsto.const_mul
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f : Filter α
m : α → ℕ∞
a b : ℕ∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ 0 ∨ a ≠ ⊤
this : a = 0
⊢ Tendsto (fun b => a * m b) f (𝓝 (a * b))
Tactic:
simp [this, tendsto_const_nhds]
Proof state after:
no goals
Theorem: ENat.iSup_zero_eq_zero
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
⊢ ⨆ x, 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.mul_iSup
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Tactic:
by_cases hf : ∀ i, f i = 0
Proof state after:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i

case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Theorem: ENat.mul_iSup
Proof state before:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Tactic:
refine' (monotone_id.const_mul' _).map_iSup_of_continuousAt _ (mul_zero c)
Proof state after:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => c * id x) (⨆ i, f i)
Theorem: ENat.mul_iSup
Proof state before:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => c * id x) (⨆ i, f i)
Tactic:
refine' ENat.Tendsto.const_mul tendsto_id (Or.inl _)
Proof state after:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ i, f i) ≠ 0
Theorem: ENat.mul_iSup
Proof state before:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ i, f i) ≠ 0
Tactic:
exact mt ENat.iSup_eq_zero.1 hf
Proof state after:
no goals
Theorem: ENat.mul_iSup
Proof state before:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Tactic:
obtain rfl : f = fun _ ↦ 0
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ f = fun x => 0

case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i
Theorem: ENat.mul_iSup
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ f = fun x => 0

case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i
Tactic:
exact funext hf
Proof state after:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i
Theorem: ENat.mul_iSup
Proof state before:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i
Tactic:
simp only [mul_zero, ENat.iSup_zero_eq_zero]
Proof state after:
no goals
Theorem: ENat.iSup_mul
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Tactic:
simp_rw [mul_comm, ENat.mul_iSup]
Proof state after:
no goals
Theorem: ENat.tsum_le_of_subset
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s t : Set α
h : s ⊆ t
⊢ ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x
Tactic:
rw [← diff_union_of_subset h, ENat.tsum_union_disjoint disjoint_sdiff_left]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s t : Set α
h : s ⊆ t
⊢ ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑(t \ s)), f ↑x + ∑' (x : ↑s), f ↑x
Theorem: ENat.tsum_le_of_subset
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s t : Set α
h : s ⊆ t
⊢ ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑(t \ s)), f ↑x + ∑' (x : ↑s), f ↑x
Tactic:
exact le_add_self
Proof state after:
no goals
Theorem: ENat.tsum_le_union
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s t : Set α
⊢ ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
Tactic:
rw [← diff_union_self, ENat.tsum_union_disjoint disjoint_sdiff_left]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s t : Set α
⊢ ∑' (x : ↑(s \ t)), f ↑x + ∑' (x : ↑t), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
Theorem: ENat.tsum_le_union
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s t : Set α
⊢ ∑' (x : ↑(s \ t)), f ↑x + ∑' (x : ↑t), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
Tactic:
exact add_le_add_right (ENat.tsum_le_of_subset diff_subset) _
Proof state after:
no goals
Theorem: ENat.tsum_insert
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
a : α
h : a ∉ s
⊢ ∑' (x : ↑(insert a s)), f ↑x = f a + ∑' (x : ↑s), f ↑x
Tactic:
rw [← singleton_union, ENat.tsum_union_disjoint, tsum_singleton]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
a : α
h : a ∉ s
⊢ Disjoint {a} s
Theorem: ENat.tsum_insert
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
a : α
h : a ∉ s
⊢ Disjoint {a} s
Tactic:
rwa [disjoint_singleton_left]
Proof state after:
no goals
Theorem: ENat.tsum_sub
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hfin : ∑' (a : α), g a ≠ ⊤
h : g ≤ f
⊢ ∑' (a : α), (f a - g a) = ∑' (a : α), f a - ∑' (a : α), g a
Tactic:
rw [← WithTop.add_right_cancel_iff hfin, ← ENat.tsum_add,
  tsum_congr (fun i ↦ tsub_add_cancel_of_le (h i)), tsub_add_cancel_of_le (ENat.tsum_le_tsum h)]
Proof state after:
no goals
Theorem: ENat.mul_tsum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : ℕ∞
⊢ c * ∑' (a : α), f a = ∑' (a : α), c * f a
Tactic:
simp_rw [ENat.tsum_eq_iSup_sum, ENat.mul_iSup, Finset.mul_sum]
Proof state after:
no goals
Theorem: ENat.tsum_mul
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : ℕ∞
⊢ (∑' (a : α), f a) * c = ∑' (a : α), f a * c
Tactic:
simp_rw [ENat.tsum_eq_iSup_sum, ENat.iSup_mul, Finset.sum_mul]
Proof state after:
no goals
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
⊢ ∑' (x : ↑s), f ↑x = ⊤ ↔ ∃ a ∈ s, f a = ⊤
Tactic:
refine' ⟨hs.induction_on (by simp) @fun a s' has' _ IH htop ↦ _,
  fun ⟨a, has, ha⟩ ↦ ENat.tsum_eq_top_of_eq_top ⟨⟨a, has⟩, ha⟩⟩
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
obtain (ht | hne) := eq_or_ne (f a) ⊤
Proof state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
ht : f a = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
rw [ENat.tsum_insert has', WithTop.add_eq_top, or_iff_right hne] at htop
Proof state after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
obtain ⟨b, hbs, hbtop⟩ := IH htop
Proof state after:
case inr.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
b : α
hbs : b ∈ s'
hbtop : f b = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
case inr.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑s'), f ↑x = ⊤
hne : f a ≠ ⊤
b : α
hbs : b ∈ s'
hbtop : f b = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
exact ⟨b, Or.inr hbs, hbtop⟩
Proof state after:
no goals
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
⊢ ∑' (x : ↑∅), f ↑x = ⊤ → ∃ a ∈ ∅, f a = ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.Finite.tsum_eq_top_iff
Proof state before:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
ht : f a = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
Tactic:
exact ⟨a, mem_insert _ _, ht⟩
Proof state after:
no goals
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
⊢ ∑' (a : α), f a = ⊤
Tactic:
rw [ENat.tsum_eq_iSup_sum, iSup_eq_top]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
⊢ ∀ b < ⊤, ∃ i, b < ∑ a ∈ i, f a
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
⊢ ∀ b < ⊤, ∃ i, b < ∑ a ∈ i, f a
Tactic:
intro b hb
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ∞
hb : b < ⊤
⊢ ∃ i, b < ∑ a ∈ i, f a
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ∞
hb : b < ⊤
⊢ ∃ i, b < ∑ a ∈ i, f a
Tactic:
lift b to ℕ using hb.ne
Proof state after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
obtain ⟨s, hss, hsc⟩ := exists_subset_encard_eq ((add_one_le_of_lt hb).trans_eq hf.encard_eq.symm)
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑b + 1
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑b + 1
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
rw [← Nat.cast_one, ← Nat.cast_add] at hsc
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
set s' := (finite_of_encard_eq_coe hsc).toFinset
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
Tactic:
refine ⟨s', lt_of_lt_of_le ?_ (Finset.sum_le_sum (show ∀ i ∈ s', 1 ≤ f i from ?_))  ⟩
Proof state after:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ↑b < ∑ i ∈ s', 1

case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s', 1 ≤ f i
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s', 1 ≤ f i
Tactic:
simp only [Finite.mem_toFinset, ENat.one_le_iff_ne_zero, s']
Proof state after:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s, f i ≠ 0
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s, f i ≠ 0
Tactic:
exact hss
Proof state after:
no goals
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ↑b < ∑ i ∈ s', 1
Tactic:
rw [Finset.sum_const, nsmul_eq_mul, mul_one,
  ← (finite_of_encard_eq_coe hsc).encard_eq_coe_toFinset_card, hsc, Nat.cast_lt]
Proof state after:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ b < b + 1
Theorem: ENat.tsum_eq_top_of_support_infinite
Proof state before:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ b < b + 1
Tactic:
exact Nat.lt.base b
Proof state after:
no goals
Theorem: ENat.tsum_const_eq_top_of_ne_zero
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
inst✝ : Infinite ι
c : ℕ∞
hc : c ≠ 0
⊢ (support fun x => c).Infinite
Tactic:
rwa [support_const hc, infinite_univ_iff]
Proof state after:
no goals
Theorem: ENat.tsum_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
⊢ ∑' (a : α), f a = ⊤ ↔ (support f).Infinite ∨ ∃ a, f a = ⊤
Tactic:
refine' ⟨fun h ↦ _, _⟩
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∑' (a : α), f a = ⊤
⊢ (support f).Infinite ∨ ∃ a, f a = ⊤

case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
⊢ ((support f).Infinite ∨ ∃ a, f a = ⊤) → ∑' (a : α), f a = ⊤
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
⊢ ((support f).Infinite ∨ ∃ a, f a = ⊤) → ∑' (a : α), f a = ⊤
Tactic:
rintro (h | h)
Proof state after:
case refine'_2.inl
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : (support f).Infinite
⊢ ∑' (a : α), f a = ⊤

case refine'_2.inr
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∃ a, f a = ⊤
⊢ ∑' (a : α), f a = ⊤
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_2.inr
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∃ a, f a = ⊤
⊢ ∑' (a : α), f a = ⊤
Tactic:
exact ENat.tsum_eq_top_of_eq_top h
Proof state after:
no goals
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∑' (a : α), f a = ⊤
⊢ (support f).Infinite ∨ ∃ a, f a = ⊤
Tactic:
rw [or_iff_not_imp_left, not_infinite]
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∑' (a : α), f a = ⊤
⊢ (support f).Finite → ∃ a, f a = ⊤
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∑' (a : α), f a = ⊤
⊢ (support f).Finite → ∃ a, f a = ⊤
Tactic:
intro hfin
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∑' (a : α), f a = ⊤
hfin : (support f).Finite
⊢ ∃ a, f a = ⊤
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∑' (a : α), f a = ⊤
hfin : (support f).Finite
⊢ ∃ a, f a = ⊤
Tactic:
rw [← tsum_support_eq, Finite.tsum_eq_top_iff hfin] at h
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∃ a ∈ support f, f a = ⊤
hfin : (support f).Finite
⊢ ∃ a, f a = ⊤
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : ∃ a ∈ support f, f a = ⊤
hfin : (support f).Finite
⊢ ∃ a, f a = ⊤
Tactic:
obtain ⟨a, -, h⟩ := h
Proof state after:
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hfin : (support f).Finite
a : α
h : f a = ⊤
⊢ ∃ a, f a = ⊤
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hfin : (support f).Finite
a : α
h : f a = ⊤
⊢ ∃ a, f a = ⊤
Tactic:
exact ⟨a, h⟩
Proof state after:
no goals
Theorem: ENat.tsum_eq_top_iff
Proof state before:
case refine'_2.inl
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
h : (support f).Infinite
⊢ ∑' (a : α), f a = ⊤
Tactic:
exact ENat.tsum_eq_top_of_support_infinite h
Proof state after:
no goals
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ∑' (a : ↑s), f ↑a = ⊤ ↔ (s ∩ support f).Infinite ∨ ∃ a ∈ s, f a = ⊤
Tactic:
simp_rw [ENat.tsum_eq_top_iff, Subtype.exists, exists_prop]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ((support fun a => f ↑a).Infinite ∨ ∃ a ∈ s, f a = ⊤) ↔ (s ∩ support f).Infinite ∨ ∃ a ∈ s, f a = ⊤
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ((support fun a => f ↑a).Infinite ∨ ∃ a ∈ s, f a = ⊤) ↔ (s ∩ support f).Infinite ∨ ∃ a ∈ s, f a = ⊤
Tactic:
convert Iff.rfl
Proof state after:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ (s ∩ support f).Finite ↔ (support fun a => f ↑a).Finite
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ (s ∩ support f).Finite ↔ (support fun a => f ↑a).Finite
Tactic:
simp_rw [← Set.finite_coe_iff]
Proof state after:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Finite ↑(s ∩ support f) ↔ Finite ↑(support fun a => f ↑a)
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
case h.e'_2.h.e'_1.h.a
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Finite ↑(s ∩ support f) ↔ Finite ↑(support fun a => f ↑a)
Tactic:
exact Bijective.finite_iff (f := fun i ↦ ⟨⟨i,i.2.1⟩, i.2.2⟩)
  ⟨by rintro ⟨i, hi⟩ ⟨j, hj⟩ hij; simpa using hij, by rintro ⟨⟨i,his⟩, hi⟩; use ⟨i, ⟨his, hi⟩⟩⟩
Proof state after:
no goals
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Injective fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩
Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
Proof state after:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
hi : i ∈ s ∩ support f
j : α
hj : j ∈ s ∩ support f
hij : (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨i, hi⟩ = (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
hi : i ∈ s ∩ support f
j : α
hj : j ∈ s ∩ support f
hij : (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨i, hi⟩ = (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ Surjective fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩
Tactic:
rintro ⟨⟨i,his⟩, hi⟩
Proof state after:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
his : i ∈ s
hi : ⟨i, his⟩ ∈ support fun a => f ↑a
⊢ ∃ a, (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) a = ⟨⟨i, his⟩, hi⟩