mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case hg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun x_1 ↦ f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)

Tactic:
· rw [← isLittleO_one_iff ℝ]
    refine h.isBigO_comp.trans_isLittleO ?_
    apply IsLittleO.const_mul_left
    rw [isLittleO_norm_left, isLittleO_one_iff, ← sub_self x.2]
    exact continuous_snd.continuousAt.sub tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
have : μ (s ∪ t) ≠ ∞ :=
    ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨h₁.lt_top, h₂.lt_top⟩ )).ne

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
h : IntegrableOn f s μ
⊢ IntegrableOn f s (μ.restrict t)

Tactic:
dsimp only [IntegrableOn] at h ⊢
  exact h.mono_measure <| Measure.restrict_mono_measure Measure.restrict_le_self _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ∫⁻ (a : α), ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a‖ₑ ∂μ = ∫⁻ (a : α), ((fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ) a ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ (fun a ↦ ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a‖ₑ) =ᵐ[μ] (fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
⊢ ∀ (x : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))),
    ‖{ toFun := fun u ↦ MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯, map_add' := ⋯, map_smul' := ⋯ } x‖ = ‖x‖

Tactic:
intro u
    simp only [eLpNorm, LinearMap.coe_mk, AddHom.coe_mk,
      one_ne_zero, ENNReal.one_ne_top, ENNReal.toReal_one, if_false, eLpNorm', ENNReal.rpow_one,
      _root_.div_one, Lp.norm_def]
    rw [lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas.coe_nnreal_ennreal
        (Filter.Eventually.of_forall fun x => ENNReal.coe_lt_top)]
    congr 1
    apply lintegral_congr_ae
    filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp] with x hx
    rw [hx]
    simp [NNReal.smul_def, enorm_smul]

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

Goal state before:
pp: case refine_1
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
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) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
⊢ ∀ u_1 ∈ u '' T, IsOpen[inst✝³] u_1

Tactic:
rintro v ⟨w, -, rfl⟩

Goal state after:
case refine_1
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
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) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : ↑s
⊢ IsOpen[inst✝³] (u w)
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : ¬c = 0
⊢ IsClosedMap fun x ↦ x • c

Tactic:
exact (isClosedEmbedding_smul_left hc).isClosedMap

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

Goal state before:
pp: case refine_2
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) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
⊢ ∀ u_1 ∈ u '' T, IntegrableOn f (u_1 ∩ s) μ

Tactic:
rintro v ⟨w, -, rfl⟩

Goal state after:
case refine_2
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) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : ↑s
⊢ IntegrableOn f (u w ∩ s) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun i ↦ f i)
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)

Tactic:
finprod_def'

Goal state after:
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down) then
          ∏ i ∈ Finite.toFinset h, L.support.mulIndicator (fun i ↦ f i) i.down
        else 1
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun i ↦ f i)
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)
    μ

Tactic:
finprod_def'

Goal state after:
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down) then
          ∏ i ∈ Finite.toFinset h, L.support.mulIndicator (fun i ↦ f i) i.down
        else 1
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)
    μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : T2Space F
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
⊢ FiniteDimensional 𝕜 (E ⧸ (↑f).ker)

Tactic:
exact f.toLinearMap.quotKerEquivRange.symm.finiteDimensional

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (fun a ↦ edist (↑↑(f - g) a) 0) =ᵐ[μ] fun a ↦ edist (↑↑f a - ↑↑g a) 0
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
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
⊢ LocallyIntegrable f μ

Tactic:
intro x
  rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩
  have : Fact (μ U < ⊤) := ⟨h'U⟩
  refine ⟨U, hU, ?_⟩
  rw [IntegrableOn, ← memLp_one_iff_integrable]
  apply (hf.restrict U).mono_exponent hp

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

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
by
  by_cases hp_zero : p = 0
  · simpa only [hp_zero, eLpNorm_exponent_zero] using tendsto_const_nhds
  have hp : 0 < p.toReal := toReal_pos hp_zero hp_ne_top
  suffices Tendsto (fun n => ∫⁻ x, ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0) by
    simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_ne_top]
    convert! continuous_rpow_const.continuousAt.tendsto.comp this
    simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]
  -- We simply check the conditions of the Dominated Convergence Theorem:
  -- (1) The function "`p`-th power of distance between `f` and the approximation" is measurable
  have hF_meas n : Measurable fun x => ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal := by
    simpa only [← edist_eq_enorm_sub] using
      (approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
        (measurable_edist_right.comp hf).pow_const p.toReal
  -- (2) The functions "`p`-th power of distance between `f` and the approximation" are uniformly
  -- bounded, at any given point, by `fun x => ‖f x - y₀‖ ^ p.toReal`
  have h_bound n :
    (fun x ↦ ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] (‖f · - y₀‖ₑ ^ p.toReal) :=
    .of_forall fun x => rpow_le_rpow (coe_mono (nnnorm_approxOn_le hf h₀ x n)) toReal_nonneg
  -- (3) The bounding function `fun x => ‖f x - y₀‖ ^ p.toReal` has finite integral
  have h_fin : (∫⁻ a : β, ‖f a - y₀‖ₑ ^ p.toReal ∂μ) ≠ ⊤ :=
    (lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_ne_top hi).ne
  -- (4) The functions "`p`-th power of distance between `f` and the approximation" tend pointwise
  -- to zero
  have h_lim :
    ∀ᵐ a : β ∂μ, Tendsto (‖approxOn f hf s y₀ h₀ · a - f a‖ₑ ^ p.toReal) atTop (𝓝 0) := by
    filter_upwards [hμ] with a ha
    have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
      (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
    convert! continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
    simp [zero_rpow_of_pos hp]
  -- Then we apply the Dominated Convergence Theorem
  simpa using tendsto_lintegral_of_dominated_convergence _ hF_meas h_bound h_fin h_lim

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

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst✝ : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
f' : β → E := ⋯
⊢ ∃ g, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp (⇑g) p μ

Tactic:
have hf' : MemLp f' p μ := hf.ae_eq hf.1.ae_eq_mk

Goal state after:
β : Type u_2
inst✝¹ : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst✝ : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
⊢ ∃ g, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp (⇑g) p μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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

Tactic:
exact fun i hi => hps i (Finset.mem_insert_of_mem hi)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : Eₗ
h_mem : ∀ x ∈ e.range, ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖
⊢ ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

Tactic:
exact h_dense.induction h_mem (isClosed_le (by fun_prop) (by fun_prop)) x

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
x : α
⊢ 0 x ≤ (SimpleFunc.map ({x | 0 ≤ x}.piecewise id 0) g) x

Tactic:
simpa using! Set.indicator_apply_nonneg id

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • (ENNReal.toReal ∘ g) x = ((map g f).lintegral μ).toReal

pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ (ENNReal.toReal ∘ g) 0 = 0

Tactic:
map_lintegral,

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • (ENNReal.toReal ∘ g) x = (∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})).toReal

α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ (ENNReal.toReal ∘ g) 0 = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case hμ
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := ⋯
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := ⋯
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
⊢ ∀ᵐ (x : α) ∂μ,
    ↑↑↑g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})

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

Tactic:
· have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
      refine hg_nonneg.mono fun a ha => subset_closure ?_
      simpa using ha

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

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

Tactic:
smul_sum

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x = c • ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x

Tactic:
smul_sum

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, c • (T (⇑f ⁻¹' {x})) x
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 : α → G
h : f =ᵐ[μ] g
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ

Tactic:
by
  simp only [integral_eq_setToFun]
  exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ‖↑↑(Lp.posPart f₁) a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := ⋯
⊢ (fun a ↦ ENNReal.ofReal (f a)) =ᵐ[μ] fun a ↦ ‖↑↑(Lp.posPart f₁) a‖ₑ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = ∫⁻ (a : α), ‖↑↑(Lp.negPart f₁) a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := ⋯
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ (fun a ↦ ENNReal.ofReal (-f a)) =ᵐ[μ] fun a ↦ ‖↑↑(Lp.negPart f₁) a‖ₑ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : ClosedIciTopology E
f : α → E
hf : f ≤ᵐ[μ] 0
⊢ ∫ (x : α), f x ∂μ ≤ 0

Tactic:
by
  rw [← neg_nonneg, ← integral_neg]
  refine integral_nonneg_of_ae ?_
  filter_upwards [hf] with x hx
  simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'

Tactic:
by
  simp only [edist_nndist]
  norm_cast
  apply dist_vadd_vadd_le

Goal state after: