mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : 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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
⊢ setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g

Tactic:
rw [sub_eq_add_neg, setToSimpleFunc_add T h_add hf, setToSimpleFunc_neg T h_add hg,
    sub_eq_add_neg]
  rw [integrable_iff] at hg ⊢
  intro x hx_ne
  rw [SimpleFunc.coe_neg, Pi.neg_def, ← Function.comp_def, preimage_comp, neg_preimage,
    Set.neg_singleton]
  refine hg (-x) ?_
  simp [hx_ne]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integral (c • f) = c • integral f

Tactic:
rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =ᶠ[l] 0

Tactic:
rw [IsEquivalent, sub_zero]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u =o[l] 0 ↔ u =ᶠ[l] 0
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =ᶠ[l] 0

Tactic:
rw [IsEquivalent, sub_zero]
  exact isLittleO_zero_right_iff

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

pp: case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
· conv in 𝓝 _ => rw [← sub_self (1 : β)]
    exact hφ.sub tendsto_const_nhds

Goal state after:
case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Tactic:
integral_eq_lintegral_of_nonneg_ae _ hf.norm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖f x‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Tactic:
by
  have : ‖x‖ ≠ 0 := by simp [hx]
  simp [field, norm_smul, r_nonneg, rclike_simps]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ dist x (y₀ + y) = ‖x - (y₀ + y)‖

Tactic:
dist_eq_norm

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ ‖x - (y₀ + y)‖ = ‖x - (y₀ + y)‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) (c • f) = c • (setToL1 hT) f

Tactic:
rw [setToL1_eq_setToL1' hT h_smul, setToL1_eq_setToL1' hT h_smul]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1' 𝕜 hT h_smul) (c • f) = c • (setToL1' 𝕜 hT h_smul) f
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫ (x : X), f x ∂∑ i ∈ s, μ i ∈ Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ↑ε

Tactic:
Metric.mem_ball,

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ dist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂Measure.sum μ) < ↑ε
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
⊢ dist (x₁ * y₁) (x₂ * y₂) ≤ 2 * Af * Ag

Tactic:
dist_eq_norm

Goal state after:
case h
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
⊢ ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C → ∀ (x : α), dist (f x) (g x) < C

Tactic:
intro w x

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist (f x) (g x) < C
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C✝ : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist ((f n) x) ((f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n ↦ (f n) x
F : α → β
hF : ∀ (x : α), Tendsto (fun n ↦ (f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist ((f 0) x) ((f 0) y) ≤ C
⊢ ∃ C,
    ∀ (x y : α),
      dist ({ toFun := F, continuous_toFun := ⋯ }.toFun x) ({ toFun := F, continuous_toFun := ⋯ }.toFun y) ≤ C

Tactic:
refine ⟨C + (b 0 + b 0), fun x y => ?_⟩

Goal state after:
case refine_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist ((f n) x) ((f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n ↦ (f n) x
F : α → β
hF : ∀ (x : α), Tendsto (fun n ↦ (f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist ((f 0) x) ((f 0) y) ≤ C
x y : α
⊢ dist ({ toFun := F, continuous_toFun := ⋯ }.toFun x) ({ toFun := F, continuous_toFun := ⋯ }.toFun y) ≤ C + (b 0 + b 0)
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ dist f g

Tactic:
dist_eq_norm

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ ‖f - g‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Star

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : α →ᵇ β
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖

Tactic:
by
    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]
    intro x
    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
    exact norm_coe_le_norm (star f * f) x

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

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
have hf : StronglyMeasurable[m] f := @SimpleFunc.stronglyMeasurable β F m _ f

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
hf : StronglyMeasurable ⇑f
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
by
  by_cases x_mem_closure : x ∈ closure E
  · filter_upwards [self_mem_nhdsWithin] with δ δ_pos
    simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]
  · have obs := eventually_notMem_thickening_of_infEDist_pos x_mem_closure
    filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin]
      with δ x_notin_thE _
    simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]

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

Goal state before:
pp: α : 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
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
a : α
h_lin : Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
⊢ Tendsto (fun n ↦ x (n + k)) atTop l

Tactic:
rwa [tendsto_add_atTop_iff_nat]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂ν ∂μ = ∫ (x : X), s.indicator (fun x ↦ ∫ (y : Y), f x y ∂ν) x ∂μ

Tactic:
integral_indicator₂

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

Goal state before:

Tactic:
rightLim f z ≤ f a := hf.rightLim_le za
        _ < u := (h'y ⟨hz.1.trans_lt za, ay⟩).2

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

Goal state before:
pp: case refine_2
α : 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 : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a

pp: case refine_3
α : 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 : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x ↦ fs x a) s x

Tactic:
· filter_upwards [self_mem_nhdsWithin] with x hx using h_bound x hx

Goal state after:
case refine_3
α : 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 : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x ↦ fs x a) s x
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
⊢ ∃ p, Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

Tactic:
have hl :=
      ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')

Goal state after:
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
hl : f.length (s i) < f.length (s i) + ↑(ε' i)
⊢ ∃ p, Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ AEStronglyMeasurable.mk f hf =ᵐ[μ.restrict t] 0

Tactic:
EventuallyEq,

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f hf x = 0 x
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s

Tactic:
simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

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

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s

Tactic:
apply norm_setIntegral_le_of_norm_le_const_ae hs
    have A : ∀ᵐ x : X ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C := by
      filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
      rw [← h2 h3]
      exact h1 h3
    have B : MeasurableSet {x | ‖hfm.mk f x‖ ≤ C} :=
      hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic
    filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _
    rwa [h1]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ re ⟪x, x⟫ = √(re ⟪x, x⟫ * re ⟪x, x⟫)

Tactic:
sqrt_mul_self inner_self_nonneg

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ re ⟪x, x⟫ = re ⟪x, x⟫
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Tactic:
have : Continuous eval :=
    ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫ = √(re ⟪x, x⟫ * re ⟪x, x⟫)

Tactic:
sqrt_mul_self inner_self_nonneg

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫ = re ⟪x, x⟫