mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
⊢ ξ ∈ Metric.closedBall 0 ε

Tactic:
rw [mem_closedBall_zero_iff]
      -- Now suppose `ξ ≠ 0`. By contradiction, let's assume `ε < ‖ξ‖`, and show that
      -- `ξ₀ ∈ 𝓑 ⊆ {ξ₀}ᶜ`, which is a contradiction.
      by_contra! h
      suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ by
        rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this
        exact notMem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this)
      -- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`,
      -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.
      refine (balancedCore_balanced _).smul_mem ?_ hξ
      rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr hξ0), one_mul]
      exact (hξ₀ε.trans h).le

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

Tactic:
by_cases H : finrank 𝕜 (LinearMap.range l) = 0

Goal state after:
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : finrank 𝕜 ↥l.range = 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g ν
⊢ Integrable (g ∘ f) μ ↔ Integrable g ν

Tactic:
rw [← hf.map_eq] at hg ⊢

Goal state after:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g (Measure.map f μ)
⊢ Integrable (g ∘ f) μ ↔ Integrable g (Measure.map f μ)
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : finrank 𝕜 ↥l.range = 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

Tactic:
rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
    rw [H]
    exact continuous_zero

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : s.Finite
f : α → E
⊢ IntegrableOn f s μ

Tactic:
simpa using IntegrableOn.finset (s := hs.toFinset)

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable (g + f) μ ↔ Integrable g μ

Tactic:
rw [add_comm, integrable_add_iff_integrable_right hf]

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
⊢ Function.Injective ⇑(l.ker.liftQ l ⋯)

Tactic:
← LinearMap.ker_eq_bot

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
⊢ (l.ker.liftQ l ⋯).ker = ⊥
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᵐ[μ] 0
hg : g ≤ᵐ[μ] 0
⊢ Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ

Tactic:
exact integrable_add_iff_of_nonneg h_meas.neg (hf.mono (fun _ ↦ neg_nonneg_of_nonpos))
    (hg.mono (fun _ ↦ neg_nonneg_of_nonpos))

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
by
  rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_coe_smul₀]
  · congr!
  · exact hf.ennreal_toNNReal

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x ↦ f default) =ᵐ[μ.restrict s] f
t : Set β
ht : IsOpen[inst✝¹] t
u : Set α
u_open : IsOpen[inst✝⁴] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s ∪ (fun x ↦ f default) ⁻¹' t \ s)

Tactic:
exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
by
  let := pseudoMetrizableSpacePseudoMetric α
  borelize β
  rw [aestronglyMeasurable_iff_aemeasurable_separable]
  refine ⟨hf.aemeasurable hs, f '' s, hf.isSeparable_image h's, ?_⟩
  exact mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G
⊢ ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖

Tactic:
neg_add,

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G
⊢ ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x✝ : G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E x✝) x‖ ≤ ‖x✝‖ * ∏ i, ‖x i‖

Tactic:
rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]

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

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : μ {a} ≠ ∞
ha' : ‖f a‖ₑ ≠ ∞
hab : a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

pp: case neg
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : μ {a} ≠ ∞
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
· rw [← Ioo_union_left hab, integrableOn_union,
      eq_true (integrableOn_singleton ha'), and_true]

Goal state after:
case neg
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : μ {a} ≠ ∞
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: 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 μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen[inst✝³] (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ x, u x
T : Set ↑s
hT_count : T.Countable
hT_un : ⋃ i ∈ T, u i = ⋃ i, u i
⊢ s ⊆ ⋃ i ∈ T, u i

Tactic:
rwa [hT_un]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x
x : X
hx : x ∈ conv
⊢ (l.limUnder fun x_1 ↦ f x_1 x) = Function.extend Subtype.val (fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x) (fun x ↦ e) x

Tactic:
Function.extend_val_apply hx

Goal state after:
case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x
x : X
hx : x ∈ conv
⊢ (l.limUnder fun x_1 ↦ f x_1 x) = l.limUnder fun x_1 ↦ f x_1 ↑⟨x, hx⟩
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 x

Tactic:
by
  obtain rfl | hl := eq_or_neBot l
  · simpa [limUnder, Filter.map_bot] using stronglyMeasurable_const
  let e := Classical.choice hE
  let conv := {x | ∃ c, Tendsto (f · x) l (𝓝 c)}
  have mconv : MeasurableSet conv := StronglyMeasurable.measurableSet_exists_tendsto hf
  have hconv : StronglyMeasurable (fun x : conv ↦ limUnder l (f · x)) := by
    refine stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_
    refine tendsto_pi_nhds.2 fun x ↦ ?_
    obtain ⟨c, hc⟩ := x.2
    rwa [hc.limUnder_eq]
  have : (fun x ↦ limUnder l (f · x)) = ((↑) : conv → X).extend
      (fun x ↦ limUnder l (f · x)) (fun _ ↦ e) := by
    ext x
    by_cases hx : x ∈ conv
    · rw [Function.extend_val_apply hx]
    · rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
  rw [this]
  exact (MeasurableEmbedding.subtype_coe mconv).stronglyMeasurable_extend hconv
    stronglyMeasurable_const

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional 𝕜 ↥M := Finite.span_of_finite 𝕜 hF_finite
h_cover : U ⊆ ↑M + c • U
n : ℕ
⊢ U ⊆ ↑M + c ^ n • U

Tactic:
induction n with
    | zero => simpa using! fun x hx ↦ ⟨0, M.zero_mem, x, hx, zero_add x⟩
    | succ n ih =>
      calc
        U ⊆ M + c ^ n • U := ih
        _ ⊆ M + c ^ n • (M + c • U) := by gcongr
        _ ⊆ M + c ^ (n + 1) • U := by
          rw [smul_add, smul_smul, pow_succ, ← add_assoc]
          congr!
          lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
          simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α →ₘ[μ] ε
⊢ MeasureTheory.Integrable (↑f) μ ↔ f.Integrable

Tactic:
by
  rw [← integrable_mk f.aestronglyMeasurable, mk_coeFn]

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

Goal state before:
pp: case mpr
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iio a) μ

Tactic:
refine (integrableOn_union.mpr ⟨?_, hs.mono hs' le_rfl⟩).mono Iio_subset_Iic_union_Ioo le_rfl

Goal state after:
case mpr
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iic s') μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : μ s ≠ ∞
this : Fact (μ s < ∞)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.restrict s, ‖f a‖ ≤ C

Tactic:
filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))

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

Goal state before:
pp: X : Type u_1
R : Type u_8
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn (fun x ↦ g x * f x) s μ

Tactic:
by
  rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
  exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_mul (hg.mono hk_sub) hk_c

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (x + y) • f = x • f + y • f

Tactic:
ext1; exact add_smul _ _ _

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

Goal state before:
pp: case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C ≤ max C C'

pp: case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C' ≤ max C C'

Tactic:
· exact le_max_left C C'

Goal state after:
case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C' ≤ max C C'
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) μ
h : Pairwise fun x y ↦ T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
⊢ setToSimpleFunc T (map Prod.fst (f.pair g)) = setToSimpleFunc T (map Prod.snd (f.pair g))

Tactic:
map_setToSimpleFunc T h_add h_pair Prod.fst_zero

Goal state after:
α : 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) μ
h : Pairwise fun x y ↦ T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 = setToSimpleFunc T (map Prod.snd (f.pair g))
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ integral (μ + ν) f = integral μ f + integral ν f

Tactic:
integral_def

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
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
f : ↥(Lp E 1 μ)
⊢ Continuous integral

Tactic:
integral_def

Goal state after:
α : 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
f : ↥(Lp E 1 μ)
⊢ Continuous ⇑integralCLM
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖

Tactic:
norm_smul

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
by_cases hf : Integrable (fun a => (f a : ℝ)) μ

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : Integrable (fun a ↦ ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a ↦ ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

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

Tactic:
rw [← hf.ge_iff_eq', Filter.EventuallyEq, Filter.EventuallyLE]
    simp only [Pi.zero_apply, ofReal_eq_zero]

Goal state after: