-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem sum_measure [PseudoMetrizableSpace β] {m : MeasurableSpace α} {μ : ι → Measure α}
    (h : ∀ i, AEStronglyMeasurable f (μ i)) : AEStronglyMeasurable f (Measure.sum μ)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
A : ∀ (i : ι), ∃ t, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
choose t t_sep ht using A

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
have A : ∀ i : ι, ∃ t : Set β, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i) := fun i =>
  (aestronglyMeasurable_iff_aemeasurable_separable.1 (h i)).2

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
A : ∀ (i : ι), ∃ t, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
x : α
hx : x ∈ f ⁻¹' t i
⊢ ∃ i, f x ∈ t i

Tactic:
exact ⟨i, hx⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
refine ⟨⋃ i, t i, .iUnion t_sep, ?_⟩

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∀ᵐ (x : α) ∂sum μ, f x ∈ ⋃ i, t i

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∀ᵐ (x : α) ∂sum μ, f x ∈ ⋃ i, t i

Tactic:
simp only [Measure.ae_sum_eq, mem_iUnion, eventually_iSup]

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∀ (b : ι), ∀ᵐ (x : α) ∂μ b, ∃ i, f x ∈ t i

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, ∃ i, f x ∈ t i

Tactic:
filter_upwards [ht i] with x hx

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
x : α
hx : x ∈ f ⁻¹' t i
⊢ ∃ i, f x ∈ t i

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (sum μ)

Tactic:
borelize β

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (sum μ)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (sum μ)

Tactic:
refine
  aestronglyMeasurable_iff_aemeasurable_separable.2
    ⟨AEMeasurable.sum_measure fun i => (h i).aemeasurable, ?_⟩

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∀ (b : ι), ∀ᵐ (x : α) ∂μ b, ∃ i, f x ∈ t i

Tactic:
intro i

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, ∃ i, f x ∈ t i