mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
| j₂.posPart.real i

Tactic:
← Set.inter_union_compl i T

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
| j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s A ≤ -↑n

Tactic:
refine le_trans ?_ (le_of_lt (h_lt _))

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s A ≤ s (B n)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ 1 / ↑(measureUnivNNReal μ) ^ (1 / p.toReal) * (μ tᶜ).toReal ^ (1 / p.toReal) ≤ 1

Tactic:
mul_comm,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ (μ tᶜ).toReal ^ (1 / p.toReal) * (1 / ↑(measureUnivNNReal μ) ^ (1 / p.toReal)) ≤ 1
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = ↑m

Tactic:
SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi,

Goal state after:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ ↑(NNReal.mk (μ.toSignedMeasure (univ ∩ i)) ⋯) = ↑m
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
have :
    (s.singularPart μ).toJordanDecomposition =
      ⟨s.toJordanDecomposition.posPart.singularPart μ,
        s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by
    refine JordanDecomposition.toSignedMeasure_injective ?_
    rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
  rw [totalVariation, this]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ 0 < ↑(measureUnivNNReal μ) ^ (1 / p.toReal)

Tactic:
· exact Real.rpow_pos_of_pos (measureUnivNNReal_pos hμ) _

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm ((starRingEnd (α → K)) f) p μ = lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf ?_]

Goal state after:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ ↑C
⊢ (μ.restrict s) univ ^ p.toReal⁻¹ * ENNReal.ofReal ↑C ≤ ↑C * μ s ^ (1 / p.toReal)

Tactic:
mul_comm,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ ↑C
⊢ ENNReal.ofReal ↑C * (μ.restrict s) univ ^ p.toReal⁻¹ ≤ ↑C * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
⊢ μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂

Tactic:
by
  rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]
  exact FiniteMeasure.apply_union_le _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
⊢ μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂

Tactic:
have := measure_union_le (μ := (μ : Measure Ω)) s₁ s₂

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this : ↑μ (s₁ ∪ s₂) ≤ ↑μ s₁ + ↑μ s₂
⊢ μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ {x | max C 1 ≤ ‖Exists.choose ⋯ x‖₊}.indicator (fun a ↦ ‖Exists.choose ⋯ a‖) x ≤
    {x | C ≤ ‖g i x‖₊}.indicator (fun a ↦ ‖g i a‖) x

Tactic:
← le_max_left

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ {x | C ≤ ‖Exists.choose ⋯ x‖₊}.indicator (fun a ↦ ‖Exists.choose ⋯ a‖) x ≤
    {x | C ≤ ‖g i x‖₊}.indicator (fun a ↦ ‖g i a‖) x
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∈ t
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∉ t
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

Tactic:
· simpa [memt]

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∉ t
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : ↑C * μ {x | ↑C ≤ ↑‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1
⊢ μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ

Tactic:
mul_comm,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | ↑C ≤ ↑‖μ[g | ℱ n] x‖₊} * ↑C ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1
⊢ μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ 1 * eLpNorm g 1 μ

Tactic:
one_mul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ eLpNorm g 1 μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C ≤ ENNReal.ofReal δ

Tactic:
rw [ENNReal.div_le_iff_le_mul (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne),
      hC, NNReal.inv_mk, ENNReal.coe_mul, ENNReal.coe_toNNReal hg.eLpNorm_lt_top.ne, ← mul_assoc, ←
      ENNReal.ofReal_eq_coe_nnreal, ← ENNReal.ofReal_mul hδ.le, mul_inv_cancel₀ hδ.ne',
      ENNReal.ofReal_one, one_mul, ENNReal.rpow_one]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ≤ eLpNorm g 1 μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
this :
  (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) • ↑(δ ^ (1 / p.toReal)) ≤
    eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ False

Tactic:
← ENNReal.coe_smul,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
this :
  ↑((2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) • δ ^ (1 / p.toReal)) ≤
    eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ False
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
⊢ iIndepSets (π ∘ g) κ μ

Tactic:
by
  intro s f hf
  let f' := Function.extend g f fun _ => ∅
  have f'_apply x : f' (g x) = f x := hg.extend_apply ..
  classical
  have hf' : ∀ i ∈ s.image g, f' i ∈ π i := by
    simp_rw [Finset.forall_mem_image, f'_apply]
    exact hf
  filter_upwards [@h (s.image g) f' hf'] with a ha
  simpa [Finset.set_biInter_finset_image, Finset.prod_image hg.injOn, f'_apply] using ha

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
⊢ Indep m' ⊥ κ μ

Tactic:
by
  intro s t _ ht
  rw [Set.mem_ofPred_eq, MeasurableSpace.measurableSet_bot_iff] at ht
  rcases eq_zero_or_isMarkovKernel κ with rfl | h
  · simp
  refine Filter.Eventually.of_forall (fun a ↦ ?_)
  rcases ht with ht | ht
  · rw [ht, Set.inter_empty, measure_empty, mul_zero]
  · rw [ht, Set.inter_univ, measure_univ, mul_one]

Goal state after: