-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
/-- A function is integrable for the counting measure iff its norm is summable. -/
lemma integrable_count_iff :
    Integrable f Measure.count ↔ Summable (‖f ·‖)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ Integrable f Measure.count ↔ Summable fun x => ‖f x‖

Tactic:
rw [Integrable, hasFiniteIntegral_count_iff, and_iff_right_iff_imp]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ (Summable fun x => ‖f x‖) → AEStronglyMeasurable f Measure.count

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t

Tactic:
refine ⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩

Result:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ TopologicalSpace.IsSeparable (f '' univ)

Proof state:
case refine_2.inr.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
x : α
hg : f x ∈ f '' univ
hg' : f x ≠ 0
⊢ f x ∈ f '' Function.support f ∪ {0}

Tactic:
exact Or.inl ⟨x, hg', rfl⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
g : β
hg : g ∈ f '' univ
⊢ g ∈ f '' Function.support f ∪ {0}

Tactic:
rcases eq_or_ne g 0 with rfl | hg'

Result:
case refine_2.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
hg : 0 ∈ f '' univ
⊢ 0 ∈ f '' Function.support f ∪ {0}

case refine_2.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
g : β
hg : g ∈ f '' univ
hg' : g ≠ 0
⊢ g ∈ f '' Function.support f ∪ {0}

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ f '' univ ⊆ f '' Function.support f ∪ {0}

Tactic:
intro g hg

Result:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
g : β
hg : g ∈ f '' univ
⊢ g ∈ f '' Function.support f ∪ {0}

Proof state:
case refine_2.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
g : β
hg : g ∈ f '' univ
hg' : g ≠ 0
⊢ g ∈ f '' Function.support f ∪ {0}

Tactic:
obtain ⟨x, -, rfl⟩ := (mem_image ..).mp hg

Result:
case refine_2.inr.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
x : α
hg : f x ∈ f '' univ
hg' : f x ≠ 0
⊢ f x ∈ f '' Function.support f ∪ {0}

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ (Summable fun x => ‖f x‖) → AEStronglyMeasurable f Measure.count

Tactic:
intro hs

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
⊢ AEStronglyMeasurable f Measure.count

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ TopologicalSpace.IsSeparable (f '' univ)

Tactic:
suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
  (((hs'.image f).union (countable_singleton 0)).mono this).isSeparable

Result:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ f '' univ ⊆ f '' Function.support f ∪ {0}

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this : MeasurableSpace β := borel β
⊢ AEStronglyMeasurable f Measure.count

Tactic:
haveI : BorelSpace β := ⟨rfl⟩

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEStronglyMeasurable f Measure.count

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
⊢ AEStronglyMeasurable f Measure.count

Tactic:
letI : MeasurableSpace β := borel β

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this : MeasurableSpace β := borel β
⊢ AEStronglyMeasurable f Measure.count

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEMeasurable f Measure.count

Tactic:
refine (measurable_zero.measurable_of_countable_ne ?_).aemeasurable

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ {x | 0 x ≠ f x}.Countable

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
⊢ (Function.support f).Countable

Tactic:
simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
  using hs.countable_support

Result:
no goals