-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
/-- A countable sum of finite measures is s-finite.
This lemma is superseded by the instance below. -/
lemma sfinite_sum_of_countable [Countable ι]
    (m : ι → Measure α) [∀ n, IsFiniteMeasure (m n)] : SFinite (Measure.sum m)

Proof state:
case intro.inr
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure 0

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.inl.intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (Function.extend f m 0 (f i))

Tactic:
rw [hf.extend_apply]

Result:
case intro.inl.intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (m i)

Proof state:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
⊢ SFinite (sum m)

Tactic:
obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι

Result:
case intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
⊢ SFinite (sum m)

Proof state:
case intro.inr
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Tactic:
rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]

Result:
case intro.inr
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure 0

Proof state:
case intro.inl.intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (m i)

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Tactic:
rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn

Result:
case intro.inl.intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (Function.extend f m 0 (f i))

case intro.inr
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Proof state:
case intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
⊢ SFinite (sum m)

Tactic:
refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩

Result:
case intro
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
⊢ IsFiniteMeasure (Function.extend f m 0 n)