mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
by
  choose s h1s h2s using hC
  cases nonempty_encodable (ι → ℕ)
  let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).getD default
  refine ⟨fun n => Set.pi univ fun i => s i (e n i), fun n =>
    mem_image_of_mem _ fun i _ => h1s i _, ?_⟩
  simp_rw [e,
    (surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
    iUnion_univ_pi s, h2s, pi_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
⊢ ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝ → ↑(f ⊔ g) a✝ ≤ ↑f' a✝

Tactic:
ha_sup

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝

Tactic:
ha_sup

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ⊔ ↑g a✝ ≤ ↑f' a✝
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✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (List.map (fun i ↦ (μ i) (s i)) (sortedUniv ι)).prod = ∏ i, (μ i) (s i)

pp: case hnd
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

pp: case hnd
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

Tactic:
←
    List.prod_toFinset,

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ∏ i ∈ (sortedUniv ι).toFinset, (μ i) (s i) = ∏ i, (μ i) (s i)

case _hl
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

case hnd
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

case hnd
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ ∫⁻ (a : α), ↑f a ∂μ = f.lintegral

Tactic:
rw [← lintegral_mk (hf := f.aestronglyMeasurable), mk_coeFn]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ε ≤ ‖f x‖₊} < ∞

Tactic:
by
  simp_rw [← ENNReal.coe_le_coe]
  apply hℒp.meas_ge_lt_top' hp_ne_zero hp_ne_top (by simp [hε])

Goal state after:
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 x✝ : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (x✝ i)
⊢ ((Measure.pi μ).restrict (univ.pi fun i ↦ s i)) (univ.pi x✝) = ∏ i, ((μ i).restrict (s i)) (x✝ i)

Tactic:
simp_rw [restrict_apply (MeasurableSet.univ_pi h), restrict_apply (h _),
    ← Set.pi_inter_distrib, pi_pi]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
by_cases hg' : eLpNorm' g p μ = 0
    · have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 := by
        simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
        rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
        exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx
      have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all
      simpa only [hg', mul_zero, nonpos_iff_eq_zero] using eLpNorm'_eq_zero_of_ae_eq_zero hp this
    · simp_all

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

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm (fun x ↦ ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
rw [← eLpNorm_enorm_rpow f hq_pos]

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm (fun x ↦ ‖f x‖ ^ q) p μ = eLpNorm (fun x ↦ ‖f x‖ₑ ^ q) p μ
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Tactic:
have hxy' : 0 < y - x := by linarith
  have hxz' : 0 < z - x := by linarith
  field_simp
  linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ 1

Tactic:
simpa using! convexOn_id (convex_Ici _)

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Tactic:
antivaryOn_inv_left₀ hf,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
⊢ MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔
    (∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → f x < f x_2 → g x ≤ g x_2) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → g x < g x_2 → f x ≤ f x_2

Tactic:
exact (and_iff_right_of_imp MonovaryOn.symm).symm

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : 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
⊢ ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

Tactic:
· have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
    simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this
    convert! this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl] <;> intro i hi
    · rcases eq_or_lt_of_le (hz i hi) with hz | hz
      · simp [A i hi hz.symm]
      · exact rpow_def_of_pos hz _
    · rcases eq_or_lt_of_le (hz i hi) with hz | hz
      · simp [A i hi hz.symm]
      · rw [exp_log 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,
    ← @NNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1]), inv_inv]
  exact add_rpow_le_rpow_add _ _ hp1

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
by_cases h : 1 < p
  · have hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo (0 : ℝ≥0∞) 1 := by
      constructor
      · simp
      · rwa [ENNReal.inv_lt_one, one_lt_ofReal]
    rw [show LpAddConst (ENNReal.ofReal p)⁻¹ =
        (2 : ℝ≥0∞) ^ (1 / ((ENNReal.ofReal p)⁻¹).toReal - 1) by
      rw [LpAddConst, if_pos hmem]]
    simp only [ENNReal.toReal_inv, div_inv_eq_mul, one_mul]
    rw [ENNReal.toReal_ofReal hp]
    exact rpow_add_le_mul_rpow_add_rpow _ _ h.le
  · have hp1 : p ≤ 1 := not_lt.mp h
    rw [LpAddConst_of_one_le (ENNReal.one_le_inv.mpr (ENNReal.ofReal_le_one.mpr hp1)), one_mul]
    exact rpow_add_le_add_rpow _ _ hp hp1

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

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
rw [h_rw]

Goal state after:
case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
calc
    (∫⁻ a : α, (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ a : α, f a ^ p * g a ^ p ∂μ) ^ (1 / p) := by
      simp_rw [Pi.mul_apply, ENNReal.mul_rpow_of_nonneg _ _ hp0]
    _ ≤ ((∫⁻ a, f a ^ (p * p2) ∂μ) ^ (1 / p2) *
        (∫⁻ a, g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) := by
      gcongr
      simp_rw [ENNReal.rpow_mul]
      exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)
    _ = (∫⁻ a : α, f a ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) := by
      rw [@ENNReal.mul_rpow_of_nonneg _ _ (1 / p) (by simp [hp0]), ← ENNReal.rpow_mul, ←
        ENNReal.rpow_mul]
      have hpp2 : p * p2 = q := by
        symm
        rw [mul_comm, ← div_eq_iff hp0_ne]
      have hpq2 : p * q2 = r := by
        rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
        simp [field, p2, q2, Real.conjExponent]
      simp_rw [div_mul_div_comm, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_m : AEMeasurable (fun a ↦ (f + g) a ^ (p - 1)) μ
h_add_apply : ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ = ∫⁻ (a : α), (f a + g a) * (f + g) a ^ (p - 1) ∂μ
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) + g a * (f + g) a ^ (p - 1) ∂μ =
    ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ

Tactic:
rw [lintegral_add_left' (hf.fun_mul h_add_m)]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, g i ^ q) / (∑ i ∈ s, g i ^ q) ^ (q⁻¹ * q) = 1

Tactic:
inv_mul_cancel₀ hpq.symm.ne_zero,

Goal state after:
case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, g i ^ q) / (∑ i ∈ s, g i ^ q) ^ 1 = 1
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
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
intro ε

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
⊢ 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
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
⊢ TendstoInMeasure μ f' l g'

Tactic:
intro ε

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∞
⊢ 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)
Module: Mathlib.Analysis.MeanInequalities

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

pp: case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i * f i ^ p

pp: case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

pp: case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i

pp: case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

Tactic:
← rpow_add',

Goal state after:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ (∑ i ∈ s, w i * f i) / ↑(#s) ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ / ↑(#s) ^ (1 - p⁻¹ + p⁻¹)

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

case h
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 1 - p⁻¹ + p⁻¹ ≠ 0

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i * f i ^ p

case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i

case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) ≤
    ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) ^ p⁻¹)
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
coe_mul

Goal state after:
case neg
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) ≤
    ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹)) * ↑((∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) ^ p⁻¹)
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
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 σ
F : Type u_8
G : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
⊢ ‖(B c).compLp f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖

Tactic:
norm_compLp_le,

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 σ
F : Type u_8
G : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
⊢ ‖B c‖ * ‖f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 ↦ ‖(f x - g) x_1‖ₑ) μ ≤ ε
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ edist (f x x_1) (g x_1)} ≤ ε

Tactic:
intro ε

Goal state after:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 ↦ ‖(f x - g) x_1‖ₑ) μ ≤ ε
ε : ℝ≥0∞
⊢ ε > 0 → ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ edist (f x x_1) (g x_1)} ≤ ε
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
intro ε

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
⊢ ε > 0 → ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
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 t, (∀ (i : ι), t i ∈ 𝓝 0) ∧ (↑I).pi t ⊆ ⇑f ⁻¹' V

Tactic:
have hfV : f ⁻¹' V ∈ 𝓝 0 := (map_continuous f).tendsto' _ _ f.map_zero hV

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 := ⋯ }
hfV : ⇑f ⁻¹' V ∈ 𝓝 0
⊢ ∃ I t, (∀ (i : ι), t i ∈ 𝓝 0) ∧ (↑I).pi t ⊆ ⇑f ⁻¹' V
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case hbc
𝕜 : 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 • x‖ ≤ 1

Tactic:
exact (hε _ hlt).le

Goal state after: