mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ ↑(n + 1) ≠ ∞ ∨ ∑ x ∈ Finset.range (n + 1), μ (s x) ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case e'_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
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure μ'' (fun n ω ↦ (0, Y n ω - c)) l 0
n : ι
ω : Ω''
⊢ (((fun n ω ↦ (X n ω, Y n ω)) - fun n ω ↦ (X n ω, c)) n ω).1 = 0

Tactic:
simp

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

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

Tactic:
simp

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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (∏ i, if i ∈ s then (κ a)[f i | Y i ⁻¹' t i] else 1) = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ eLpNorm f p (dirac i) = eLpNorm f p (count.restrict {i})

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
f : ↥(Lp E p ν)
⊢ f ∈ ↑(simpleFunc E p ν) →
    Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦
      (compMeasurePreserving ⇑↑(f, y).2 ⋯) (f, y).1

Tactic:
hf

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
f : ↥(Lp E p ν)
hf : f ∈ ↑(simpleFunc E p ν)
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦
    (compMeasurePreserving ⇑↑(f, y).2 ⋯) (f, y).1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst✝ : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
⊢ eLpNorm f p count < ∞

Tactic:
by
  have := Fintype.ofFinite α
  refine (eLpNorm_mono_enorm (g := fun _ ↦ Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_
  · exact fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
  · exact (memLp_const_enorm <| by simp [h, LT.lt.ne]).eLpNorm_lt_top

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

Goal state before:
pp: case refine_1.inl
α : Type u_2
inst✝¹ : MeasurableSpace α
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
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
x : α
n : ℕ
inst✝ : IsFiniteMeasure 0
hr : ∀ (n : ℕ), r ≤ 0 (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f 0 < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : 0 N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < 0 (⋂ n ∈ u, s n)
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂0
hμ : 0 ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂0 ≤ 0 univ
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun x ↦ f x a) atTop ∂0 ≤ limsup (fun x_1 ↦ f x_1 x) atTop
⊢ ⨍⁻ (x : α), f n x ∂0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: case pos
ι : 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 : Finite ι
⊢ StronglyMeasurable (hs.piecewise f)

pp: case neg
ι : 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 : ¬Finite ι
⊢ StronglyMeasurable (hs.piecewise f)

Tactic:
· refine ⟨fun n => simpleFunc_piecewise hs hm (fun i => (hf i).approx n), fun x => ?_⟩
    simp [simpleFunc_piecewise, piecewise_apply, StronglyMeasurable.tendsto_approx]

Goal state after:
case neg
ι : 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 : ¬Finite ι
⊢ StronglyMeasurable (hs.piecewise f)
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 : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hε : ∞ ≠ 0
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ∞

Tactic:
simp

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η_top : η = ∞
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ∞ → eLpNorm g p μ ≤ ∞ → eLpNorm (f + g) p μ < ↑ε
⊢ μ ∅ ≠ ∞

Tactic:
simp

Goal state after:
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
l : Filter ι
inst✝¹ : NeZero μ
inst✝ : IsFiniteMeasure μ
⊢ ∀ᶠ (i : ι) in l, MeasurableSet univ

Tactic:
simp

Goal state after:
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
l : Filter ι
inst✝¹ : NeZero μ
inst✝ : IsFiniteMeasure μ
⊢ ∀ᶠ (i : ι) in l, μ univ ≠ ∞

Tactic:
simp

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 β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ∞
⊢ μ ∅ ≠ ∞

Tactic:
simp

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 β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ∞
⊢ μ ∅ ≠ ∞

Tactic:
simp

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 β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
hι : ¬Nonempty ι
⊢ μ ∅ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ∞
⊢ μ ∅ ≠ ∞

Tactic:
simp

Goal state after:
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
⊢ 0 ≤ 2⁻¹

Tactic:
simp

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 β
p : ℝ≥0∞
inst✝ : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
by
  obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι
  set g : Fin n → α → β := f ∘ hn.some.symm
  have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _
  obtain ⟨s, hμs, hfε⟩ := unifTight_fin hp_top hg hε
  refine ⟨s, hμs, fun i => ?_⟩
  simpa only [g, Function.comp_apply, Equiv.symm_apply_apply] using hfε (hn.some i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
obtain ⟨N, hNε⟩ := hf_tendsto ε (by simpa only [gt_iff_lt, ENNReal.coe_pos])

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Function.UnifTight

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

Tactic:
simp

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

Goal state before:
pp: case pos.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hg' : MemLp g p 0
hui : UnifIntegrable f p 0
hut : UnifTight f p 0
hfg : ∀ᵐ (x : α) ∂0, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p 0 ≤ ε

Tactic:
simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0..2 * π,
      (2 * ↑π * I)⁻¹ • ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I)) =
    (2 * ↑π * I)⁻¹ •
      ∫ (θ : ℝ) in 0..2 * π,
        ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I))

Tactic:
simp

Goal state after:
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✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
this : μ F * 2 ^ finrank ℝ E < μ ↑(S n)
y : E
hy : y ∈ ↑K
⊢ (fun x ↦ ↑(1 + u n) • x) (-y) = -(fun x ↦ ↑(1 + u n) • x) y

Tactic:
simp

Goal state after:
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:
rw [← hgg'x]

Goal state after:
α : 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))
Module: Mathlib.Topology.Homotopy.Affine

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
f g : C(X, E)
⊢ ∀ (x : X), (Path.segment (f (0, x).2) (g (0, x).2)) (0, x).1 = f x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Homotopy.Affine

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
f g : C(X, E)
⊢ ∀ (x : X), (Path.segment (f (1, x).2) (g (1, x).2)) (1, x).1 = g x

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
ι : Type u_5
s : Finset ι
f : ι → α →C_c β
a : α
⊢ (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

Tactic:
simp

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

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p) = 1 / p * Gamma ((q + 1) / p)

Tactic:
rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
      simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by ring, ← integral_const_mul,
        ← mul_assoc]

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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
x : α
⊢ (f + g).toReal x = (f.toReal + g.toReal) x

Tactic:
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
x : α
⊢ (a • f).toReal x = ((RingHom.id ℝ≥0) a • f.toReal) x

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ (toRealLinearMap f) x = ↑(f x)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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 α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f : α →C_c ℝ≥0
⊢ 0 ≤ toRealLinearMap f

Tactic:
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 α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f g : α →C_c ℝ≥0
⊢ NNReal.mk (Λ (toRealLinearMap (f + g))) ⋯ = NNReal.mk (Λ (toRealLinearMap f)) ⋯ + NNReal.mk (Λ (toRealLinearMap g)) ⋯

Tactic:
simp

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f g : α →C_c ℝ≥0
⊢ NNReal.mk (Λ f.toReal + Λ g.toReal) ⋯ = NNReal.mk (Λ f.toReal) ⋯ + NNReal.mk (Λ g.toReal) ⋯
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
nhdsWithin_eq_nhds.2,

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

case inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ Icc 0 2 ∈ 𝓝 (2 * t)
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 : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
⊢ C * ‖b - a‖ * |1 - 0| = C * ‖b - a‖

Tactic:
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 : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ CurveIntegrable ω γ

Tactic:
apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
  simp only [funext (curveIntegralFun_def ω γ)]
  apply ContinuousOn.clm_apply
  · exact hω.comp (by fun_prop) fun _ _ ↦ hγs _
  · exact hγ.continuousOn_derivWithin uniqueDiffOn_Icc_zero_one le_rfl

Goal state after: