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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
a : α
ha_mono : Monotone fun i ↦ f i a
i : ℕ
⊢ ∀ ⦃b : ℕ⦄, i ≤ b → (fun i ↦ f' i a) i ≤ (fun i ↦ f' i a) b

Tactic:
j

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
a : α
ha_mono : Monotone fun i ↦ f i a
i j : ℕ
⊢ i ≤ j → (fun i ↦ f' i a) i ≤ (fun i ↦ f' i a) j
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ dist (f x) (f y) = dist x y

Tactic:
dist_eq_norm_vsub V₂,

Goal state after:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ ‖f x -ᵥ f y‖ = dist x y
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
a : α
ha : Antitone fun i ↦ f i a
i : ℕ
⊢ ∀ ⦃b : ℕ⦄, i ≤ b → (fun i ↦ f' i a) i ≤ (fun i ↦ f' i a) b

Tactic:
j

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
a : α
ha : Antitone fun i ↦ f i a
i j : ℕ
⊢ i ≤ j → (fun i ↦ f' i a) i ≤ (fun i ↦ f' i a) j
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ

Tactic:
simp_rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)

Tactic:
simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp1 hp2, one_div]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
⊢ EqOn f (⇑A.symm ∘ g) s

Tactic:
intro x hx
    have : A (f x) = g x := gs hx
    simp only [(· ∘ ·), ← this, A.symm_apply_apply]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : AddMonoid β
inst✝¹ : BoundedAdd β
inst✝ : ContinuousAdd β
f : α →ᵇ β
⊢ ⇑(nsmulRec 0 f) = 0 • ⇑f

Tactic:
rw [nsmulRec, zero_smul, coe_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁸ : TopologicalSpace α
inst✝⁷ : CompactSpace α
inst✝⁶ : PseudoMetricSpace β
inst✝⁵ : SeminormedAddCommGroup E
f✝ g✝ : C(α, β)
C : ℝ
R : Type u_4
inst✝⁴ : Zero R
inst✝³ : Zero β
inst✝² : PseudoMetricSpace R
inst✝¹ : SMul R β
inst✝ : IsBoundedSMul R β
r : R
f g : C(α, β)
⊢ dist (r • f) (r • g) ≤ dist r 0 * dist f g

Tactic:
by
    simpa only [← dist_mkOfCompact] using! dist_smul_pair r (mkOfCompact f) (mkOfCompact g)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : SeminormedAddCommGroup E
x y : C(α, E)
⊢ dist x y = ‖-x + y‖

Tactic:
by rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]

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

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : u =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖u n * r ^ n‖) =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n

Tactic:
by
      apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp

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₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : 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:
h_eq_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
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
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₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ' T hT' f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' f₂ + setToFun μ' T hT' g₂

Tactic:
h_eq_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
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ' T hT' f₂ + setToFun μ' T hT' g₂ = setToFun μ' T hT' f₂ + setToFun μ' T hT' g₂
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

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

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μ : IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
· have : μ Set.univ = ∞ := by
      by_contra hμ'
      exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
    rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
    · exact le_top
    · simp [hr]
    · simp

Goal state after:
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μ : 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 β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ ↦ (thickening δ E).mulIndicator f) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))

Tactic:
by
  rw [tendsto_pi_nhds]
  intro x
  rw [tendsto_congr' (mulIndicator_thickening_eventually_eq_mulIndicator_closure f E x)]
  apply tendsto_const_nhds

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : NoTopOrder α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
⊢ Tendsto (leftLim f) atTop (𝓝 b)

Tactic:
apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : NoTopOrder α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
x : α
⊢ MapClusterPt (leftLim f x) (𝓝 x) f
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val✝ : NoTopOrder α
⊢ Tendsto (rightLim f) atTop (𝓝 b)

Tactic:
apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val✝ : NoTopOrder α
x : α
⊢ MapClusterPt (rightLim f x) (𝓝 x) f
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Iotop a b ⊆ Ioc a b

Tactic:
simp only [Iotop]

Goal state after:
R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ (if IsTop b then Ioc a b else Ioo a b) ⊆ Ioc a b
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Ioo a b ⊆ Iotop a b

Tactic:
simp only [Iotop]

Goal state after:
R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Ioo a b ⊆ if IsTop b then Ioc a b else Ioo a b
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
a b : R
⊢ IsOpen[inst✝¹] (Iotop a b)

Tactic:
simp only [Iotop]

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
a b : R
⊢ IsOpen[inst✝¹] (if IsTop b then Ioc a b else Ioo a b)
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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
x : α
hx : Summable fun n ↦ ↑‖f n x‖₊
⊢ HasSum (fun n ↦ f n x) (∑' (i : ι), f i x)

Tactic:
exact hx.of_norm.hasSum

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s : Set R
hR : Nonempty R
⊢ f.length (s \ botSet) = f.length s

Tactic:
· simp [length_eq]

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

Goal state before:
pp: case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : μ.innerContent U✝ ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : μ.innerContent U✝ - ↑ε < μ U
⊢ μ.innerContent U✝ ≤ μ U + ↑ε

Tactic:
rw [← tsub_le_iff_right]

Goal state after:
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : μ.innerContent U✝ ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : μ.innerContent U✝ - ↑ε < μ U
⊢ μ.innerContent U✝ - ↑ε ≤ μ U
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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
have ht : IntegrableOn f t μ := by apply integrableOn_zero.congr_fun_ae; symm; exact ht_eq

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ ∀ (i : { i // ↑i ⊆ ↑U' ∩ U }), μ ↑i + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
rintro ⟨L, hL⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
hL : ↑L ⊆ ↑U' ∩ U
⊢ μ ↑⟨L, hL⟩ + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁴ : OrderTopology R
inst✝³ : CompactIccSpace R
inst✝² : MeasurableSpace R
inst✝¹ : BorelSpace R
inst✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : f.outer (Ioc a b) < f.length (t i) + ↑(ε' i)
⊢ f.outer (botSet ∪ Ioc a b) < f.length (t i) + ofReal ↑(ε' i)

Tactic:
calc f.outer (botSet ∪ Ioc a b)
      _ ≤ f.outer botSet + f.outer (Ioc a b) := measure_union_le _ _
      _ ≤ f.length botSet + f.outer (Ioc a b) := by gcongr; apply outer_le_length
      _ = 0 + f.outer (Ioc a b) := by
        simp only [← length_sdiff_botSet, sdiff_self, empty_sdiff, outer_Ioc, zero_add]
        simp [empty_sdiff]
      _ = f.outer (Ioc a b) := by simp
      _ < f.length (t i) + ofReal ↑(ε' i) := by simpa using h₂

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ ∀ x ∈ s, ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty → ¬((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty

Tactic:
rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h1g₂ : g₂ ∈ (fun x ↦ g₁ * x) ⁻¹' V
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h1g₃ : g₃ ∈ (fun x ↦ g₁ * x) ⁻¹' V
h2g₃ : g₃ ∈ K₂.carrier
⊢ False
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
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ 0 < index (↑K₀) U

Tactic:
exact index_pos K₀ hU

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑K₀) U

Tactic:
exact index_pos K₀ hU

Goal state after:
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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atTop atTop
x : R
⊢ f.measure (Ici x) = ∞

Tactic:
← top_le_iff,

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atTop atTop
x : R
⊢ ∞ ≤ f.measure (Ici x)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atBot atBot
x : R
this✝ : Nonempty R
val✝ : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
⊢ f.measure (Iio x) = ∞

Tactic:
← top_le_iff,

Goal state after:
case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atBot atBot
x : R
this✝ : Nonempty R
val✝ : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
⊢ ∞ ≤ f.measure (Iio 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✝⁴ : MeasurableSpace R
inst✝³ : BorelSpace R
inst✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
inst✝ : Nonempty R
hf : Tendsto (↑f) atTop atTop
inhabited_h : Inhabited R
⊢ f.measure univ = ∞

Tactic:
← top_le_iff,

Goal state after:
R : Type u_1
inst✝⁸ : LinearOrder R
inst✝⁷ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁶ : OrderTopology R
inst✝⁵ : CompactIccSpace R
inst✝⁴ : MeasurableSpace R
inst✝³ : BorelSpace R
inst✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
inst✝ : Nonempty R
hf : Tendsto (↑f) atTop atTop
inhabited_h : Inhabited R
⊢ ∞ ≤ f.measure univ
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✝⁴ : MeasurableSpace R
inst✝³ : BorelSpace R
inst✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
inst✝ : Nonempty R
hf : Tendsto (↑f) atBot atBot
inhabited_h : Inhabited R
⊢ f.measure univ = ∞

Tactic:
← top_le_iff,

Goal state after:
R : Type u_1
inst✝⁸ : LinearOrder R
inst✝⁷ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁶ : OrderTopology R
inst✝⁵ : CompactIccSpace R
inst✝⁴ : MeasurableSpace R
inst✝³ : BorelSpace R
inst✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
inst✝ : Nonempty R
hf : Tendsto (↑f) atBot atBot
inhabited_h : Inhabited R
⊢ ∞ ≤ f.measure univ
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
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}

Tactic:
unfold clPrehaar

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f ⊥
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}