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

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

Tactic:
ENNReal.rpow_one

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : p = 1
⊢ ∫⁻ (a : α), (f + g) a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf : liminf (fun n ↦ eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n ↦ eLpNorm' (f n) p μ ^ p) atTop
⊢ liminf (fun i ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop = liminf (fun n ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ 1) atTop

Tactic:
ENNReal.rpow_one

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
w : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i ↦ ↑(w i)) i * f i ≤
    (∑ i ∈ s, (fun i ↦ ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i ↦ ↑(w i)) i * f i ^ p) ^ p⁻¹

Tactic:
lift f to ι → ℝ≥0 using hf

Goal state after:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i ↦ ↑(w i)) i * (fun i ↦ ↑(f i)) i ≤
    (∑ i ∈ s, (fun i ↦ ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i ↦ ↑(w i)) i * (fun i ↦ ↑(f i)) i ^ p) ^ p⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
⊢ (Summable fun i ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
lift f to ι → ℝ≥0 using hf

Goal state after:
ι : Type u
g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i ↦ g i ^ q
f : ι → ℝ≥0
hf_sum : Summable fun i ↦ (fun i ↦ ↑(f i)) i ^ p
⊢ (Summable fun i ↦ ((fun i ↦ ↑(f i)) i * g i) ^ r) ∧
    ∑' (i : ι), ((fun i ↦ ↑(f i)) i * g i) ^ r ≤
      (∑' (i : ι), (fun i ↦ ↑(f i)) i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg_sum : HasSum (fun i ↦ g i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i ↦ f i * g i) C

Tactic:
lift f to ι → ℝ≥0 using hf

Goal state after:
ι : Type u
g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : HasSum (fun i ↦ g i ^ q) (B ^ q)
f : ι → ℝ≥0
hf_sum : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i ↦ (fun i ↦ ↑(f i)) i * g i) C
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ p
⊢ (Summable fun i ↦ (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
lift f to ι → ℝ≥0 using hf

Goal state after:
ι : Type u
g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i ↦ g i ^ p
f : ι → ℝ≥0
hf_sum : Summable fun i ↦ (fun i ↦ ↑(f i)) i ^ p
⊢ (Summable fun i ↦ ((fun i ↦ ↑(f i)) i + g i) ^ p) ∧
    (∑' (i : ι), ((fun i ↦ ↑(f i)) i + g i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i ↦ ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hfA : HasSum (fun i ↦ f i ^ p) (A ^ p)
hgB : HasSum (fun i ↦ g i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i ↦ (f i + g i) ^ p) (C ^ p)

Tactic:
lift f to ι → ℝ≥0 using hf

Goal state after:
ι : Type u
g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hgB : HasSum (fun i ↦ g i ^ p) (B ^ p)
f : ι → ℝ≥0
hfA : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i ↦ ((fun i ↦ ↑(f i)) i + g i) ^ p) (C ^ p)
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
hfg : TendstoInMeasure μ f atTop g
n k : ℕ
hn : seqTendstoAeSeq hfg n ≤ k
⊢ μ {x | 2⁻¹ ^ n ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ n

Tactic:
by
  cases n
  · exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn
  · exact Classical.choose_spec
      (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)

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

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
a : α
ha1 : ↑↑(hg.compLp g0 f) a = (g ∘ ↑↑f) a
⊢ ↑↑(hg.compLp g0 f') a = (g ∘ ↑↑f') a →
    ↑↑(hg.compLp g0 f - hg.compLp g0 f') a = (↑↑(hg.compLp g0 f) - ↑↑(hg.compLp g0 f')) a →
      ↑↑(f - f') a = (↑↑f - ↑↑f') a → ‖↑↑(hg.compLp g0 f - hg.compLp g0 f') a‖ ≤ ↑c * ‖↑↑(f - f') a‖

Tactic:
ha2

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
a : α
ha1 : ↑↑(hg.compLp g0 f) a = (g ∘ ↑↑f) a
ha2 : ↑↑(hg.compLp g0 f') a = (g ∘ ↑↑f') a
⊢ ↑↑(hg.compLp g0 f - hg.compLp g0 f') a = (↑↑(hg.compLp g0 f) - ↑↑(hg.compLp g0 f')) a →
    ↑↑(f - f') a = (↑↑f - ↑↑f') a → ‖↑↑(hg.compLp g0 f - hg.compLp g0 f') a‖ ≤ ↑c * ‖↑↑(f - f') a‖
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
g✝ : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
a : α
ha1 : ↑↑(f + g) a = (↑↑f + ↑↑g) a
⊢ ↑↑(L.compLp (f + g)) a = L (↑↑(f + g) a) →
    ↑↑(L.compLp f) a = L (↑↑f a) →
      ↑↑(L.compLp g) a = L (↑↑g a) →
        ↑↑(L.compLp f + L.compLp g) a = (↑↑(L.compLp f) + ↑↑(L.compLp g)) a →
          ↑↑(L.compLp (f + g)) a = ↑↑(L.compLp f + L.compLp g) a

Tactic:
ha2

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
g✝ : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
a : α
ha1 : ↑↑(f + g) a = (↑↑f + ↑↑g) a
ha2 : ↑↑(L.compLp (f + g)) a = L (↑↑(f + g) a)
⊢ ↑↑(L.compLp f) a = L (↑↑f a) →
    ↑↑(L.compLp g) a = L (↑↑g a) →
      ↑↑(L.compLp f + L.compLp g) a = (↑↑(L.compLp f) + ↑↑(L.compLp g)) a →
        ↑↑(L.compLp (f + g)) a = ↑↑(L.compLp f + L.compLp g) a
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
g : E → F
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
a✝ : α
ha1 : ↑↑(c • f) a✝ = (c • ↑↑f) a✝
⊢ ↑↑(L.compLp (c • f)) a✝ = L (↑↑(c • f) a✝) →
    ↑↑(σ c • L.compLp f) a✝ = (σ c • ↑↑(L.compLp f)) a✝ →
      ↑↑(L.compLp f) a✝ = L (↑↑f a✝) → ↑↑(L.compLp (c • f)) a✝ = ↑↑(σ c • L.compLp f) a✝

Tactic:
ha2

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
g : E → F
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
a✝ : α
ha1 : ↑↑(c • f) a✝ = (c • ↑↑f) a✝
ha2 : ↑↑(L.compLp (c • f)) a✝ = L (↑↑(c • f) a✝)
⊢ ↑↑(σ c • L.compLp f) a✝ = (σ c • ↑↑(L.compLp f)) a✝ →
    ↑↑(L.compLp f) a✝ = L (↑↑f a✝) → ↑↑(L.compLp (c • f)) a✝ = ↑↑(σ c • L.compLp f) a✝
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 : ∀ (n : ℕ), eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
h2 : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
h3 : (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
h4 : ∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ < ∞
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i ↦ f (i + 1) x - f i x

Tactic:
exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i ↦ f (i + 1) x - f i x
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

Tactic:
refine h_summable.mono fun x hx ↦ ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i ↦ f (i + 1) x - f i x
x : α
hx : Summable fun i ↦ f (i + 1) x - f i x
⊢ ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
x : α ⊕ β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      x =
    f x

Tactic:
cases x

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : α
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inl val✝) =
    f (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inr val✝) =
    f (Sum.inr val✝)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : 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
⊢ Absorbs 𝕜 V (⇑f '' s)

Tactic:
rw [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV),
      NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]

Goal state after:
ι : 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
⊢ ∃ i, 0 < i ∧ ∀ ⦃x : 𝕜⦄, x ∈ {y | ‖y‖ < i} → MapsTo (fun x_1 ↦ x • x_1) (⇑f '' s) V
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖

Tactic:
← norm_inv,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖x‖ = ‖(c ^ n)⁻¹‖ * ‖c ^ n • x‖
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖c ^ n‖⁻¹ * 1 ≤ ↑ε⁻¹ * ‖c‖ * ‖f x‖

Tactic:
by rwa [mul_one]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
⊢ Monotone fun C ↦ ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖

Tactic:
exact fun C₁ C₂ hC ↦ forall₂_imp fun i x ↦ le_trans' <| by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝ : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

Tactic:
rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsCompl p q
⊢ IsTopCompl p q ↔ Continuous[inst✝², instTopologicalSpaceSubtype] ⇑(p.projectionOnto q h)

Tactic:
rw [h.isTopCompl_iff, IsInducing.subtypeVal.continuous_iff]
  rfl

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

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

Tactic:
union_comm,

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

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

Tactic:
union_comm,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (t ∪ s) = μ.real s + μ.real t
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hm : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s \ t) = μ.real (s ∪ t) - μ.real t

Tactic:
union_comm,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hm : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s \ t) = μ.real (t ∪ s) - μ.real t
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : μ (s₃ \ s₁) ≠ ∞
A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

Tactic:
simp [measureReal_def, A.1, A.2]

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

Goal state before:
pp: 𝕜 : 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
h : ε < ‖ξ‖
this : ξ₀ * (ξ⁻¹ * ξ) ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ False

Tactic:
inv_mul_cancel₀ hξ0,

Goal state after:
𝕜 : 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
h : ε < ‖ξ‖
this : ξ₀ * 1 ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ False
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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
          s.piecewise_insert _ _ _

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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
⊢ ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ∞
⊢ IntegrableOn (↑↑f) s μ

Tactic:
refine memLp_one_iff_integrable.mp ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ∞
⊢ MemLp (↑↑f) 1 (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (f ∘ e) l (Measure.comap e μ)

Tactic:
← he.integrableAtFilter_map_iff,

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter f (map e l) (Measure.map e (Measure.comap e μ))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
by
  rcases hf with ⟨s, sl, hs⟩
  exact ⟨s, sl, hs.neg⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable (fun x ↦ f x • c) μ ∧ HasFiniteIntegral (fun x ↦ f x • c) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ

Tactic:
aestronglyMeasurable_smul_const_iff (f := f) hc,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ ∧ HasFiniteIntegral (fun x ↦ f x • c) μ ↔ AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ