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

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ f ⁻¹' (f '' K)ᶜ ⊆ Kᶜ

Tactic:
simp only [preimage_compl, compl_subset_compl]

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ K ⊆ f ⁻¹' f '' K
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case hs
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : ↑M
s : Set Ω'
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω') ∂↑↑μ, x ∈ range f

Tactic:
exact (null_iff_toMeasure_null (↑μ) (range f)ᶜ).mp (by exact μ.2)

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

Goal state before:
pp: case neg
α : 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 ∩ univ) = (κ a) (f1 n) * 1

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
h✝ : n ∈ p2
⊢ (κ a) (univ ∩ f2 n) = 1 * (κ a) (f2 n)

pp: case neg
α : 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
h✝ : n ∉ p2
⊢ (κ a) (univ ∩ univ) = 1 * 1

Tactic:
all_goals simp only [measure_univ, one_mul, mul_one, Set.inter_univ, Set.univ_inter]

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

Goal state before:
pp: case iSup
Ω : 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 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ) →
          ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω * T.indicator (fun x ↦ c) ω ∂μ =
            (∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
intro f h_meas_f h_mono_f h_ind_f

Goal state after:
case iSup
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω * T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝ : Disjoint (Function.support f') (Function.support g)
⊢ Measurable f' →
    Measurable g →
      ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
        ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
          ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
h_measMg_f'

Goal state after:
case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
⊢ Measurable g →
    ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
      ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
        ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
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, Y; μ] + cov[X, Z; μ]

Tactic:
rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]

Goal state after:
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✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable id (Measure.map f μ) ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t

Tactic:
refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
hB : MeasurableSet B
⊢ (μ (f ⁻¹' A ∩ g ⁻¹' B)).toReal = (μ (f ⁻¹' A) * μ (g ⁻¹' B)).toReal

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
hB : MeasurableSet B
⊢ μ (f ⁻¹' A) * μ (g ⁻¹' B) ≠ ∞

Tactic:
toReal_mul,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
hB : MeasurableSet B
⊢ (μ (f ⁻¹' A ∩ g ⁻¹' B)).toReal = (μ (f ⁻¹' A)).toReal * (μ (g ⁻¹' B)).toReal

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
hB : MeasurableSet B
⊢ μ (f ⁻¹' A) * μ (g ⁻¹' B) ≠ ∞
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: case lim
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ i x = ((fun y ↦ atTop.limUnder fun x ↦ h x y) ∘ f) x

Tactic:
rw [Function.comp_apply, Tendsto.limUnder_eq]

Goal state after:
case lim
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ Tendsto (fun x_1 ↦ h x_1 (f x)) atTop (𝓝 (i x))
Module: Mathlib.MeasureTheory.Function.Floor

Goal state before:
pp: R : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : OrderTopology R
inst✝² : MeasurableSpace R
inst✝¹ : IsStrictOrderedRing R
inst✝ : BorelSpace R
⊢ Measurable Int.fract

Tactic:
intro s hs

Goal state after:
R : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : OrderTopology R
inst✝² : MeasurableSpace R
inst✝¹ : IsStrictOrderedRing R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract ⁻¹' s)
Module: Mathlib.MeasureTheory.Function.Floor

Goal state before:
pp: case inl
R : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
n : R
h : ⌈n⌉₊ = 0
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})

Tactic:
simp_all [Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]

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

Goal state before:
pp: case inr
R : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
n : R
h : ⌈n⌉₊ ≠ 0
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})

Tactic:
simp_all [Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]

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
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j

Tactic:
by
        by_cases h_nonempty : Set.Nonempty s
        swap; · simp only [h_nonempty, if_false, le_refl]
        simp only [h_nonempty, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp,
          forall_apply_eq_imp_iff₂]
        refine fun f hf_mem => le_trans ?_ (f.mono hij)
        have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' s := ⟨f, hf_mem, rfl⟩
        exact sInf_le hfi_mem

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
this : ∀ᶠ (n : ℕ) in atTop, e ↑((G n).index x) = hs.index x
⊢ ∀ᶠ (n : ℕ) in atTop, (⋯.approx n) x = (⋯.approx n) x

Tactic:
filter_upwards [this] with n hn using by rw [hn]

Goal state after:
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
⊢ (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν =
    (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν.haarScalarFactor μ • μ

Tactic:
integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport ν μ f_cont f_comp

Goal state after:
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
⊢ (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν.haarScalarFactor μ • μ =
    (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν.haarScalarFactor μ • μ
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬g 0 = 0
⊢ HasCompactSupport (ContinuousMap.toFun 0)

Tactic:
exact .zero

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeSup β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x✝ : α
⊢ (s.sup' H f) x✝ = s.sup' H (fun i ↦ ⇑(f i)) x✝

Tactic:
simp [finsetSup'_apply]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
f : G
⊢ HasCompactSupport ⇑f

Tactic:
exact HasCompactSupport.of_compactSpace f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case hderiv
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x

Tactic:
rw [min_eq_left hab, max_eq_right hab]
    intro t ht
    exact hfd.hasDerivAt (isOpen_Ioo.mem_nhds ht) |>.hasDerivWithinAt

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case hBi
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := ⋯
hsm : MeasurableSet s
⊢ IntervalIntegrable (s.indicator fun x ↦ C) volume a b

Tactic:
intervalIntegrable_iff_integrableOn_Ioo_of_le hab

Goal state after:
case hBi
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ IntegrableOn (s.indicator fun x ↦ C) (Ioo a b) volume
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x

Tactic:
by
  simp only [torusIntegral, integral_smul, ← smul_comm a (_ : ℂ) (_ : E)]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ max (#↑s) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Tactic:
exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ charFun (μ ∗ ν) t = charFun μ t * charFun ν t

Tactic:
charFun_apply

Goal state after:
E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ ∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂μ ∗ ν = (∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂μ) * ∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂ν
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
⊢ charFun (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F))) ξ) t =
    charFun (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F))) (μ.prod ν)) t

Tactic:
MeasurableEquiv.coe_toLp,

Goal state after:
E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
⊢ charFun (Measure.map (toLp 2) ξ) t = charFun (Measure.map (toLp 2) (μ.prod ν)) t
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ charFun (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i))) ν) t =
    charFun (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i))) (Measure.pi μ)) t

Tactic:
MeasurableEquiv.coe_toLp,

Goal state after:
ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ charFun (Measure.map (toLp 2) ν) t = charFun (Measure.map (toLp 2) (Measure.pi μ)) t