mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case mp
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (F : Set Ω), IsClosed[inst✝³] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
⊢ ∀ (G : Set Ω), IsOpen[inst✝³] G → μ G ≤ liminf (fun i ↦ (μs i) G) L

Tactic:
G

Goal state after:
case mp
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (F : Set Ω), IsClosed[inst✝³] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
G : Set Ω
⊢ IsOpen[inst✝³] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case e'_3.e'_5
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Measure.map X (1 • μ) = Measure.map X μ

Tactic:
one_smul

Goal state after:
case e'_3.e'_5
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Measure.map X μ = Measure.map X μ
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case e'_3.e'_6
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Measure.map Y (1 • ν) = Measure.map Y ν

Tactic:
one_smul

Goal state after:
case e'_3.e'_6
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Measure.map Y ν = Measure.map Y ν
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∈ p1
h2 : n ∈ p2
⊢ (κ a) (f1 n ∩ f2 n) = (κ a) (f1 n) * (κ a) (f2 n)

Tactic:
exact absurd rfl (Set.disjoint_iff_forall_ne.mp hST (hp1 h1) (hp2 h2))

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ (∏ i, μ (Y i ⁻¹' t i))⁻¹ * ∏ i, μ (g i) = ∏ i, (μ (Y i ⁻¹' t i))⁻¹ * μ (g i)

Tactic:
rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case neg
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
x✝ : i ∈ Finset.univ
hi : i ∉ s
⊢ (μ (Y i ⁻¹' t i))⁻¹ * μ (g i) = if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1

Tactic:
· simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top μ _)]

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ →
    ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun x ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
h_ind_g

Goal state after:
case add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
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 α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
hp : IsPiSystem p
h_le' : ∀ (i : ι), generateFrom (π i) ≤ _mΩ
⊢ Indep m_p (m a) η μ

Tactic:
have hm_p : m_p ≤ _mΩ := generateFrom_piiUnionInter_le π h_le' S

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
hp : IsPiSystem p
h_le' : ∀ (i : ι), generateFrom (π i) ≤ _mΩ
hm_p : m_p ≤ _mΩ
⊢ Indep m_p (m a) η μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f' : Measurable f'
⊢ (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ + ∫⁻ (a : Ω), g a * T.indicator (fun x ↦ c) a ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ +
      (∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
h_ind_g

Goal state after:
case add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f' : Measurable f'
⊢ (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ +
      (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ +
      (∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ -
      ((∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ - (1 • ∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ

Tactic:
one_smul

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ -
      ((∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ 0 ≤ 1 / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → Ω'
hX : MeasurePreserving X μ ν
f : Ω' → ℝ
hf : AEMeasurable f ν
⊢ Var[fun ω ↦ f (X ω); μ] = Var[f; ν]

Tactic:
by
  rw [← hX.map_eq, variance_map (hX.map_eq ▸ hf) hX.aemeasurable, Function.comp_def]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
⊢ 0 ≤ b - X ω

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
⊢ 0 ≤ X ω - a

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), (X ^ 2) x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2 ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j

Tactic:
refine (f.mono hij).trans ?_

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f j ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (∏ i, (κ a) (Y i ⁻¹' t i))⁻¹ * ∏ i, (κ a) (g i) = ∏ i, ((κ a) (Y i ⁻¹' t i))⁻¹ * (κ a) (g i)

Tactic:
rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _

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

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
⊢ ∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)

Tactic:
obtain ⟨x, hxN, hx⟩ := exists_notMem_null_laverage_le hμ
    (ne_top_of_le_ne_top (by finiteness) this) hN₀

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun x ↦ f x a) atTop ∂μ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
⊢ ∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: case refine_1
α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst✝ : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ ∀ (x : α), ‖f x‖ₑ ≤ ‖Finset.univ.sup fun x ↦ ‖f x‖ₑ‖ₑ

pp: case refine_2
α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst✝ : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ eLpNorm (fun x ↦ Finset.univ.sup fun x ↦ ‖f x‖ₑ) p count < ∞

Tactic:
· exact fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)

Goal state after:
case refine_2
α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst✝ : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ eLpNorm (fun x ↦ Finset.univ.sup fun x ↦ ‖f x‖ₑ) p count < ∞
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h : μ F * 2 ^ finrank ℝ E < μ s
⊢ μ F * 2 ^ finrank ℝ E < ENNReal.ofReal (2⁻¹ ^ finrank ℝ E) * 2 ^ finrank ℝ E * μ s

Tactic:
ofReal_pow (by simp : 0 ≤ (2 : ℝ)⁻¹),

Goal state after:
E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h : μ F * 2 ^ finrank ℝ E < μ s
⊢ μ F * 2 ^ finrank ℝ E < ENNReal.ofReal 2⁻¹ ^ finrank ℝ E * 2 ^ finrank ℝ E * μ s
Module: Mathlib.MeasureTheory.Function.UnifTight

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

Tactic:
by
  refine tendsto_of_subseq_tendsto fun ns hns => ?_
  obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns
  exact ⟨ms,
    tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
      (fun ε hε => -- `UnifIntegrable` on a subsequence
        let ⟨δ, hδ, hδ'⟩ := hui hε
        ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      (fun ε hε => -- `UnifTight` on a subsequence
        let ⟨s, hμs, hfε⟩ := hut hε
        ⟨s, hμs, fun i => hfε _⟩)
      hms'⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 0 < p

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ -1 < q + 1

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : t < 0
h : 0 ≤ t ∧ 2 * t ≤ 1
⊢ False

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : t < 0
h : 0 ≤ t ∧ t ≤ 1
⊢ False

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 2 * t < 1

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ t < 1

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 0 < p

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ -1 < q + 1

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ -2 < 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ p ≠ 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ -2 < 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ p ≠ 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
ω✝ : E → E →L[𝕜] F
γab✝ : Path c b
γbc✝ : Path b a
⊢ 1 - t < 1 / 2

Tactic:
linarith

Goal state after: