mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : 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
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
have hfX := (hf.comp_aemeasurable hX)

Goal state after:
Ω : 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) μ
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e_f.hY
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (fun ω ↦ ω i) (Measure.pi μ)

Tactic:
· exact Measurable.aemeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ Measure.map (u ∘ f) μ = Measure.map (u ∘ g) ν

Tactic:
← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ Measure.map u (Measure.map f μ) = Measure.map (u ∘ g) ν
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : (𝓝[>] i).NeBot
⊢ ⨅ j, ⨅ (_ : j > i), ↑𝓕 j ≤ m

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : ¬(𝓝[>] i).NeBot
⊢ ↑𝓕 i ≤ m

Tactic:
· obtain ⟨j, hj⟩ := (frequently_gt_nhds i).exists
        exact iInf₂_le_of_le j hj (𝓕.le j)

Goal state after:
case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : ¬(𝓝[>] i).NeBot
⊢ ↑𝓕 i ≤ m
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁴ : (i : ι) → TopologicalSpace (β i)
inst✝³ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝² : ∀ (i : ι), BorelSpace (β i)
inst✝¹ : Preorder ι
X : ι → Type u_4
inst✝ : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ (fun i ↦ MeasurableSpace.comap (restrictLe i) MeasurableSpace.pi) i ≤
    (fun i ↦ MeasurableSpace.comap (restrictLe i) MeasurableSpace.pi) j

Tactic:
simp only
    rw [← restrictLe₂_comp_restrictLe hij, ← comap_comp]
    exact comap_mono (measurable_restrictLe₂ _).comap_le

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

Goal state before:
pp: Ω : Type u_1
ι✝ : Type u_2
m : MeasurableSpace Ω
β : ι✝ → Type u_3
inst✝⁴ : (i : ι✝) → TopologicalSpace (β i)
inst✝³ : ∀ (i : ι✝), MetrizableSpace (β i)
mβ : (i : ι✝) → MeasurableSpace (β i)
inst✝² : ∀ (i : ι✝), BorelSpace (β i)
inst✝¹ : Preorder ι✝
ι : Type u_4
X : ι → Type u_5
inst✝ : (i : ι) → MeasurableSpace (X i)
s t : Finset ι
hst : s ⊆ t
⊢ (fun s ↦ MeasurableSpace.comap s.restrict MeasurableSpace.pi) s ≤
    (fun s ↦ MeasurableSpace.comap s.restrict MeasurableSpace.pi) t

Tactic:
by
    simp only
    rw [← restrict₂_comp_restrict hst, ← comap_comp]
    exact comap_mono (measurable_restrict₂ hst).comap_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε

Tactic:
by_cases hη_top : η = ∞

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε
hη_top : η = ∞
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε
hη_top : ¬η = ∞
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη_top : η = ∞
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < ↑ε
i : ι
⊢ eLpNorm (∅ᶜ.indicator ((f + g) i)) p μ ≤ ↑ε

Tactic:
simp only [compl_empty, indicator_univ, Pi.add_apply]

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη_top : η = ∞
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < ↑ε
i : ι
⊢ eLpNorm (f i + g i) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
i : ι
hi : μ (F i) ≠ 0
hi' : μ (F i) ≠ ∞
⊢ μ (univ ∩ F i) / μ (F i) = 1

Tactic:
simp [ENNReal.div_self hi hi']

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
⊢ ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) * ((∫ (x : G), f (x * g) ∂μ) / ∫ (x : G), f x ∂μ) =
    1 * ((∫ (x : G), f (x * g) ∂μ) / ∫ (x : G), f x ∂μ)

Tactic:
by rw [r]

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 β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
⊢ C(α, γ)

Tactic:
exact if g 0 = 0 then g.comp f else 0

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ toNNRealLinear (toRealPositiveLinear Λ) = Λ

Tactic:
ext f
  simp

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
⊢ -(2 • -curveIntegralFun ω γbc (1 - 2 * (1 - t))) = 2 • curveIntegralFun ω γbc (2 * t - 1)

Tactic:
smul_neg,

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₀ : 1 / 2 < t
⊢ - -(2 • curveIntegralFun ω γbc (1 - 2 * (1 - t))) = 2 • curveIntegralFun ω γbc (2 * t - 1)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
have hgd : DifferentiableOn ℝ g (Ioo a b) :=
      UniformSpace.Completion.toComplL.differentiable.comp_differentiableOn hfd

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
⊢ ‖f b - f a‖ ≤ C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0}

Tactic:
have hC₀ : 0 ≤ C := (norm_nonneg _).trans <| hC _ <| hmem_s (1 / 2) (by norm_num)

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
⊢ ‖f b - f a‖ ≤ C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0}
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a✝ b c d : E
γ₁ : Path a✝ b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a, b_1) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b_1))) t (φ (a, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b_1)), ((dω (φ (a, b_1))) u) v = ((dω (φ (a, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a b_1 : ↑I), ψ (↑a, ↑b_1) = φ (a, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
a : ℝ × ℝ
haU : a ∈ U
⊢ Icc 0 1 ∈ 𝓝 a

Tactic:
rwa [← mem_interior_iff_mem_nhds, hinterior]

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a✝ b c d : E
γ₁ : Path a✝ b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a, b_1) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b_1))) t (φ (a, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b_1)), ((dω (φ (a, b_1))) u) v = ((dω (φ (a, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a b_1 : ↑I), ψ (↑a, ↑b_1) = φ (a, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
a : ℝ × ℝ
haU : a ∈ U
⊢ Icc 0 1 ∈ 𝓝 a

Tactic:
rwa [← mem_interior_iff_mem_nhds, hinterior]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₁
⊢ s₁ ⊆ ((fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ) 1)ᶜ

Tactic:
simp only [Fin.isValue, one_ne_zero, ↓reduceIte, compl_compl, subset_refl]

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

Goal state before:
pp: case refine_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ AEStronglyMeasurable (fun θ ↦ (∏ i, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ))
    (volume.restrict (Icc 0 fun x ↦ 2 * π))

Tactic:
refine (Continuous.aestronglyMeasurable ?_).smul hf.1

Goal state after:
case refine_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ Continuous fun θ ↦ ∏ i, ↑(R i) * cexp (↑(θ i) * I) * I
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x - g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) - ∯ (x : Fin n → ℂ) in T(c, R), g x

Tactic:
simpa only [sub_eq_add_neg, ← torusIntegral_neg] using! torusIntegral_add hf hg.neg

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
a✝ : ℝ
hz : a✝ ∈ range ⇑f
⊢ a✝ ∈ Ioc (a + ↑0 * ε) (a + ↑N * ε)

Tactic:
simpa using Ioo_subset_Ioc_self (hf hz)

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x ↦ 2 * π
⊢ ((↑(R i) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm (θ, Θ) i) * I) * I *
        ∏ i_1,
          ↑(R (i.succAbove i_1)) *
              cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm (θ, Θ) (i.succAbove i_1)) * I) *
            I) •
      f fun i_1 ↦ c i_1 + ↑(R i_1) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm (θ, Θ) i_1) * I)) =
    (↑(R i) * cexp (↑θ * I) * I * ∏ i_1, ↑((R ∘ i.succAbove) i_1) * cexp (↑(Θ i_1) * I) * I) •
      f
        (i.insertNth (circleMap (c i) (R i) θ) fun i_1 ↦
          (c ∘ i.succAbove) i_1 + ↑((R ∘ i.succAbove) i_1) * cexp (↑(Θ i_1) * I))

Tactic:
simp only [MeasurableEquiv.piFinSuccAbove_symm_apply, i.insertNth_apply_same,
      i.insertNth_apply_succAbove, (· ∘ ·), Fin.insertNthEquiv, Equiv.coe_fn_mk]

Goal state after:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x ↦ 2 * π
⊢ ((↑(R i) * cexp (↑θ * I) * I * ∏ x, ↑(R (i.succAbove x)) * cexp (↑(Θ x) * I) * I) •
      f fun i_1 ↦ c i_1 + ↑(R i_1) * cexp (↑(i.insertNth θ Θ i_1) * I)) =
    (↑(R i) * cexp (↑θ * I) * I * ∏ x, ↑(R (i.succAbove x)) * cexp (↑(Θ x) * I) * I) •
      f
        (i.insertNth (circleMap (c i) (R i) θ) fun i_1 ↦
          c (i.succAbove i_1) + ↑(R (i.succAbove i_1)) * cexp (↑(Θ i_1) * 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
μ : Measure E
ν : Measure F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
t : WithLp 2 (E × F)
⊢ ∫ (x : WithLp 2 (E × F)),
      cexp
        (↑(⟪x.ofLp.1, t.ofLp.1⟫ + ⟪x.ofLp.2, t.ofLp.2⟫) *
          I) ∂Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F))) (μ.prod ν) =
    ∫ (z : E × F), cexp (↑⟪z.1, t.ofLp.1⟫ * I) * cexp (↑⟪z.2, t.ofLp.2⟫ * I) ∂μ.prod ν

Tactic:
integral_map_equiv

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
μ : Measure E
ν : Measure F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
t : WithLp 2 (E × F)
⊢ ∫ (x : E × F),
      cexp
        (↑(⟪((MeasurableEquiv.toLp 2 (E × F)) x).ofLp.1, t.ofLp.1⟫ +
              ⟪((MeasurableEquiv.toLp 2 (E × F)) x).ofLp.2, t.ofLp.2⟫) *
          I) ∂μ.prod ν =
    ∫ (z : E × F), cexp (↑⟪z.1, t.ofLp.1⟫ * I) * cexp (↑⟪z.2, t.ofLp.2⟫ * I) ∂μ.prod ν