mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q

Tactic:
apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
⊢ Metric.ball 0 ε ⊆ q.ball 0 1
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sSup ((fun x ↦ ‖f x‖) '' ball 0 1) = ‖f‖

Tactic:
by
  simpa only [NNReal.coe_sSup, Set.image_image] using! NNReal.coe_inj.2 f.sSup_unit_ball_eq_nnnorm

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ ∀ (K : Set X), IsCompact K → ContinuousOn (CompactCoherentification.map f ∘ ⇑(CompactCoherentification.mk X)) K

Tactic:
CompactCoherentification.map_comp_mk

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ ∀ (K : Set X), IsCompact K → ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) K
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance

Tactic:
simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
    UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover',
    UniformSpace.comap_iInf, ← UniformSpace.comap_comap]

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (toUniformOnFunIsCompact ∘ fun x ↦ x.comp (φ i)) inferInstance
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
⊢ μ[|univ] = μ

Tactic:
simp [cond, measure_univ, Measure.restrict_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✝ : α
⊢ ↑f a✝ ≤ ↑f' a✝ → ↑g a✝ ≤ ↑f' a✝ → ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝ → ↑(f ⊔ g) a✝ ≤ ↑f' a✝

Tactic:
haf

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✝
⊢ ↑g a✝ ≤ ↑f' a✝ → ↑(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✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
⊢ ↑f' a✝ ≤ ↑f a✝ → ↑f' a✝ ≤ ↑g a✝ → ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝ → ↑f' a✝ ≤ ↑(f ⊓ g) a✝

Tactic:
haf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ x = b

Tactic:
case =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ ∃ b', AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ = fun x ↦ b'

Tactic:
case =>

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

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

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

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)
i : ι
s : Set (α i)
hs : (μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : (μ i) t = 0
⊢ (μ i) (update (fun j ↦ univ) i t i) = 0

Tactic:
simp [hμt]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x ↦ c) μ < ‖c‖ₑ
h' : μ {a | ¬‖s.indicator (fun x ↦ c) a‖ₑ < ‖c‖ₑ} = 0
⊢ False

Tactic:
push Not at h'

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x ↦ c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x ↦ c) a‖ₑ} = 0
⊢ False
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖

Tactic:
rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
        Real.norm_eq_abs, abs_of_nonneg hc]

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ c
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ (p + q) / q = p

Tactic:
← h.mul_eq_add,

Goal state after:
case inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p * q / q = p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

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

Goal state after:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ∞ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < ↑R + 1
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ) atTop < ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case refine_2
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∑ i ∈ insertNone s, i.elim q p = 1

pp: case refine_3
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∀ i ∈ insertNone s, 0 ≤ i.elim q p

Tactic:
· simp_rw [sum_insertNone, Option.elim]
    exact hpq

Goal state after:
case refine_3
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∀ i ∈ insertNone s, 0 ≤ i.elim q p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
    rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top
    refine lt_of_le_of_lt (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos) ?_
    refine ENNReal.mul_lt_top hfq_lt_top ?_
    exact ENNReal.rpow_lt_top_of_nonneg (by simp [hp_pos.le]) (by finiteness)

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

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

pp: case h₂
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

Tactic:
· exact lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow hpq hf (hf.add hg)

Goal state after:
case h₂
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
obtain hg_top | hg_top := eq_top_or_lt_top (∫⁻ a, g a ^ p ∂μ)

Goal state after:
case inr.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ = ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

case inr.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
⊢ MemLp (fun ω ↦ ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
simpa [Finset.prod_fn] using MemLp.prod hf

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✝ : 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∞
hε : 0 < ε
this : (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) =ᶠ[l] fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)

Tactic:
tendsto_congr' this

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∞
hε : 0 < ε
this : (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) =ᶠ[l] fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 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
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
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)

Tactic:
have hB1 : ∑' i, B1 i < ∞ := by
    rw [hB1_has.tsum_eq]
    exact ENNReal.ofReal_lt_top

Goal state after:
α : 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
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ∞
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
⊢ ‖f‖₊ ≤ c * ‖g‖₊

Tactic:
by
  simp only [nnnorm_def]
  have := eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul h p
  rwa [← ENNReal.toNNReal_le_toNNReal, ENNReal.smul_def, smul_eq_mul, ENNReal.toNNReal_mul,
    ENNReal.toNNReal_coe] at this
  · finiteness
  · exact ENNReal.mul_ne_top ENNReal.coe_ne_top (by finiteness)

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

Goal state before:
pp: case zero
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg 0 ≤ k
⊢ μ {x | 2⁻¹ ^ 0 ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ 0

pp: case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (n✝ + 1) ≤ k
⊢ μ {x | 2⁻¹ ^ (n✝ + 1) ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ (n✝ + 1)

Tactic:
· exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn

Goal state after:
case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (n✝ + 1) ≤ k
⊢ μ {x | 2⁻¹ ^ (n✝ + 1) ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ (n✝ + 1)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
convert! this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp]

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i = ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i ^ p = ∑ x ∈ s, ↑(f x).toNNReal ^ p

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, g i ^ q = ∑ x ∈ s, ↑(g x).toNNReal ^ q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4
ι : 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 :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
⊢ (∑ i ∈ s, w i) ^ (1 - p⁻¹) = (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹)

Tactic:
convert! rfl with i hi

Goal state after:
case e'_3.a
ι : 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 :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
i : ι
hi : i ∈ s
⊢ ↑(w i).toNNReal = w i
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
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ (𝓝 0).HasBasis (fun Si ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si ↦ {f | MapsTo (⇑f) Si.1 (b Si.2)}

Tactic:
have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup

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
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (𝓝 0).HasBasis (fun Si ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si ↦ {f | MapsTo (⇑f) Si.1 (b Si.2)}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ → AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
rintro ⟨g', g'meas, hg'⟩
    refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.stronglyMeasurable.smul g'meas, ?_⟩
    rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
    filter_upwards [hg'] with x hx h'x
    rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]
    simp only [Ne, ENNReal.coe_eq_zero] at h'x
    simpa only [NNReal.coe_eq_zero, Ne] using h'x

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 : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')

Tactic:
simp_rw [indicatorConstLp, ← MemLp.toLp_add, indicator_add]

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ MemLp.toLp ((s.indicator fun x ↦ c) + s.indicator fun x ↦ c') ⋯ =
    MemLp.toLp (fun a ↦ s.indicator (fun x ↦ c) a + s.indicator (fun x ↦ c') a) ⋯
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
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const] <;> try assumption

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)