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

Goal state before:
pp: case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
have hp_lt_top : p < ∞ := hpq.trans_lt (lt_top_iff_ne_top.mpr hq_top)

Goal state after:
case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
by
        congr with i
        rw [mul_comm]

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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr✝ : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
⊢ 0 < 1 / r.toReal

Tactic:
by rw [hpqr']; positivity

Goal state after:
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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
f_lim : α → E
hf_lim_meas : MemLp f_lim p μ
h_tendsto : Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ x, Tendsto f atTop (𝓝 x)

Tactic:
exact ⟨hf_lim_meas.toLp f_lim, tendsto_Lp_of_tendsto_eLpNorm f_lim hf_lim_meas h_tendsto⟩

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
← Real.rpow_mul hg',

Goal state after:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
hf' : 0 ≤ ∑' (i : ι), f i ^ p
hg' : 0 ≤ ∑' (i : ι), g i ^ q
hr : 0 < r
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    ((∑' (i : ι), f i ^ p) ^ (r / p)) ^ (1 / r) * (∑' (i : ι), g i ^ q) ^ (r / q * (1 / r))
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_pow : ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
⊢ (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i

Tactic:
by
      rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]

Goal state after:
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
B : G →L[𝕜] E →L[𝕜] F
g h : G
⊢ compLpₗ p μ (B (g + h)) = compLpₗ p μ (B g) + compLpₗ p μ (B h)

Tactic:
ext f
    filter_upwards [(B (g + h)).coeFn_compLp f, (B g).coeFn_compLp f, (B h).coeFn_compLp f,
      Lp.coeFn_add ((B g).compLp f) ((B h).compLp f)] with x hx hg hh hadd
    simp only [compLpₗ_apply, LinearMap.add_apply, hx, hadd]
    simp only [map_add, add_apply, Pi.add_apply, hg, hh]

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✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
⊢ Tendsto (fun i ↦ f (ns i) ω) atTop (𝓝 (g ω)) → Tendsto (fun i ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω)) → g ω = h ω

Tactic:
hg1

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun i ↦ f (ns i) ω) atTop (𝓝 (g ω))
⊢ Tendsto (fun i ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω)) → g ω = h ω
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : PseudoEMetricSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
⊢ AEMeasurable g μ

Tactic:
by
  obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'
  exact aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ (a / ∏ i ∈ I, c i) • f (update y i₀ (y i₀)) = a • f x

Tactic:
update_eq_self,

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ (a / ∏ i ∈ I, c i) • f y = a • f x
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case neg
𝕜 : 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
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖

Tactic:
rcases rescale_to_shell_zpow hc ε0 hx with ⟨n, -, hlt, -, hle⟩

Goal state after:
case neg
𝕜 : 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 : ‖σ₁₂ c ^ n • f x‖ < ↑ε
hle : ‖σ₁₂ c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖σ₁₂ c‖ * ‖f x‖
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case hg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ (fun x_1 ↦ ‖x_1.2 - x.2‖) =o[𝓝 x] fun _x ↦ 1

Tactic:
rw [isLittleO_norm_left, isLittleO_one_iff, ← sub_self x.2]

Goal state after:
case hg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun x_1 ↦ x_1.2 - x.2) (𝓝 x) (𝓝 (x.2 - x.2))
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✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
M : Type u_5
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : SMulCommClass 𝕜 M F
inst✝ : ContinuousConstSMul M F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Tactic:
let := IsTopologicalAddGroup.rightUniformSpace F

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✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
M : Type u_5
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : SMulCommClass 𝕜 M F
inst✝ : ContinuousConstSMul M F
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)
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
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := fun g ↦ { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
⊢ Continuous[topologicalSpace, topologicalSpace] aux.toFun

Tactic:
by
      apply continuous_of_tendsto_nhds_zero aux
      rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff <|
        ContinuousLinearMap.hasBasis_nhds_zero_of_basis <|
        ContinuousMultilinearMap.hasBasis_nhds_zero]
      rintro ⟨U, V, W⟩ ⟨hU, hV, hW⟩
      refine ⟨(.image2 (fun f v ↦ f v) U V, W), ⟨?_, hW⟩, ?_⟩
      · exact ContinuousMultilinearMap.isVonNBounded_image2_apply hU hV
      · exact fun g hg f hf m hm ↦ hg _ <| mem_image2_of_mem hf hm

Goal state after:
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 t : Set α
hs : MeasurableSet s
hsμ : μ s ≠ ∞
ht : MeasurableSet t
htμ : μ t ≠ ∞
c : E
hc : c ≠ 0
⊢ indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t

Tactic:
by
  simp_rw [← indicator_const_eventuallyEq hc, indicatorConstLp, MemLp.toLp_eq_toLp_iff]

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

Goal state before:
pp: case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝¹ : Fintype ι
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = 0
⊢ Continuous[inst✝⁴, Pi.topologicalSpace] ⇑ξ.equivFun

Tactic:
Fintype.card_eq_zero_iff

Goal state after:
case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝¹ : Fintype ι
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : IsEmpty ι
⊢ Continuous[inst✝⁴, Pi.topologicalSpace] ⇑ξ.equivFun
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : (fun x ↦ g x * (f x).toReal) = fun x ↦ (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
exact integrable_withDensity_iff_integrable_smul' hf hflt

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ∞
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩

Goal state after:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ∞
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable ((support g).indicator (f + g)) μ

Tactic:
exact hfg.indicator hg.measurableSet_support

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, μ s = ∞
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : (μ.restrict v) v < ∞
⊢ False

Tactic:
have : μ v ≠ ∞ := ne_of_lt (by simpa only [Measure.restrict_apply_self])

Goal state after:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, μ s = ∞
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this✝ : (μ.restrict v) v < ∞
this : μ v ≠ ∞
⊢ False
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

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

Tactic:
cases n
  · rw [norm_mkPiAlgebraFin_zero]
    simp
  · refine le_antisymm norm_mkPiAlgebraFin_succ_le ?_
    refine le_of_eq_of_le ?_ <|
      ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1
    simp

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 x

Tactic:
obtain rfl | hl := eq_or_neBot l
  · simpa [limUnder, Filter.map_bot] using stronglyMeasurable_const
  let e := Classical.choice hE
  let conv := {x | ∃ c, Tendsto (f · x) l (𝓝 c)}
  have mconv : MeasurableSet conv := StronglyMeasurable.measurableSet_exists_tendsto hf
  have hconv : StronglyMeasurable (fun x : conv ↦ limUnder l (f · x)) := by
    refine stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_
    refine tendsto_pi_nhds.2 fun x ↦ ?_
    obtain ⟨c, hc⟩ := x.2
    rwa [hc.limUnder_eq]
  have : (fun x ↦ limUnder l (f · x)) = ((↑) : conv → X).extend
      (fun x ↦ limUnder l (f · x)) (fun _ ↦ e) := by
    ext x
    by_cases hx : x ∈ conv
    · rw [Function.extend_val_apply hx]
    · rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
  rw [this]
  exact (MeasurableEmbedding.subtype_coe mconv).stronglyMeasurable_extend hconv
    stronglyMeasurable_const

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ‖f‖ = (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal

Tactic:
simp [Lp.norm_def, eLpNorm, eLpNorm'_eq_lintegral_enorm]

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

Goal state before:
pp: case refine_1
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
⊢ ∃ u, IsOpen[inst✝³] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ

pp: case refine_2
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
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ

pp: case refine_3
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
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

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 ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
· refine ⟨∅, isOpen_empty, Subset.rfl, integrableOn_empty⟩

Goal state after:
case refine_2
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
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ

case refine_3
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
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

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 ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ
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
𝕜 : 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
⊢ (support fun x ↦ g x • f x) ⊆ K

Tactic:
apply support_subset_iff'.2

Goal state after:
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
⊢ ∀ x ∉ K, g x • f x = 0