mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
refine
    ae_lt_top (.liminf fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
      (lt_of_le_of_lt
          (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
          (lt_of_le_of_lt ?_ (by finiteness : (R : ℝ≥0∞) ^ p.toReal < ∞))).ne

Goal state after:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ liminf (fun i ↦ ∫⁻ (a : α), ↑‖f i a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
· exact rpow_def_of_pos hz _

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
rw [one_div, ← @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1])]
  rw [inv_inv]
  exact add_rpow_le_rpow_add _ _ hp1

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

Tactic:
rw [(geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz).mpr ?_] at h

Goal state after:
case mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∑ i ∈ s, w i * z i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ 2 ^ (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), 2 ^ (p - 1) * g a ^ p ∂μ < ∞

pp: case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ AEMeasurable (fun a ↦ 2 ^ (p - 1) * f a ^ p) μ

Tactic:
lintegral_const_mul' _ _ (by finiteness),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ 2 ^ (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ + 2 ^ (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞

case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ AEMeasurable (fun a ↦ 2 ^ (p - 1) * f a ^ p) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ

Tactic:
by
  have h_le_μ := eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp0_lt hpq hf
  rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
⊢ MemLp f p μ

Tactic:
have : (toMeasurable μ s).indicator f = f := by
    apply Set.indicator_eq_self.2
    apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_
    contrapose hx
    exact subset_toMeasurable μ s hx

Goal state after:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p

Tactic:
refine fun y => mul_div_cancel_left_of_imp fun h => ?_

Goal state after:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
y : ℝ≥0
h : y = 0
⊢ y ^ p = 0
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

Tactic:
by_cases x ∈ s

Goal state after:
case pos
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∈ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

case neg
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∉ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
⊢ g x = g' x → {x | ε ≤ edist (f' i x) (g' x)} x = {x | ε ≤ edist (f i x) (g x)} x

Tactic:
hxg

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ edist (f' i x) (g' x)} x = {x | ε ≤ edist (f i x) (g x)} x
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_6
s : Finset ι
f : ι → ↥(Lp E p μ)
⊢ ↑↑(∑ i ∈ s, f i) =ᵐ[μ] fun x ↦ ∑ i ∈ s, ↑↑(f i) x

Tactic:
grw [coeFn_finsetSum]
  filter_upwards with x using by simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ edist (MemLp.toLp f hf) (MemLp.toLp g hg) = eLpNorm (f - g) p μ

Tactic:
rw [edist_def]
  exact eLpNorm_congr_ae (hf.coeFn_toLp.sub hg.coeFn_toLp)

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}ᶜ

Tactic:
Set.mem_compl_iff,

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ x ∉ {x | ε ≤ edist (f n x) (g x)}
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
⊢ g x = AEStronglyMeasurable.mk g hg x →
    Tendsto (fun n ↦ f n x) atTop (𝓝 (g x)) →
      Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))

Tactic:
hxg

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
⊢ Tendsto (fun n ↦ f n x) atTop (𝓝 (g x)) →
    Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ↑((∑ i ∈ s, ((f i).toNNReal + (g i).toNNReal) ^ p) ^ (1 / p)) ≤
    ↑((∑ i ∈ s, (f i).toNNReal ^ p) ^ (1 / p) + (∑ i ∈ s, (g i).toNNReal ^ p) ^ (1 / p))
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
push_cast [ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this

Goal state after:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  (∑ i ∈ s, (↑(f i).toNNReal + ↑(g i).toNNReal) ^ p) ^ (1 / p) ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ (1 / p) + (∑ x ∈ s, ↑(g x).toNNReal ^ p) ^ (1 / p)
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : ↑↑|f| x ≤ ↑↑|g| x
hxf : ↑↑|f| x = |↑↑f x|
⊢ ↑↑|g| x = |↑↑g x| → ‖↑↑f x‖ ≤ ‖↑↑g x‖

Tactic:
hxg

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : ↑↑|f| x ≤ ↑↑|g| x
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : |↑↑f x| ≤ ↑↑|g| x
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖

Tactic:
hxg

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : |↑↑f x| ≤ |↑↑g x|
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case inr
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
hne : i ≠ i₀
⊢ update y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i

Tactic:
simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ ↑(Units.oneSub (-(↑x⁻¹ * t)) ⋯)⁻¹ * ↑x⁻¹ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
← inverse_unit,

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (↑(Units.oneSub (-(↑x⁻¹ * t)) ⋯))⁻¹ʳ * ↑x⁻¹ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n ↦ t ^ n
⊢ ∑ i ∈ range n, t ^ i + ∑' (i : ℕ), t ^ (i + n) = ∑ i ∈ range n, t ^ i + t ^ n * (1 - t)⁻¹ʳ

Tactic:
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n ↦ t ^ n
⊢ ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
⊢ Tendsto (fun x_1 ↦ ‖x_1 - ↑x‖) (𝓝 ↑x) (𝓝 0)

Tactic:
exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
hcont : Continuous[Pi.topologicalSpace, inst✝] ((toFun {s | IsVonNBounded 𝕜 s}) f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
      (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) = c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)
⊢ f ∈ range toUniformOnFun

Tactic:
exact ⟨⟨⟨f, by intro; convert! hadd, by intro; convert! hsmul⟩, hcont⟩, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing g.compContinuousMultilinearMap

Tactic:
← isUniformInducing_toUniformOnFun.of_comp_iff

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing (toUniformOnFun ∘ g.compContinuousMultilinearMap)
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : 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
this : Tendsto (fun y ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0))
⊢ Tendsto (fun x_1 ↦ f x_1 - f x) (𝓝 x) (𝓝 0)

Tactic:
by
    simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ Integrable f 0

Tactic:
constructor <;> fun_prop

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:
add_comm,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable (f + g) μ ↔ Integrable g μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ Integrable (fun x ↦ ‖f x‖ₑ) μ

Tactic:
constructor <;> fun_prop

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 : α → β
hf : Integrable f μ
⊢ Integrable (fun a ↦ ‖f a‖) μ

Tactic:
constructor <;> fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
R : Type u_8
inst✝² : NormedRing R
inst✝¹ : Module R β
inst✝ : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x ↦ ‖g x‖ₑ) μ ≠ ∞
⊢ MemLp (fun x ↦ g x • f x) 1 μ

Tactic:
refine ⟨g_aestronglyMeasurable.smul hf.1, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
R : Type u_8
inst✝² : NormedRing R
inst✝¹ : Module R β
inst✝ : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x ↦ ‖g x‖ₑ) μ ≠ ∞
⊢ eLpNorm (fun x ↦ g x • f x) 1 μ < ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
by
  rcases exists_seq_strictAnti_tendsto' ENNReal.zero_lt_top with ⟨u, _, u_pos, u_lim⟩
  let v n := toMeasurable (μ.restrict s) { x | u n ≤ ‖f x‖ₑ }
  have A : ∀ n, μ (s ∩ v n) ≠ ∞ := by
    intro n
    rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
      measure_toMeasurable]
    exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne
  apply Measure.restrict_toMeasurable_of_cover _ A
  intro x hx
  obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖ₑ :=
    ((tendsto_order.1 u_lim).2 _ (pos_of_ne_zero (h's x hx))).exists
  exact mem_iUnion.2 ⟨n, subset_toMeasurable _ _ hn.le⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
⊢ μ {x | ε < ‖f x‖ₑ} < ∞

Tactic:
by_cases hε' : ε = ∞
  · simp [hε']
  exact lt_of_le_of_lt (measure_mono (fun _ h ↦ (Set.mem_ofPred_eq ▸ h).le))
    (hf.measure_enorm_ge_lt_top hε hε')

Goal state after: