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

Goal state before:
pp: case refine_1
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
⊢ ∀ (n : ℕ), IsOpen[inst✝³] (u n)

Tactic:
intro n
    have : u n ∈ T' := by rw [hu]; exact mem_range_self n
    rcases mem_insert_iff.1 this with h | h
    · rw [h]
      exact isOpen_empty
    · exact T_open _ h

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

Goal state before:
pp: case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ Integrable (K.indicator f) μ

pp: case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ MemLp g ∞ μ

Tactic:
· rw [integrable_indicator_iff hK.measurableSet]
    exact hf.integrableOn_isCompact hK

Goal state after:
case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ MemLp g ∞ μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ Integrable (K.indicator f) μ

pp: case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ MemLp g ∞ μ

Tactic:
· rw [integrable_indicator_iff hK.measurableSet]
    exact hf.integrableOn_isCompact hK

Goal state after:
case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ MemLp g ∞ μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst✝ : AddCommMonoid β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
⊢ FinMeasAdditive μ (T + T')

Tactic:
intro s t hs ht hμs hμt hst
  simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
  abel

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

Goal state before:
pp: case refine_2.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ Disjoint (S a) (⋃ i ∈ s, S i)

Tactic:
· simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ {x ∈ f.range | x ≠ 0}
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ {x ∈ f.range | x ≠ 0}
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0

Tactic:
rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (f a) ∂μ).toReal

Tactic:
by
  have hf' : f.FinMeasSupp μ := integrable_iff_finMeasSupp.1 hf
  simp only [← map_apply g f, lintegral_eq_lintegral]
  rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]
  · refine Finset.sum_congr rfl fun b _ => ?_
    rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
  · rintro a -
    by_cases a0 : a = 0
    · rw [a0, hg0, zero_mul]; exact WithTop.zero_ne_top
    · apply mul_ne_top (ht a) (hf'.meas_preimage_singleton_ne_zero a0).ne
  · simp [hg0]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun n ↦ ↑((x n).toLp ⋯)) atTop (𝓝 ↑g)
⊢ Tendsto (fun n ↦ coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x n).toLp ⋯, ⋯⟩) atTop (𝓝 g)

Tactic:
rw [tendsto_iff_dist_tendsto_zero] at this ⊢

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b ↦ dist ↑((x b).toLp ⋯) ↑g) atTop (𝓝 0)
⊢ Tendsto (fun b ↦ dist (coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x b).toLp ⋯, ⋯⟩) g) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range, (⇑(T (⇑f ⁻¹' {x})) + ⇑(T' (⇑f ⁻¹' {x}))) x =
    ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x

Tactic:
simp_rw [Pi.add_apply, sum_add_distrib]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a
a✝ : α
ha : f a✝ =ᵐ[ν] g a✝
⊢ f a✝ =ᵐ[ν] g a✝

Tactic:
filter_upwards [ha] with _ hb using hb

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
b : E
hb : b ∈ f.range
⊢ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖ ≤ C * μ.real (⇑f ⁻¹' {b}) * ‖b‖

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
hb : 0 ∈ f.range
⊢ ‖T (⇑f ⁻¹' {0})‖ * ‖0‖ ≤ C * μ.real (⇑f ⁻¹' {0}) * ‖0‖

case inr
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
b : E
hb✝ : b ∈ f.range
hb : b ≠ 0
⊢ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖ ≤ C * μ.real (⇑f ⁻¹' {b}) * ‖b‖
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ Tendsto (u / v) l (𝓝 1)

Tactic:
convert! this.add key

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝

case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
s : Multiset ι
f g : ι → α → β
h : ∀ i ∈ s, f i ~[l] g i
⊢ (fun x ↦ (Multiset.map (fun x_1 ↦ f x_1 x) s).prod) ~[l] fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) s).prod

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
  exact listProd h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ 0 ≤ᵐ[μ] fun x ↦ (f x).toReal

Tactic:
exact Eventually.of_forall fun x => ENNReal.toReal_nonneg

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

Goal state before:
pp: case refine_2.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

Tactic:
filter_upwards [h_tendsto] with x hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
x : α
hx : Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ (fun s ↦ c • T s) ⋯ f = c • setToFun μ T hT f

pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ (fun s ↦ c • T s) ⋯ f = c • setToFun μ T hT f

Tactic:
· simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left hT c]

Goal state after:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ (fun s ↦ c • T s) ⋯ f = c • setToFun μ T hT f
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
⊢ (∀ i ∈ ∅, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)

Tactic:
intro _

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
hf✝ : ∀ i ∈ ∅, Integrable (f i) μ
⊢ setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
⊢ s * t ⊆ (fun p ↦ p.1 * p.2) '' closedBall 0 Af ×ˢ closedBall 0 Ag

Tactic:
intro _

Goal state after:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
a✝ : ℝ≥0
⊢ a✝ ∈ s * t → a✝ ∈ (fun p ↦ p.1 * p.2) '' closedBall 0 Af ×ˢ closedBall 0 Ag
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h✝ : Subsingleton E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i, ‖t i • g i‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖

Tactic:
rw [smul_mul_assoc]

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊

Tactic:
v.sum_equivFun

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ‖u e‖₊ = ‖u e‖₊
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist (f x) (f y) ≤ b
x y : α
⊢ dist ((c • f.toContinuousMap).toFun x) ((c • f.toContinuousMap).toFun y) ≤ dist c 0 * b

Tactic:
refine (dist_smul_pair c (f x) (f y)).trans ?_
          gcongr
          apply hb

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
hx' : ∀ y ∈ F, 1 ≤ ‖y - x‖
⊢ ∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

Tactic:
exact ⟨x, xR, fun y hy => hx' _ (Submodule.subset_span hy)⟩

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

Goal state before:
pp: case pos.h_add
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ : α → E
⊢ ∀ ⦃g : α → E⦄,
    Disjoint (Function.support f₂) (Function.support g) →
      Integrable f₂ μ →
        Integrable g μ →
          setToFun μ T hT f₂ = setToFun μ' T hT' f₂ →
            setToFun μ T hT g = setToFun μ' T hT' g → setToFun μ T hT (f₂ + g) = setToFun μ' T hT' (f₂ + g)

Tactic:
g₂

Goal state after:
case pos.h_add
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
⊢ Disjoint (Function.support f₂) (Function.support g₂) →
    Integrable f₂ μ →
      Integrable g₂ μ →
        setToFun μ T hT f₂ = setToFun μ' T hT' f₂ →
          setToFun μ T hT g₂ = setToFun μ' T hT' g₂ → setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))
x : α
⊢ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x ≠ ∞

Tactic:
by_cases x_mem : x ∈ closure E <;> simp [x_mem]

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y

Tactic:
edist_dist,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal (dist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y)) ≤ ↑δ.toNNReal⁻¹ * edist x y