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

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂0, f a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae 0) fun i ↦ (f i).toReal
⊢ (essSup f 0).toReal = essSup (fun a ↦ (f a).toReal) 0

pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun i ↦ (f i).toReal
hμ : NeZero μ
⊢ (essSup f μ).toReal = essSup (fun a ↦ (f a).toReal) μ

Tactic:
· simp [essSup, limsup, limsSup]

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun i ↦ (f i).toReal
hμ : NeZero μ
⊢ (essSup f μ).toReal = essSup (fun a ↦ (f a).toReal) μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) (univ.pi s) ≤ ∏ i, (μ i) (s i)

case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
⊢ map (fun x i ↦ f i (x i)) (Measure.pi μ) = Measure.pi fun i ↦ map (f i) (μ i)

Tactic:
have (i : ι) := (hμ i).of_map _ (hf i)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ map (fun x i ↦ f i (x i)) (Measure.pi μ) = Measure.pi fun i ↦ map (f i) (μ i)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
⊢ rexp y < (rexp z - rexp y) / (z - y)

Tactic:
have h1 : 0 < z - y := by linarith

Goal state after:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y < (rexp z - rexp y) / (z - y)
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ 1 - 1 * p⁻¹ = q⁻¹

Tactic:
simp [one_sub_inv p q]

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ
h : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
by simp [h.inv_add_inv_eq_inv]

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
by simpa using hab

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
by simpa using hab

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑p.conjExponent = (↑p).conjExponent

Tactic:
rw [NNReal.conjExponent, conjExponent]

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑p - 1)⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0
hr : r ≠ 0
h : (↑p).HolderTriple ↑q ↑r
hp : p ≠ 0
hq : q ≠ 0
⊢ p⁻¹ + q⁻¹ = r⁻¹

Tactic:
exact_mod_cast h.inv_add_inv_eq_inv

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
hp : p ≠ 0
hq : q ≠ 0
⊢ (↑p)⁻¹ + (↑q)⁻¹ = (↑r)⁻¹

Tactic:
exact_mod_cast h.inv_add_inv_eq_inv

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a : ℝ≥0∞
ha : 1 ≤ a
⊢ a.HolderConjugate (1 - a⁻¹)⁻¹

Tactic:
by
  simpa using inv_one_sub_inv (ENNReal.inv_le_one.mpr ha)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a ↦ ‖f a‖ₑ ^ q) =ᵐ[μ] 0 ∧ 0 < q
x : α
hx : f x = 0 ∧ 0 < q
⊢ f x = 0 x

Tactic:
simp [hx.1]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

Tactic:
prod_eq_zero his

Goal state after:
case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ≤ ∑ i ∈ s, w i * z i

case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p

Tactic:
← mul_one ((a + b) ^ p)

Goal state after:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
prod_eq_zero his

Goal state after:
case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
lift a to NNReal using ha
  lift b to NNReal using hb
  exact_mod_cast NNReal.add_rpow_le_rpow_add a b hp1

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

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p✝ : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ ≤ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1

Tactic:
by simp [h2i₀]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : 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:
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
  have H₁ : ∀ s : Finset ι,
      (∑ i ∈ s, (f i + g i) ^ p) ≤
        ((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p := by
    intro s
    rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]
    refine le_trans (Lp_add_le s f g hp) ?_
    gcongr <;>
      refine Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_
    exacts [hf, hg]
  have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p) := by
    refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩
    rintro a ⟨s, rfl⟩
    exact H₁ s
  have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
  refine ⟨H₂, ?_⟩
  rw [one_div, NNReal.rpow_inv_le_iff pos, ← one_div]
  exact H₂.tsum_le_of_sum_le H₁

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
convert! h ε.toReal (ENNReal.toReal_pos hε.ne' hε_top) with i a

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
i : ι
a : α
⊢ ε ≤ edist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (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
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ 0 ∈ {f | eLpNorm (↑f) p μ < ∞}

Tactic:
by simp [eLpNorm_congr_ae AEEqFun.coeFn_zero, eLpNorm_zero]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB

Goal state after:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a ↦ f a ^ p) (A ^ p)
hgB : HasSum (fun a ↦ g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i ↦ (f i + g i) ^ p) (C ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i ↦ ((fun i ↦ ↑(f i)) i + (fun i ↦ ↑(g i)) 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
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
⊢ TendstoInMeasure μ f atTop g

Tactic:
tendstoInMeasure_iff_tendsto_toNNReal

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
by
  refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
  refine tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
    hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_
  have : (fun n => eLpNorm ((hf n).mk (f n) - hg.mk g) p μ) = fun n => eLpNorm (f n - g) p μ := by
    ext1 n; refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)
  rw [this]
  exact hfg

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✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous

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✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case inl
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : μ s₂ ≠ ∞
H : μ s₁ = ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁

pp: case inr
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : μ s₂ ≠ ∞
H : μ s₁ < ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
· simp [measureReal_def, H, measure_sdiff_eq_top H h']

Goal state after:
case inr
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : μ s₂ ≠ ∞
H : μ s₁ < ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Module: Mathlib.MeasureTheory.Measure.Real

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

Tactic:
simp only [measureReal_def, add_apply, ENNReal.toReal_add h₁ h₂]

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 μ
ε : ℝ
hε : 0 < ε
x : α
⊢ ε ≤ ‖f x‖ ↔ ‖ε‖ ≤ ‖f x‖

Tactic:
Real.norm_of_nonneg hε.le

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
⊢ ε ≤ ‖f x‖ ↔ ε ≤ ‖f x‖
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 : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∏ j, update (fun x ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)

Tactic:
rw [prod_update_of_mem (Finset.mem_univ _)]

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 : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ‖m₁ - m₂‖ * ∏ x ∈ univ \ {i}, max ‖m₁‖ ‖m₂‖ = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖

case refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖
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 𝕜
z : G
⊢ ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
𝕜 : 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 𝕜
z : G
⊢ ‖f.smulRight z‖₊ ≤ ‖f‖₊ * ‖z‖₊

case refine_2
𝕜 : 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 𝕜
z : G
⊢ ‖f‖₊ * ‖z‖₊ ≤ ‖f.smulRight z‖₊
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
h_ind : ∀ (n : ℕ), U ⊆ ↑M + c ^ n • U
h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets
x : Eᵤ
hx : x ∈ U
⊢ x ∈ ↑M

Tactic:
choose m hm u hu h_eq using fun n ↦ h_ind n hx

Goal state after:
𝕜 : 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
h_ind : ∀ (n : ℕ), U ⊆ ↑M + c ^ n • U
h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets
x : Eᵤ
hx : x ∈ U
m : ℕ → Eᵤ
hm : ∀ (n : ℕ), m n ∈ ↑M
u : ℕ → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun x1 x2 ↦ x1 + x2) (m n) (u n) = x
⊢ x ∈ ↑M
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 α
⊢ ∀ {x : ↥(Lp E p μ)}, x ∈ {f | ∃ s, AEEqFun.mk ⇑s ⋯ = ↑f} → -x ∈ {f | ∃ s, AEEqFun.mk ⇑s ⋯ = ↑f}

Tactic:
by
    rintro f ⟨s, hs⟩
    use -s
    simp only [← hs, AEEqFun.neg_mk, SimpleFunc.coe_neg, AddSubgroup.coe_neg]

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

Goal state before:
pp: case cons
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
ι : Type u_8
s✝ : Finset ι
μ : ι → Measure α
T : ι → Set α → β
C : ι → ℝ
hT : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
i : ι
s : Finset ι
his : i ∉ s
hs' : s.Nonempty
ih : DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs' C)
⊢ DominatedFinMeasAdditive (∑ i ∈ cons i s his, μ i) (∑ i ∈ cons i s his, T i) ((cons i s his).sup' ⋯ C)

Tactic:
simpa [his, Finset.sup'_cons hs' C] using (hT i).add_measure (μ i) (∑ j ∈ s, μ j) ih

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
⊢ P f

Tactic:
suffices ∀ f : α →ₛ E, ∀ hf : MemLp f p μ, P (toLp f hf) by
    rw [← toLp_toSimpleFunc f]
    apply this

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
⊢ ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (f.toLp hf)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ μ.real s • x = μ.real t • x

Tactic:
measureReal_def

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ (μ s).toReal • x = (μ t).toReal • x
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 ≠ ∞
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (f a) ∂μ).toReal

Tactic:
have hf' : f.FinMeasSupp μ := integrable_iff_finMeasSupp.1 hf

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 μ
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (f a) ∂μ).toReal