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

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p μ

Tactic:
rw [← this, memLp_indicator_iff_restrict (measurableSet_toMeasurable μ s)] at hfq ⊢

Goal state after:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p (μ.restrict (toMeasurable μ s))
Module: Mathlib.Analysis.MeanInequalities

Goal state before:

Tactic:
∑ i ∈ s, f i * g i = ∑ i ∈ s, g i * f i := by
        congr with i
        rw [mul_comm]
      _ ≤ (∑ i ∈ s, g i ^ q) ^ (1 / q) * (∑ i ∈ s, f i ^ p) ^ (1 / p) :=
        (inner_le_Lp_mul_Lp_of_norm_eq_zero s g f hpq.symm hg)
      _ = (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := mul_comm _ _

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.calc_1.e_f
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
i : ι
⊢ ↑(w i * f i) = ↑(w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i))

Tactic:
rw [← mul_assoc, ← rpow_of_add_eq _ one_ne_zero, rpow_one]

Goal state after:
case inr.calc_1.e_f
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
i : ι
⊢ 1 - p⁻¹ + p⁻¹ = 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, g i ^ q) ^ (r / q) ≤ (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
· gcongr
      exact hg.sum_le_tsum _ (fun _ _ => zero_le)

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

Goal state before:
pp: case pos
α : 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 ∂μ < ∞
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
simp_rw [h1, one_div_one, ENNReal.rpow_one]

Goal state after:
case pos
α : 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 ∂μ < ∞
h1 : p = 1
⊢ ∫⁻ (a : α), (f + g) a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
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 (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
by
  induction s using cons_induction with
  | empty =>
    by_cases hμ : μ = 0 <;>
      simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]
  | cons i s hi ih =>
    rw [prod_cons]
    exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
⊢ ∃ C ≤ A + B, HasSum (fun i ↦ (f i + g i) ^ p) (C ^ p)

Tactic:
by
  have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'
  obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable
  have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp']
  have hB : B = (∑' i : ι, g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp']
  refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩
  · simpa [hA, hB] using H₂
  · simpa only [rpow_self_rpow_inv hp'] using H₁.hasSum

Goal state after:
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
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))

Tactic:
rw [← hxg, funext fun n => hxf n]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

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

Tactic:
rw [← hx] at hf

Goal state after:
case pos
𝕜 : 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
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hf : Filter.comap (⇑f) (𝓝 (f x)) ≤ 𝓝 0
hx : f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ * ‖x‖ * ‖y‖ ≤ max ‖f‖ 1 * ‖x‖ * ‖y‖

Tactic:
by
          gcongr; apply le_max_left

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

Goal state before:
pp: case h₁
𝕜 : 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)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    {a | Continuous[Pi.topologicalSpace, inst✝³.toTopologicalSpace] ((toFun {s | IsVonNBounded 𝕜 s}) a)}

Tactic:
exact UniformOnFun.isClosed_setOfPred_continuous h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype] ⇑(p.quotientEquivOfIsCompl q h)

Tactic:
by
  rw [p.isQuotientMap_mkQL.continuous_iff, isTopCompl_comm]
  exact h.symm.isTopCompl_iff_projectionOnto

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t (μ.restrict s)
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
by
  simp only [measureReal_def, restrict_apply₀ ht]

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i ↦ (s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (⋂ i, s i).mulIndicator f a

Tactic:
exact hs.piecewise_eventually_eq_iInter f 1 a

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
⊢ MemLp.toLp (s.indicator fun x ↦ c) ⋯ + MemLp.toLp (s.indicator fun x ↦ c') ⋯ =
    MemLp.toLp (s.indicator fun x ↦ c + c') ⋯

Tactic:
← MemLp.toLp_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 (s.indicator fun x ↦ c + c') ⋯
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 ≠ ∞
⊢ dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖

Tactic:
by
  -- Squeezed for performance reasons
  simp only [Lp.dist_edist, edist_indicatorConstLp_eq_enorm, enorm, ENNReal.coe_toReal,
    Lp.coe_nnnorm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
by
  simpa using hf.integrable_norm_rpow (mod_cast hp) (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
h : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (μ.restrict univ)

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
h : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

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

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
⊢ Integrable f μ ↔ Integrable f μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
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 ι = n + 1
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
Z : finrank 𝕜 ↥f.range + finrank 𝕜 ↥f.ker = n + 1
this : finrank 𝕜 ↥f.range = 1
⊢ finrank 𝕜 ↥f.ker = n

Tactic:
rw [this, add_comm, Nat.add_one] at Z

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
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 ι = n + 1
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
Z : (finrank 𝕜 ↥f.ker).succ = n + 1
this : finrank 𝕜 ↥f.range = 1
⊢ finrank 𝕜 ↥f.ker = n
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 : ContinuousMultilinearMap 𝕜 E 𝕜
z : G
⊢ ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊

Tactic:
by
  refine le_antisymm ?_ ?_
  · refine opNNNorm_le_iff.2 fun m => (nnnorm_smul_le _ _).trans ?_
    rw [mul_right_comm]
    gcongr
    exact le_opNNNorm _ _
  · obtain hz | hz := eq_zero_or_pos ‖z‖₊
    · simp [hz]
    rw [← le_div_iff₀ hz, opNNNorm_le_iff]
    intro m
    rw [div_mul_eq_mul_div, le_div_iff₀ hz]
    refine le_trans ?_ ((f.smulRight z).le_opNNNorm m)
    rw [smulRight_apply, nnnorm_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst✝³] ↑p
hq : FiniteDimensional 𝕜 ↥q
⊢ FiniteDimensional 𝕜 (E ⧸ p)

Tactic:
exact (p.quotientEquivOfIsCompl q h).symm.finiteDimensional

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 μ)
⊢ Integrable (↑↑f) μ

Tactic:
rw [← memLp_one_iff_integrable]
  exact Lp.memLp f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal |f a|

Tactic:
abs_of_nonneg h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal (f a)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ AEStronglyMeasurable (fun x ↦ (approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ

Tactic:
· apply (SimpleFunc.aestronglyMeasurable _).sub
    apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩).aestronglyMeasurable
    exact .mono (.of_subtype (range f ∪ {0})) subset_union_left

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝ : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
z : ℤ
⊢ t ^ z ~[l] u ^ z

Tactic:
by
  match z with
  | Int.ofNat _ => simpa using h.pow _
  | Int.negSucc _ => simpa using (h.pow _).inv

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : SeminormedAddCommGroup W
inst✝¹ : PseudoMetricSpace Q
inst✝ : NormedAddTorsor W Q
x y : P × Q
⊢ dist x y = ‖x -ᵥ y‖

Tactic:
simp only [Prod.dist_eq, NormedAddTorsor.dist_eq_norm', Prod.norm_def, Prod.fst_vsub,
      Prod.snd_vsub]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:

Tactic:
∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ := by
                  refine integral_mono_ae ?lhs ?rhs ?ae_le
                  case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq
                  case rhs => fun_prop (disch := aesop)
                  case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
            _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)
            _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]

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

Goal state before:
pp: case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
⊢ Disjoint (support ⇑f) (support ⇑f') →
    (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g) →
      (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g) →
        ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑(f + f')) p μ → ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g

Tactic:
hff'

Goal state after:
case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
⊢ (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g) →
    (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g) →
      ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑(f + f')) p μ → ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp (⇑(f + f')) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
⊢ ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g

Tactic:
rw [SimpleFunc.coe_add,
      memLp_add_of_disjoint hff' f.stronglyMeasurable f'.stronglyMeasurable] at int_ff'

Goal state after:
case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp (⇑f) p μ ∧ MemLp (⇑f') p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
⊢ ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case H
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (A ∘SL coeToLp α E ℝ) f = (setToL1SCLM α E μ hT) f

Tactic:
hA f

Goal state after:
case H
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (A ∘SL coeToLp α E ℝ) f = A ↑f