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 T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T f = setToSimpleFunc T' f

Tactic:
by
  simp_rw [setToSimpleFunc]
  refine sum_congr rfl fun x _ => ?_
  by_cases hx0 : x = 0
  · simp [hx0]
  · rw [h (f ⁻¹' {x}) (SimpleFunc.measurableSet_fiber _ _)
        (SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hx0)]

Goal state after:
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
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
by
      rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]; rw [smul_zero]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
by
      rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]; rw [smul_zero]

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 α
f : α → G
⊢ ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ

Tactic:
by
  simp only [integral_eq_setToFun]
  exact setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f

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

Goal state before:
pp: α : Type u_1
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
by
  refine sum_nonneg fun i hi => hT_nonneg _ i ?_
  rw [mem_range] at hi
  obtain ⟨y, hy⟩ := Set.mem_range.mp hi
  rw [← hy]
  refine le_trans ?_ (hf y)
  simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
refine sum_nonneg fun i hi => ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ f.range
⊢ 0 ≤ (T (⇑f ⁻¹' {i})) i
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ (0 ⁻¹' {x}) = s

Tactic:
← Function.const_zero,

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ (Function.const α 0 ⁻¹' {x}) = s
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

Tactic:
have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
    rw [h_univ_empty, hT_empty]
    simp only [setToSimpleFunc, zero_apply, sum_empty,
      range_eq_empty_of_isEmpty]

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

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

Tactic:
convert! h.fun_add (EventuallyEq.refl l v) <;> simp [add_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
⊢ ∀ᶠ (x : α) in l, v x = 0 → u x = 0

Tactic:
by_contra! h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0
⊢ False
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((fun x ↦ (φ x)⁻¹) * v⁻¹) x✝ = ((φ * v) x✝)⁻¹

Tactic:
simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst✝ : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 ≤ v t
⊢ ∀ᶠ (x : α) in l, 0 ≤ u x

Tactic:
obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul
  exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_nonneg hφ.le hv)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x ↦ ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)

Tactic:
by
  simp_rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun x => (f x).coe_nonneg)
      hfi.aestronglyMeasurable, ← ENNReal.coe_nnreal_eq]
  rw [ENNReal.ofReal_toReal]
  simpa [← lt_top_iff_ne_top, hasFiniteIntegral_iff_enorm, NNReal.enorm_eq] using
    hfi.hasFiniteIntegral

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ∨ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∞ ↔ f =ᵐ[μ] 0

Tactic:
← ENNReal.not_lt_top,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ∨ ¬∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞ ↔ f =ᵐ[μ] 0
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_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := ⋯
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ z₁ ∈ sphere 0 r

Tactic:
rw [mem_sphere_zero_iff_norm]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r
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_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r

Tactic:
exact norm_smul_inv_norm' r_pos.le z_zero

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:
rw [sub_sub, dist_eq_norm]

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous fun a ↦ blockDiagonal' (A a) ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Tactic:
dsimp only [blockDiagonal'_apply']
    split_ifs with h
    · subst h
      exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂
    · exact continuous_const

Goal state after:
Module: Mathlib.Topology.Algebra.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ x ∈ interior (interior s)

Tactic:
by rwa [interior_interior]

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
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ μ
f : β → G
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → G := AEStronglyMeasurable.mk f hfm
⊢ ∫ (y : β), g y ∂Measure.map φ μ = ∫ (y : β), g y ∂Measure.map (AEMeasurable.mk φ hφ) μ

Tactic:
by congr 1; exact Measure.map_congr hφ.ae_eq_mk

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : PartialOrder G''
inst✝² : IsOrderedAddMonoid G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α → E
hG'' : ¬CompleteSpace G''
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

pp: case pos
α : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : PartialOrder G''
inst✝² : IsOrderedAddMonoid G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α → E
hG'' : CompleteSpace G''
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
· simp [setToFun, hG'']

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : PartialOrder G''
inst✝² : IsOrderedAddMonoid G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α → E
hG'' : CompleteSpace G''
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
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
w : dist f g < C
x : α
⊢ dist (f x) (g x) < C

Tactic:
exact lt_of_le_of_lt (dist_coe_le_dist x) w

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᵐ[μ] f
hG'' : ¬CompleteSpace G''
⊢ 0 ≤ setToFun μ T hT f

pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᵐ[μ] f
hG'' : CompleteSpace G''
⊢ 0 ≤ setToFun μ T hT f

Tactic:
· simp [setToFun, hG'']

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᵐ[μ] f
hG'' : CompleteSpace G''
⊢ 0 ≤ setToFun μ T hT f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ∞
this : Fact (μ {x | ε ≤ f x} < ∞)
⊢ ε * μ.real {x | ε ≤ f x} = ∫ (x : α) in {x | ε ≤ f x}, ε ∂μ

Tactic:
simp [mul_comm]

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (g₁ x) (g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ⇑f)ᶜ
⊢ dist (h₁ ↑x) (h₂ ↑x) = dist ((extend f g₁ h₁) ↑x) ((extend f g₂ h₂) ↑x)

Tactic:
extend_apply' x.coe_prop,

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ⇑f)ᶜ
⊢ dist (h₁ ↑x) (h₂ ↑x) = dist (h₁ ↑x) ((extend f g₂ h₂) ↑x)
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:
by rw [v.sum_equivFun]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
    rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ interior K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x

Tactic:
apply thickenedIndicatorAux_mono hle

Goal state after:
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hF : CompleteSpace F
⊢ ‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
exact L1.norm_setToL1_le_mul_norm' hT _

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 α
f : α → β
a : α
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
have A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot := by
    refine inf_neBot_iff.mpr (fun s hs s' hs' ↦ ?_)
    refine ⟨f a, mem_of_mem_nhds hs, ?_⟩
    simp only [mem_map] at hs'
    apply mem_of_mem_nhdsWithin self_mem_Iic hs'
  rcases eq_or_neBot (𝓝[<] a) with h' | h'
  · simp only [MapClusterPt, ClusterPt, h', leftLim_eq_of_eq_bot, A]
  by_cases! H : ¬ ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
  · simp [MapClusterPt, ClusterPt, H, leftLim_eq_of_not_tendsto, A]
  have : MapClusterPt (f.leftLim a) (𝓝[<] a) f := (tendsto_leftLim_of_tendsto H).mapClusterPt
  exact MapClusterPt.mono this (nhdsWithin_mono _ Iio_subset_Iic_self)

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✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
⊢ leftLim (rightLim f) a = leftLim f a

Tactic:
obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))
  apply leftLim_eq_of_tendsto
  apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2
  rintro s ⟨s_mem, s_closed⟩
  obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by
    have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
    simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this
  filter_upwards [Ioo_mem_nhdsLT au] with c hc
  rcases eq_or_neBot (𝓝[>] c) with h'c | h'c
  · simpa [h'c, rightLim_eq_of_eq_bot] using hu hc
  by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
  · simpa [rightLim_eq_of_not_tendsto _ h''c] using hu hc
  apply s_closed.mem_of_tendsto (tendsto_rightLim_of_tendsto h''c)
  filter_upwards [Ioo_mem_nhdsGT_of_mem ⟨hc.1.le, hc.2⟩] with d hd using hu hd

Goal state after:
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
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter, AEStronglyMeasurable (fun a ↦ ∑ i ∈ n, F i a) μ

Tactic:
exact Eventually.of_forall fun s => s.aestronglyMeasurable_fun_sum fun n _ => hF_meas n

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

Goal state before:
pp: case pos
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
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ (let __OuterMeasure := f.outer;
      { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ })
      {a} ≤
    ⊥

Tactic:
apply (outer_le_length _ _).trans

Goal state after:
case pos
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
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ f.length {a} ≤ ⊥
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inl
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
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this : Nonempty R
val✝ : OrderBot R
⊢ f.measure (Iic x) = ofReal (↑f x - l)

Tactic:
have : Iic x = Icc ⊥ x := by simp
    rw [atBot_eq_pure_of_isBot isBot_bot] at hf
    rw [this, measure_Icc, leftLim_eq_of_isBot isBot_bot,
      tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)]

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₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ prehaar (↑K₀) U K ≤ ↑(index ↑K ↑K₀)

Tactic:
unfold prehaar

Goal state after:
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
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)