-- Mathlib/Probability/IdentDistrib.lean
theorem MemLp.uniformIntegrable_of_identDistrib {ι : Type*} {f : ι → α → E} {j : ι} {p : ℝ≥0∞}
    (hp : 1 ≤ p) (hp' : p ≠ ∞) (hℒp : MemLp (f j) p μ) (hf : ∀ i, IdentDistrib (f i) (f j) μ μ) :
    UniformIntegrable f p μ

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ UniformIntegrable f p μ

Tactic:
have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hfmeas i).2.symm

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
⊢ UniformIntegrable f p μ

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
⊢ UniformIntegrable f p μ

Tactic:
have hfmeas : ∀ i, AEStronglyMeasurable (f i) μ := fun i =>
  (hf i).aestronglyMeasurable_iff.2 hℒp.1

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ UniformIntegrable f p μ

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ UniformIntegrable f p μ

Tactic:
set g : ι → α → E := fun i => (hfmeas i).choose

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
⊢ UniformIntegrable f p μ

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
⊢ UniformIntegrable f p μ

Tactic:
have hgℒp : MemLp (g j) p μ := hℒp.ae_eq (hgeq j).symm

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
hgℒp : MemLp (g j) p μ
⊢ UniformIntegrable f p μ

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
hgℒp : MemLp (g j) p μ
⊢ UniformIntegrable f p μ

Tactic:
exact UniformIntegrable.ae_eq
  (MemLp.uniformIntegrable_of_identDistrib_aux hp hp' hgℒp hgmeas fun i =>
    (IdentDistrib.of_ae_eq (hgmeas i).aemeasurable (hgeq i)).trans
      ((hf i).trans <| IdentDistrib.of_ae_eq (hfmeas j).aemeasurable (hgeq j).symm)) hgeq

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
⊢ UniformIntegrable f p μ

Tactic:
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfmeas i).1

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ UniformIntegrable f p μ