awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
pos :
  ∀ (hι : Nonempty ι),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
neg :
  ∀ (hι : ¬Nonempty ι),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hι : Nonempty ι

Premises used: Nonempty
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : ¬Nonempty ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
⟨0, fun i => False.elim (hι <| Nonempty.intro i)⟩

Premises used: False.elim, Nonempty.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : ¬Nonempty ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
exact ⟨0, fun i => False.elim (hι <| Nonempty.intro i)⟩
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
pos :
  ∀ (C : ℝ) (hC₁ : 0 < C) (hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨C, hC₁, hC₂⟩ := hℒp.eLpNorm_indicator_norm_ge_pos_le (hfmeas _) hε

Premises used: MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_le
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
⟨⟨C, hC₁.le⟩, fun i => le_trans (le_of_eq ?_) hC₂⟩

Premises used: LT.lt.le, Subtype.mk, Exists.intro, le_of_eq, le_trans
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} x ↔
      Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}

Tactic:
ext x
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
h :
  Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖.toNNReal} x ↔
    Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x
⊢ Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} x ↔
    Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x

Tactic:
simp_rw [← norm_toNNReal]

Premises used: norm_toNNReal
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖.toNNReal} x ↔
    Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x

Tactic:
Real.le_toNNReal_iff_coe_le (norm_nonneg _)

Premises used: Real.le_toNNReal_iff_coe_le, Set.Mem, setOf, NNReal.toReal, norm_nonneg
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖.toNNReal} x ↔
    Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x

Tactic:
exact Real.le_toNNReal_iff_coe_le (norm_nonneg _)

Premises used: Real.le_toNNReal_iff_coe_le, norm_nonneg
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}

Tactic:
have : {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖} := by
    ext x
    simp_rw [← norm_toNNReal]
    exact Real.le_toNNReal_iff_coe_le (norm_nonneg _)
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
pos :
  eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ ‖f i x‖} (f i) x‖) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j) x‖) p μ
⊢ eLpNorm (Set.indicator {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} (f i)) p μ =
    eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ

Tactic:
rw [this, ← eLpNorm_norm, ← eLpNorm_norm (Set.indicator _ _)]

Premises used: MeasureTheory.eLpNorm_norm, Set.indicator
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
pos :
  eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ ‖f i x‖} (f i) x‖) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j) x‖) p μ

Tactic:
simp_rw [norm_indicator_eq_indicator_norm, coe_nnnorm]

Premises used: norm_indicator_eq_indicator_norm, coe_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
⊢ Measurable F

Tactic:
apply measurable_norm.indicator (measurableSet_le measurable_const measurable_nnnorm)

Premises used: measurable_norm, measurableSet_le, Measurable.indicator, measurable_const, measurable_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
⊢ Measurable F

Tactic:
have F_meas : Measurable F := by
    apply measurable_norm.indicator (measurableSet_le measurable_const measurable_nnnorm)
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
k : ι
h : ∀ (x : α), Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x = (F ∘ f k) x
⊢ (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k

Tactic:
ext x
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
k : ι
x : α
h h₁ h₂ h₃ : (if C ≤ ‖f k x‖ then ‖f k x‖ else 0) = (F ∘ f k) x
⊢ (if C ≤ ‖f k x‖ then ‖f k x‖ else 0) = (F ∘ f k) x

Tactic:
norm_cast
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
⊢ ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k

Tactic:
have : ∀ k, (fun x ↦ Set.indicator {x | C ≤ ‖f k x‖} (fun a ↦ ‖f k a‖) x) = F ∘ f k := by
    intro k
    ext x
    simp only [Set.indicator, Set.mem_setOf_eq]; norm_cast
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this_1 : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
pos :
  eLpNorm (F ∘ f i) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
pos₁ : eLpNorm (F ∘ f i) p μ = eLpNorm (F ∘ f j) p μ
pos₂ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f i) μ) = eLpNorm (F ∘ f j) p μ
pos₃ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f j) μ) = eLpNorm (F ∘ f j) p μ
pos₄ pos₅ : eLpNorm (F ∘ f j) p μ = eLpNorm (F ∘ f j) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ

Tactic:
rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
    (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]

Premises used: Measurable.aestronglyMeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_fst, MeasureTheory.eLpNorm_map_measure, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : 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) μ μ
⊢ ∀ (i : ι), AEStronglyMeasurable (f i) μ

Tactic:
have hfmeas : ∀ i, AEStronglyMeasurable (f i) μ := fun i =>
    (hf i).aestronglyMeasurable_iff.2 hℒp.1
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : 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 (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
⊢ ∀ (i : ι), StronglyMeasurable (g i)

Tactic:
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfmeas i).1
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : 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 (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ ∀ (i : ι), g i =ᶠ[ae μ] f i

Tactic:
have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hfmeas i).2.symm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : 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 (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
⊢ MemLp (g j) p μ

Tactic:
have hgℒp : MemLp (g j) p μ := hℒp.ae_eq (hgeq j).symm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : 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 (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
hgℒp : MemLp (g j) p μ
⊢ UniformIntegrable f p μ

Tactic:
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

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib_aux, ProbabilityTheory.IdentDistrib.of_ae_eq, MeasureTheory.UniformIntegrable.ae_eq, ProbabilityTheory.IdentDistrib.trans, MeasureTheory.StronglyMeasurable.aemeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : 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 (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
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

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib_aux, ProbabilityTheory.IdentDistrib.of_ae_eq, MeasureTheory.UniformIntegrable.ae_eq, ProbabilityTheory.IdentDistrib.trans, MeasureTheory.StronglyMeasurable.aemeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
rw :
  Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))
hf : AEMeasurable X μ
hg : AEMeasurable Y μ
hf₁ : AEMeasurable X' μ'
hg₁ : AEMeasurable Y' μ'
⊢ X' ⟂ᵢ[μ'] Y'

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]

Premises used: ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map, ProbabilityTheory.IdentDistrib.map_eq, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))

Tactic:
congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq)
      (h_ident.comp measurable_snd).map_eq

Premises used: congrArg, MeasureTheory.Measure.prod, measurable_snd, congr, ProbabilityTheory.IdentDistrib.comp, ProbabilityTheory.IdentDistrib.map_eq, measurable_fst