mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
⊢ ∃ C, ∀ (i : ℕ), eLpNorm (∑ x ∈ Finset.range i, (↑i)⁻¹ • f x) p μ ≤ ↑C

Tactic:
refine ⟨C, fun n => (eLpNorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans ?_⟩

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
⊢ ∑ i ∈ Finset.range n, eLpNorm ((↑n)⁻¹ • f i) p μ ≤ ↑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 α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ i ∈ Finset.image g s, f' i ∈ π i

Tactic:
Finset.forall_mem_image,

Goal state after:
α : 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 π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ ⦃x : ι'⦄, x ∈ s → f' (g x) ∈ π (g x)
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
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
⊢ ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x

Tactic:
intro x hx

Goal state after:
α : 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
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx : x ∈ {i, j}
⊢ (if x = i then t₁ else t₂) ∈ s x
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
⊢ ∀ (b : ℝ≥0∞), (∀ᶠ (n : ℕ) in atTop, b ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n) → b ≤ ↑‖f‖₊

Tactic:
intro x hx

Goal state after:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
⊢ x ≤ ↑‖f‖₊
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : iIndepFun f μ
⊢ μ univ = 1

Tactic:
by simpa using h.meas_biInter (S := ∅) (s := fun _ ↦ univ)

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
⊢ Tendsto (fun i ↦ μs i) atTop (𝓝 μ)

Tactic:
by
  refine tendsto_of_forall_isOpen_le_liminf_nat' fun G G_open ↦ ?_
  specialize h_opens G G_open
  have aux : ENNReal.ofNNReal (liminf (fun i ↦ μs i G) atTop) =
          liminf (ENNReal.ofNNReal ∘ fun i ↦ μs i G) atTop := by
    refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_
    · exact ENNReal.continuous_coe.continuousAt
    · exact IsBoundedUnder.isCoboundedUnder_ge ⟨1, by simp⟩
    · exact ⟨0, by simp⟩
  have obs := ENNReal.coe_mono h_opens
  simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, aux] at obs
  convert! obs
  simp only [Function.comp_apply, ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS

Tactic:
rw [generateFrom_pi.symm, comap_generateFrom]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ generateFrom ((preimage fun a i ↦ f (↑i) a) '' univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}) = generateFrom πS
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
⊢ MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT

Tactic:
rw [generateFrom_pi.symm, comap_generateFrom]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
⊢ generateFrom ((preimage fun a i ↦ f (↑i) a) '' univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}) = generateFrom πT
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
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

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

Goal state after:
α : 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
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
integral_undef

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ 0 ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ¬Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet {x | p x}
⊢ P {ω | p (X ω)} = μ {x | p x}

Tactic:
rw [← hX.map_eq, map_apply_of_aemeasurable hX.aemeasurable hp]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet {x | p x}
⊢ P {ω | p (X ω)} = P (X ⁻¹' {x | p x})
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝³ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝² : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝¹ : TopologicalSpace E
inst✝ : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
⊢ Tendsto (fun n ↦ ⟨Measure.map (X n) (μ n), ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)

Tactic:
convert! tendsto_const_nhds with j

Goal state after:
case e'_3.e'_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝³ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝² : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝¹ : TopologicalSpace E
inst✝ : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
j : ι
⊢ Measure.map (X j) (μ j) = Measure.map Z μ'
Module: Mathlib.MeasureTheory.Group.IntegralConvolution

Goal state before:
pp: M : Type u_1
F : Type u_2
inst✝⁵ : Monoid M
mM : MeasurableSpace M
inst✝⁴ : MeasurableMul₂ M
inst✝³ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝² : NormedSpace ℝ F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ ∫ (x : M × M), f (x.1 * x.2) ∂μ.prod ν = ∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ

Tactic:
integral_prod

Goal state after:
M : Type u_1
F : Type u_2
inst✝⁵ : Monoid M
mM : MeasurableSpace M
inst✝⁴ : MeasurableMul₂ M
inst✝³ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝² : NormedSpace ℝ F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ ∫ (x : M), ∫ (y : M), f ((x, y).1 * (x, y).2) ∂ν ∂μ = ∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ

case hf
M : Type u_1
F : Type u_2
inst✝⁵ : Monoid M
mM : MeasurableSpace M
inst✝⁴ : MeasurableMul₂ M
inst✝³ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝² : NormedSpace ℝ F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ Integrable (fun x ↦ f (x.1 * x.2)) (μ.prod ν)
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᵐ[μ] f' n
hgg' : g =ᵐ[μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x
x : α
hff'x : ∀ (i : ℕ), f i x = f' i x
hgg'x : g x = g' x
hfgx : Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun x_1 ↦ f x_1 x) atTop (𝓝 (g x))

Tactic:
exact hfgx

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C_c β
x✝ : α
⊢ r • f x✝ * g x✝ = r • (f x✝ * g x✝)

Tactic:
rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ tsupport (⇑f ∘ ⇑g) ⊆ ⇑g ⁻¹' tsupport f.toFun

Tactic:
intro x hx

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
hx : x ∈ tsupport (⇑f ∘ ⇑g)
⊢ x ∈ ⇑g ⁻¹' tsupport f.toFun
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun ⊆
    Function.support f₁.toFun ∪ Function.support f₂.toFun

Tactic:
intro x hx

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
⊢ x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
⊢ f.nnrealPart.toReal - (-f).nnrealPart.toReal = f

Tactic:
by ext x; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
f g : α →C_c ℝ≥0
⊢ (f + g).toReal = f.toReal + g.toReal

Tactic:
by ext x; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
a : ℝ≥0
f : α →C_c ℝ≥0
⊢ (a • f).toReal = (RingHom.id ℝ≥0) a • f.toReal

Tactic:
by ext x; simp

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

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

Tactic:
by ext x; simp

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

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

Tactic:
by ext x; simp

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

Goal state before:
pp: case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : x ∈ Ioi 0
⊢ x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)

Tactic:
rw [mem_Ioi] at hx

Goal state after:
case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : x ∈ Ioi 0
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
rw [mem_Ioi] at hx

Goal state after:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
⊢ ∀ (x : α), 0 ≤ g x → (fun x ↦ (ρ x).toReal) x = g x

Tactic:
intro x hx

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
x : α
hx : 0 ≤ g x
⊢ (fun x ↦ (ρ x).toReal) x = g x
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
⊢ ∀ (x : α), (fun x ↦ (ρ x).toReal) x = g x → (fun a ↦ f a * g a) x = (fun a ↦ (ρ a).toReal * f a) x

Tactic:
intro x hx

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
x : α
hx : (fun x ↦ (ρ x).toReal) x = g x
⊢ (fun a ↦ f a * g a) x = (fun a ↦ (ρ a).toReal * f a) x
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∀ (x : α), g x = 0 x → (fun x ↦ f x * g x) x = 0 x

Tactic:
intro x hx

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
x : α
hx : g x = 0 x
⊢ (fun x ↦ f x * g x) x = 0 x
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
⊢ ∀ (x : α), (fun x ↦ (ρ x).toReal) x = g x → (fun x ↦ (ρ x).toReal * f x) x = (fun x ↦ f x * g x) x

Tactic:
intro x hx

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
x : α
hx : (fun x ↦ (ρ x).toReal) x = g x
⊢ (fun x ↦ (ρ x).toReal * f x) x = (fun x ↦ f x * g x) x