mathlib-initiative/mathlib-tactics huggingface dataset:
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
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / (p2 * p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / (q2 * p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
mul_comm p2,

Goal state after:
α : 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
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / (p * p2)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / (q2 * p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_1
ι : 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)
⊢ ∑ x ∈ s, f x ^ p / ((∑ i ∈ s, f i ^ p) ^ (1 / p)) ^ p = 1

Tactic:
← sum_div,

Goal state after:
case inr.inr.refine_1
ι : 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, f i ^ p) / ((∑ i ∈ s, f i ^ p) ^ (1 / p)) ^ p = 1
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)
⊢ ∑ x ∈ s, g x ^ q / ((∑ i ∈ s, g i ^ q) ^ (1 / q)) ^ q = 1

Tactic:
← sum_div,

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 / q)) ^ q = 1
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
pos : 0 < p
s : Finset ι
⊢ ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ p⁻¹ + (∑' (i : ι), g i ^ p) ^ p⁻¹) ^ p

Tactic:
← NNReal.rpow_inv_le_iff pos,

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
s : Finset ι
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ p⁻¹ ≤ (∑' (i : ι), f i ^ p) ^ p⁻¹ + (∑' (i : ι), g i ^ p) ^ p⁻¹
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
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ 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 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

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s ↦ ∑ i ∈ s, (f 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)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case neg
α : 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∞
hε : 0 < ε
hε_top : ¬ε = ∞
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
· exact h ε hε hε_top

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SeminormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ.real {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)

Tactic:
by
  rw [tendstoInMeasure_iff_enorm]
  congr! with ε hε hε_top
  simp_rw [measureReal_def, ENNReal.tendsto_toReal_zero_iff (fun _ ↦ measure_ne_top _ _)]

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

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
⊢ eLpNorm f_lim p μ ≤ liminf (fun n ↦ eLpNorm (f n) p μ) atTop

Tactic:
by_cases hp_top : p = ∞

Goal state after:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : p = ∞
⊢ eLpNorm f_lim p μ ≤ liminf (fun n ↦ eLpNorm (f n) p μ) atTop

case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm f_lim p μ ≤ liminf (fun n ↦ eLpNorm (f n) p μ) atTop
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
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto f fi (𝓝 f_lim) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
by
  rw [tendsto_iff_dist_tendsto_zero]
  simp_rw [dist_def]
  rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
  rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
  exact Lp.eLpNorm_ne_top _

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ toLp f hf = toLp g hg ↔ f =ᵐ[μ] g

Tactic:
by simp [toLp]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ

Tactic:
obtain ⟨t, _, ht, hunif⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist' hf hfg hδ

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

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

Tactic:
suffices { x : α | ε ≤ edist (f n x) (g x) } ⊆ t from (measure_mono this).trans ht

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

Tactic:
by
  specialize hfg ((2⁻¹ : ℝ≥0∞) ^ n) (ENNReal.pow_pos (by simp) _)
  rw [ENNReal.tendsto_atTop_zero] at hfg
  exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr <| pow_ne_zero _ <| by simp)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ eLpNorm (↑(c • ↑f)) p μ < ∞

Tactic:
eLpNorm_congr_ae (AEEqFun.coeFn_smul _ _)

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ eLpNorm (c • ↑↑f) p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_6
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg (norm_nonneg _), ← Real.rpow_mul (abs_nonneg _),
      ENNReal.toReal_inv, mul_inv_cancel₀, abs_of_nonneg (norm_nonneg _), Real.rpow_one]

Goal state after:
case e'_6
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ q.toReal ≠ 0
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
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 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
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

Tactic:
by_cases hp_top : p = ∞

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 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
hp_top : p = ∞
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

case neg
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 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
hp_top : ¬p = ∞
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq : g b₁ = f a₂
⊢ Sum.inr b₁ = Sum.inl a₂

Tactic:
exfalso
        exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ { toFun := fun x ↦ x✝ default, inj' := ⋯ } x = x✝ x

Tactic:
Function.Embedding.coeFn_mk

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ x✝ default = x✝ x
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : IsStrictMap f ∧ Surjective f
f_strict : IsStrictMap f
f_surj : Surjective f
⊢ IsQuotientMap f

Tactic:
rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at f_strict

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : IsStrictMap f ∧ Surjective f
f_strict : IsQuotientMap (rangeFactorization f)
f_surj : Surjective f
⊢ IsQuotientMap f
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by_cases hp_top : p = ∞

Goal state after:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ∞
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : ¬p = ∞
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖ₑ

Tactic:
by
  unfold indicatorConstLp
  rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case pos
𝕜 : 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
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ 0 ≤ C * 0

Tactic:
mul_zero

Goal state after:
case pos
𝕜 : 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
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ 0 ≤ 0
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

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

Tactic:
norm_mkPiAlgebraFin_zero

Goal state after:
case zero
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖1‖ = 1
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: 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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
⊢ ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen[inst✝³] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ

Tactic:
have : ∀ x : s, ∃ u, IsOpen u ∧ x.1 ∈ u ∧ IntegrableOn f (u ∩ s) μ := by
    rintro ⟨x, hx⟩
    rcases hf x hx with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩
    exact ⟨u, u_open, x_mem, h't.mono_set u_sub⟩
  choose u u_open xu hu using this
  obtain ⟨T, T_count, hT⟩ : ∃ T : Set s, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i := by
    have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
    obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
    exact ⟨T, hT_count, by rwa [hT_un]⟩
  refine ⟨u '' T, T_count.image _, ?_, by rwa [biUnion_image], ?_⟩
  · rintro v ⟨w, -, rfl⟩
    exact u_open _
  · rintro v ⟨w, -, rfl⟩
    exact hu _

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_2.inr
𝕜 : 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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ ‖f m‖₊ * ‖z‖₊ ≤ ‖f m • z‖₊

Tactic:
nnnorm_smul

Goal state after:
case refine_2.inr
𝕜 : 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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ ‖f m‖₊ * ‖z‖₊ ≤ ‖f m‖₊ * ‖z‖₊
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h₁
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDerivComponent e‖ ≤ ‖f‖

pp: case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a // a ∉ s }
a✝ : i ∈ univ
⊢ ‖x ↑i‖ ≤ ‖x‖

Tactic:
· exact MultilinearMap.mkContinuousMultilinear_norm_le _ (norm_nonneg _) _

Goal state after:
case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a // a ∉ s }
a✝ : i ∈ univ
⊢ ‖x ↑i‖ ≤ ‖x‖
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
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x ↦ C) ∞ (μ.restrict s)
⊢ MemLp f ∞ (μ.restrict s)

Tactic:
apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x ↦ C) ∞ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst✝ : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ∞
⊢ μ s = ∞ ∨ c = ∞ ∧ ¬μ s = 0

Tactic:
exact Or.inl hμs

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
⊢ MemLp (⇑f) p μ

Tactic:
by_cases hp_top : p = ∞

Goal state after:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : p = ∞
⊢ MemLp (⇑f) p μ

case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ MemLp (⇑f) p μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ C * 0 = 0

Tactic:
mul_zero

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ 0 = 0