case mp
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ Summable f →
    (∀ (x : α), Summable fun y => f { fst := x, snd := y }) ∧ Summable fun x => ∑' (y : β x), f { fst := x, snd := y }

case mpr
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ ((∀ (x : α), Summable fun y => f { fst := x, snd := y }) ∧ Summable fun x => ∑' (y : β x), f { fst := x, snd := y }) →
    Summable f
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ Summable f ↔
    (∀ (x : α), Summable fun y => f { fst := x, snd := y }) ∧ Summable fun x => ∑' (y : β x), f { fst := x, snd := y }
constructor
case mp
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun a => ↑(f a)) →
    (∀ (x : α), Summable fun a => ↑(f { fst := x, snd := a })) ∧
      Summable fun a => ∑' (a_1 : β a), ↑(f { fst := a, snd := a_1 })
case mp
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ Summable f →
    (∀ (x : α), Summable fun y => f { fst := x, snd := y }) ∧ Summable fun x => ∑' (y : β x), f { fst := x, snd := y }
simp only [← NNReal.summable_coe, NNReal.coe_tsum]
no goals
case mp
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun a => ↑(f a)) →
    (∀ (x : α), Summable fun a => ↑(f { fst := x, snd := a })) ∧
      Summable fun a => ∑' (a_1 : β a), ↑(f { fst := a, snd := a_1 })
exact fun h => ⟨h.sigma_factor, h.sigma⟩
case mpr.intro
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y => f { fst := x, snd := y }
h₂ : Summable fun x => ∑' (y : β x), f { fst := x, snd := y }
⊢ Summable f
case mpr
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
⊢ ((∀ (x : α), Summable fun y => f { fst := x, snd := y }) ∧ Summable fun x => ∑' (y : β x), f { fst := x, snd := y }) →
    Summable f
rintro ⟨h₁, h₂⟩
no goals
case mpr.intro
α : Type u_2
β✝ : Type ?u.316734
γ : Type ?u.316737
β : α → Type u_1
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y => f { fst := x, snd := y }
h₂ : Summable fun x => ∑' (y : β x), f { fst := x, snd := y }
⊢ Summable f
simpa only [← ENNReal.tsum_coe_ne_top_iff_summable, ENNReal.tsum_sigma',
  ENNReal.coe_tsum (h₁ _)] using h₂