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

Goal state before:
pp: case calc_1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst✝¹, _] f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i ↦ (μs i) {a | t < f a}) atTop

pp: case calc_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst✝¹, _] f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i ↦ (μs i) {a | t < f a}) atTop ≤
    liminf (fun i ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop

Tactic:
· -- (i)
    exact (lintegral_mono (fun t ↦ h_opens _ (continuous_def.mp f_cont _ isOpen_Ioi))).trans
            (le_refl _)

Goal state after:
case calc_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst✝¹, _] f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i ↦ (μs i) {a | t < f a}) atTop ≤
    liminf (fun i ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
⊢ IndepSets (s i) (s j) κ μ

Tactic:
by
  classical
  intro t₁ t₂ ht₁ ht₂
  have hf_m : ∀ x : ι, x ∈ ({i, j} : Finset ι) → ite (x = i) t₁ t₂ ∈ s x := by
    intro x hx
    rcases Finset.mem_insert.mp hx with hx | hx
    · simp [hx, ht₁]
    · simp [Finset.mem_singleton.mp hx, hij.symm, ht₂]
  have h_inter : ⋂ (t : ι) (_ : t ∈ ({i, j} : Finset ι)), ite (t = i) t₁ t₂ =
      ite (i = i) t₁ t₂ ∩ ite (j = i) t₁ t₂ := by
    simp only [Finset.set_biInter_singleton, Finset.set_biInter_insert]
  filter_upwards [h_indep {i, j} hf_m] with a h_indep'
  grind

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 κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ (κ a) (t1 ∩ uᶜ) = (κ a) t1 * (κ a) uᶜ

Tactic:
← Set.sdiff_eq,

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ (κ a) (t1 \ u) = (κ a) t1 * (κ a) uᶜ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)

Tactic:
filter_upwards [ihf] with a ha

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)
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 Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
let f := fun n => ite (n = a) t2 (ite (n ∈ s) (ft1 n) Set.univ)
  have h_f_mem : ∀ n ∈ insert a s, f n ∈ π n := by
    intro n hn_mem_insert
    dsimp only [f]
    rcases Finset.mem_insert.mp hn_mem_insert with hn_mem | hn_mem
    · simp [hn_mem, ht2_mem_pia]
    · grind
  have h_f_mem_pi : ∀ n ∈ s, f n ∈ π n := fun x hxS => h_f_mem x (by simp [hxS])
  have h_t1 : t1 = ⋂ n ∈ s, f n := by
    suffices h_forall : ∀ n ∈ s, f n = ft1 n by grind
    intro n hnS
    have hn_ne_a : n ≠ a := by rintro rfl; exact haS (hs_mem hnS)
    simp_rw [f, if_pos hnS, if_neg hn_ne_a]
  have h_μ_t1 : ∀ᵐ a' ∂μ, κ a' t1 = ∏ n ∈ s, κ a' (f n) := by
    filter_upwards [hp_ind s h_f_mem_pi] with a' ha'
    rw [h_t1, ← ha']
  have h_t2 : t2 = f a := by simp [f]
  have h_μ_inter : ∀ᵐ a' ∂μ, κ a' (t1 ∩ t2) = ∏ n ∈ insert a s, κ a' (f n) := by
    have h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n := by
      rw [h_t1, h_t2, Finset.set_biInter_insert, Set.inter_comm]
    filter_upwards [hp_ind (insert a s) h_f_mem] with a' ha'
    rw [h_t1_inter_t2, ← ha']
  have has : a ∉ s := fun has_mem => haS (hs_mem has_mem)
  filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2
  rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
r : ℝ≥0
hr : r < ν G
⊢ ∀ᶠ (a : ι) in l, r < (μ a) G

Tactic:
obtain ⟨T, TS, T_meas, TG⟩ :
      ∃ T : Finset (Set Ω), (∀ t ∈ T, t ∈ S) ∧ (r < ν (⋃ t ∈ T, t)) ∧ (⋃ t ∈ T, t) ⊆ G :=
    ν.exists_lt_measure_biUnion_of_isOpen h hG hr

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
r : ℝ≥0
hr : r < ν G
T : Finset (Set Ω)
TS : ∀ t ∈ T, t ∈ S
T_meas : r < ν (⋃ t ∈ T, t)
TG : ⋃ t ∈ T, t ⊆ G
⊢ ∀ᶠ (a : ι) in l, r < (μ a) G
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Var[fun ω ↦ -X ω; μ] = Var[X; μ]

Tactic:
by
  convert! variance_const_mul (-1) X μ
  · ext; ring
  · simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X + -Y, Z; μ] = cov[X, Z; μ] + -cov[Y, Z; μ]

Tactic:
covariance_add_left hX hY.neg hZ,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X, Z; μ] + cov[-Y, Z; μ] = cov[X, Z; μ] + -cov[Y, Z; μ]
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun x ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun x ↦ ‖Y x‖ₑ
⊢ ↑c * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ) ≤ ∫⁻ (ω : Ω), ‖B (X ω) (Y ω)‖ₑ ∂μ

Tactic:
rw [← lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.enorm hY.enorm J,
        ← lintegral_const_mul'' _ (by fun_prop)]
      gcongr with ω
      simp [hB, ← mul_assoc]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
this : IsProbabilityMeasure μ
⊢ (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ = 0

Tactic:
sub_self

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
this : IsProbabilityMeasure μ
⊢ 0 = 0
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB✝ : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖(B x) y‖ₑ
h : ¬Integrable (fun ω ↦ (B (f (X ω))) (g (Y ω))) μ
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
rw [integral_undef h]

Goal state after:
case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB✝ : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖(B x) y‖ₑ
h : ¬Integrable (fun ω ↦ (B (f (X ω))) (g (Y ω))) μ
⊢ 0 = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
⊢ essSup f μ = essSup g ν

Tactic:
have I : ∀ a, μ {x : α | a < f x} = ν {x : β | a < g x} := fun a =>
    h.measure_mem_eq measurableSet_Ioi
  simp_rw [essSup_eq_sInf, I]

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X' μ'

Tactic:
exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Goal state after:
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 α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω ↦ 1) ⁻¹' π i) = ∏ i ∈ S, (κ a) (((s i).indicator fun _ω ↦ 1) ⁻¹' π i)

Tactic:
simp_rw [Set.indicator_const_preimage_eq_union]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    (κ a) (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) =
      ∏ x ∈ S, (κ a) ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅)
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
n : ℕ
⊢ r ≤ (↑(n + 1))⁻¹ * ∑ x ∈ Finset.range (n + 1), μ (s x)

Tactic:
← ENNReal.div_eq_inv_mul,

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
n : ℕ
⊢ r ≤ (∑ x ∈ Finset.range (n + 1), μ (s x)) / ↑(n + 1)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case refine_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ✝ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
hXZ : Tendsto (fun n ↦ ⟨Measure.map (X n) μ'', ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)
⊢ Tendsto (fun n ↦ |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|) l (𝓝 0)

Tactic:
simp_rw [tendsto_iff_forall_lipschitz_integral_tendsto] at hXZ

Goal state after:
case refine_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ✝ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
hXZ :
  ∀ (f : E → ℝ),
    (∃ C, ∀ (x y : E), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) →
        Tendsto (fun i ↦ ∫ (ω : E), f ω ∂↑⟨Measure.map (X i) μ'', ⋯⟩) l (𝓝 (∫ (ω : E), f ω ∂↑⟨Measure.map Z μ', ⋯⟩))
⊢ Tendsto (fun n ↦ |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|) l (𝓝 0)
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
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s

Tactic:
have h_vol : μ F < μ ((2⁻¹ : ℝ) • s) := by
    rw [addHaar_smul_of_nonneg μ (by simp : 0 ≤ (2 : ℝ)⁻¹) s,
      ← ENNReal.mul_lt_mul_iff_left (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (by finiteness),
      mul_right_comm, ofReal_pow (by simp : 0 ≤ (2 : ℝ)⁻¹), ofReal_inv_of_pos zero_lt_two]
    simpa [← mul_pow, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

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
h_vol : μ F < μ (2⁻¹ • s)
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
V : ℝ → ℂ → ℂ := fun θ w ↦ circleTransformDeriv R z w (fun x ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z ↑⟨(v, y1), ⋯⟩‖ * ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖ * ‖f X‖
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖

Tactic:
hfun

Goal state after:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
V : ℝ → ℂ → ℂ := fun θ w ↦ circleTransformDeriv R z w (fun x ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z ↑⟨(v, y1), ⋯⟩‖ * ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖ * ‖f X‖
⊢ ‖circleTransformDeriv R z v f y1‖ ≤ ‖V b a‖ * ‖f X‖
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
⊢ (r • f).toReal = r • f.toReal

Tactic:
ext; simp [NNReal.smul_def]

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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
H₂ : 2 • I =ᶠ[𝓝 (2 * t)] I
⊢ (ω ((fun s ↦ γab.extend (2 * s)) t)) (derivWithin (fun s ↦ γab.extend (2 * s)) I t) =
    2 • (ω (γab.extend (2 * t))) (derivWithin ⇑γab.extend I (2 * t))

Tactic:
derivWithin_comp_mul_left,

Goal state after:
𝕜 : 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)
H₂ : 2 • I =ᶠ[𝓝 (2 * t)] I
⊢ (ω ((fun s ↦ γab.extend (2 * s)) t)) (2 • derivWithin (⇑γab.extend) (2 • I) (2 * t)) =
    2 • (ω (γab.extend (2 * t))) (derivWithin ⇑γab.extend I (2 * t))