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

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

Tactic:
by_cases hp' : p = ∞
  · subst hp'
    simp_rw [eLpNorm_exponent_top] at hbdd
    have : ∀ n, ∀ᵐ x ∂μ, (‖f n x‖ₑ) < R + 1 := fun n =>
      ae_lt_of_essSup_lt
        (lt_of_le_of_lt (hbdd n) <| ENNReal.lt_add_right ENNReal.coe_ne_top one_ne_zero)
    rw [← ae_all_iff] at this
    filter_upwards [this] with x hx using lt_of_le_of_lt
        (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
        (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)
  filter_upwards [ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd hfmeas hbdd] with x hx
  have hppos : 0 < p.toReal := ENNReal.toReal_pos hp hp'
  have :
    liminf (fun n => (‖f n x‖ₑ) ^ p.toReal) atTop =
      liminf (fun n => (‖f n x‖ₑ)) atTop ^ p.toReal := by
    change
      liminf (fun n => ENNReal.orderIsoRpow p.toReal hppos (‖f n x‖ₑ)) atTop =
        ENNReal.orderIsoRpow p.toReal hppos (liminf (fun n => (‖f n x‖ₑ)) atTop)
    refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm <;>
      isBoundedDefault
  rw [this] at hx
  rw [← ENNReal.rpow_one (liminf (‖f · x‖ₑ) atTop), ← mul_inv_cancel₀ hppos.ne.symm,
    ENNReal.rpow_mul]
  exact ENNReal.rpow_lt_top_of_nonneg (inv_nonneg.2 hppos.le) hx.ne

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
⊢ z i ^ w i = 0

Tactic:
rw [hzi]

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 ^ w i = 0
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁷ : CommRing 𝕜
inst✝¹⁶ : LinearOrder 𝕜
inst✝¹⁵ : IsStrictOrderedRing 𝕜
inst✝¹⁴ : CommRing E
inst✝¹³ : LinearOrder E
inst✝¹² : IsStrictOrderedRing E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : LinearOrder F
inst✝⁹ : IsOrderedAddMonoid F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 G
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : IsOrderedModule 𝕜 F
inst✝ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x) ≤
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y)

Tactic:
gcongr _ + (a * b) • ?_

Goal state after:
case hb
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁷ : CommRing 𝕜
inst✝¹⁶ : LinearOrder 𝕜
inst✝¹⁵ : IsStrictOrderedRing 𝕜
inst✝¹⁴ : CommRing E
inst✝¹³ : LinearOrder E
inst✝¹² : IsStrictOrderedRing E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : LinearOrder F
inst✝⁹ : IsOrderedAddMonoid F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 G
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : IsOrderedModule 𝕜 F
inst✝ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x • g y + f y • g x ≤ f x • g x + f y • g y
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ ∑ i ∈ s, w i * x = x

Tactic:
by rw [← sum_mul, hw', one_mul]

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
⊢ z i ^ w i = 0

Tactic:
rw [hzi]

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 ^ w i = 0
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y) ≤
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x)

Tactic:
gcongr _ + (a * b) • ?_

Goal state after:
case hb
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x • g x + f y • g y ≤ f x • g y + f y • g x
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : 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 ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, ∀ k ∈ s, z j = z k

Tactic:
refine ⟨by grind [geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz], fun h ↦ ?_⟩
  have ⟨k, hk⟩ : s.Nonempty := by grind [s.eq_empty_or_nonempty]
  suffices ∏ i ∈ s, z k ^ w i = ∑ i ∈ s, w i * z k by convert this using 3 <;> grind
  rw [← rpow_sum_of_nonneg (hz k hk) (hw · · |>.le), ← sum_mul, hw', rpow_one, one_mul]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

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

pp: case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
· 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

Goal state after:
case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ENNReal.ofReal ↑c * eLpNorm (fun i ↦ ‖f i‖ * ‖g i‖) p μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
ENNReal.ofReal_coe_nnreal,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ↑c * eLpNorm (fun i ↦ ‖f i‖ * ‖g i‖) p μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g p μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
⊢ ∑ i ∈ s, f i * g i ≤ 1

Tactic:
by
  have hp : 0 < p.toNNReal := zero_lt_one.trans hpq.toNNReal.lt
  have hq : 0 < q.toNNReal := zero_lt_one.trans hpq.toNNReal.symm.lt
  calc
    ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
      Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
    _ = (∑ i ∈ s, f i ^ p) / Real.toNNReal p + (∑ i ∈ s, g i ^ q) / Real.toNNReal q := by
      rw [sum_add_distrib, sum_div, sum_div]
    _ ≤ 1 / Real.toNNReal p + 1 / Real.toNNReal q := by gcongr
    _ = 1 := by simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ENNReal.ofReal ↑c * eLpNorm' (fun i ↦ ‖f i‖ * ‖g i‖) r μ ≤ ↑c * eLpNorm' f p μ * eLpNorm' g q μ

Tactic:
ENNReal.ofReal_coe_nnreal,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ↑c * eLpNorm' (fun i ↦ ‖f i‖ * ‖g i‖) r μ ≤ ↑c * eLpNorm' f p μ * eLpNorm' g q μ
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
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
set ns := ExistsSeqTendstoAe.seqTendstoAeSeq hfg

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (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✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
h2 : ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝
h3 : ↑↑g₁ a✝ ≤ ↑↑g₂ a✝
⊢ (↑↑f + ↑↑g₁) a✝ ≤ ↑↑(f + g₂) a✝

Tactic:
h2,

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
h2 : ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝
h3 : ↑↑g₁ a✝ ≤ ↑↑g₂ a✝
⊢ (↑↑f + ↑↑g₁) a✝ ≤ (↑↑f + ↑↑g₂) a✝
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ max ((-↑↑f) a✝) 0 = max (-↑↑f a✝) 0

Tactic:
Pi.neg_apply

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ max (-↑↑f a✝) 0 = max (-↑↑f a✝) 0
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case hab
ι : 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 𝕜 := ⋯
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
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ ≤ ‖∏ i ∈ I, c i‖

Tactic:
exact ha.out.le

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

Goal state before:
pp: case inr
𝕜 : 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)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
    · exact this inferInstance
    · intro f
      use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
      simp [DFunLike.ext_iff]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : μ u ≠ ∞
⊢ (s ∩ t).Nonempty

Tactic:
by
  apply nonempty_inter_of_measure_lt_add μ ht h's h't ?_
  apply (ENNReal.toReal_lt_toReal hu _).1
  · rw [ENNReal.toReal_add (measure_ne_top_of_subset h's hu) (measure_ne_top_of_subset h't hu)]
    exact h
  · exact ENNReal.add_ne_top.2 ⟨measure_ne_top_of_subset h's hu, measure_ne_top_of_subset h't hu⟩

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

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

Tactic:
exact h.mono_measure <| Measure.restrict_mono_measure Measure.restrict_le_self _

Goal state after:
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:
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.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ Integrable f ((μ.restrict s).restrict sᶜ)

Tactic:
restrict_restrict,

Goal state after:
case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ Integrable f (μ.restrict (sᶜ ∩ s))

case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ MeasurableSet sᶜ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case refine_4
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
rcases mem_nhds_iff.1 ux with ⟨v, vu, v_open, xv⟩

Goal state after:
case refine_4
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
v : Set X
vu : v ⊆ u
v_open : IsOpen[inst✝³] v
xv : x ∈ v
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ MemLp g ∞ μ

Tactic:
exact hg.memLp_top_of_hasCompactSupport h'g μ

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

Goal state before:
pp: case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ MemLp g ∞ μ

Tactic:
exact hg.memLp_top_of_hasCompactSupport h'g μ

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
f : X → E
inst✝ : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
refine ⟨Icc a b, hab, ?_⟩

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
f : X → E
inst✝ : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f A μ
g : X → E
hg : ContinuousOn g K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g x‖ ≤ C
⊢ IntegrableOn (fun x ↦ f x • g x) A μ

Tactic:
exact hf.smul_bdd C ((hg.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

Goal state after: