-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_countable [MeasurableSingletonClass α] (f : α → E) {s : Set α} (hs : s.Countable)
    (hf : IntegrableOn f s μ) :
    ∫ a in s, f a ∂μ = ∑' a : s, (μ {(a : α)}).toReal • f a

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)

Tactic:
apply hf

Result:
no goals

Proof state:
case hg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

Tactic:
exact Integrable.aestronglyMeasurable hf

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)

Tactic:
rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)

case hg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

case hf
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

case hs
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
⊢ ∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a

Tactic:
have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
⊢ ∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a

Proof state:
case e_f.h
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
a : ↑s
⊢ (μ (Subtype.val '' {a})).toReal • f ↑a = (μ {↑a}).toReal • f ↑a

Tactic:
simp

Result:
no goals

Proof state:
case hs
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s

Tactic:
exact Countable.measurableSet hs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
⊢ ∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a

Tactic:
rw [← integral_subtype_comap hs.measurableSet, integral_countable' hf']

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
⊢ ∑' (a : ↑s), ((Measure.comap Subtype.val μ) {a}).toReal • f ↑a = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
⊢ ∑' (a : ↑s), ((Measure.comap Subtype.val μ) {a}).toReal • f ↑a = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a

Tactic:
congr 1 with a : 1

Result:
case e_f.h
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
a : ↑s
⊢ ((Measure.comap Subtype.val μ) {a}).toReal • f ↑a = (μ {↑a}).toReal • f ↑a

Proof state:
case hf
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

Tactic:
exact Measurable.aemeasurable measurable_subtype_coe

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
a : ↑s
⊢ ((Measure.comap Subtype.val μ) {a}).toReal • f ↑a = (μ {↑a}).toReal • f ↑a

Tactic:
rw [Measure.comap_apply Subtype.val Subtype.coe_injective
  (fun s' hs' => MeasurableSet.subtype_image (Countable.measurableSet hs) hs') _
  (MeasurableSet.singleton a)]

Result:
case e_f.h
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → E
s : Set α
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
a : ↑s
⊢ (μ (Subtype.val '' {a})).toReal • f ↑a = (μ {↑a}).toReal • f ↑a