mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ openSegment 𝕜 x z

Tactic:
openSegment_eq_Ioo (hxy.trans hz.2)

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ Set.Ioo x z
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Ici y)

Tactic:
intro u hu v hv huv
  have step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z := by
    intro z hz
    refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
    rw [openSegment_eq_Ioo (hxy.trans hz.2)]
    exact ⟨hxy, hz.2⟩
  rcases eq_or_lt_of_le hu.2 with (rfl | hu2)
  · exact step1 ⟨hv.1, huv⟩
  · refine hf.lt_right_of_left_lt ?_ hv.1 ?_ (step1 ⟨hu.1, hu2⟩)
    · apply hf.1.segment_subset hx hu.1
      rw [segment_eq_Icc (hxy.le.trans hu.2)]
      exact ⟨hxy.le, hu.2⟩
    · rw [openSegment_eq_Ioo (hu2.trans huv)]
      exact ⟨hu2, huv⟩

Goal state after:
Module: Mathlib.Order.Monotone.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ Monovary (fun i ↦ f ↑i) fun i ↦ g ↑i

Tactic:
by
  simp [Monovary, MonovaryOn]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
calc
    _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
    _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
        convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) <| by ring
    _ = _ := by rw [cosh_eq, sinh_eq]; ring

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
hp : 0 ≤ p
hp1 : p ≤ 1
a b : ℝ≥0
⊢ (↑a + ↑b) ^ p ≤ ↑a ^ p + ↑b ^ p

Tactic:
exact_mod_cast NNReal.rpow_add_le_add_rpow a b hp hp1

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

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
have :
    Tendsto (fun η : ℝ≥0∞ => LpAddConst p * (η + η)) (𝓝[>] 0)
        (𝓝 (LpAddConst p * (0 + 0))) :=
    (ENNReal.Tendsto.const_mul (tendsto_id.add tendsto_id)
          (Or.inr (LpAddConst_lt_top p).ne)).mono_left
      nhdsWithin_le_nhds

Goal state after:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 (p.LpAddConst * (0 + 0)))
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ 0 ≤ q⁻¹

Tactic:
by simp [hq_pos.le]

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

Goal state before:
pp: case refine_2
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst✝ : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a ↦ ∑ i ∈ s, f i a) p μ) →
        (∀ i ∈ insert a s, MemLp (f i) p μ) → MemLp (fun a_3 ↦ ∑ i ∈ insert a s, f i a_3) p μ

Tactic:
· intro i s his ih hf
    simp only [his, Finset.sum_insert, not_false_iff]
    exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Goal state after:
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 = ∞
⊢ eLpNorm f p μ < ∞

pp: case neg
α : 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 = ∞
⊢ eLpNorm f p μ < ∞

Tactic:
· have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq
    rw [hp_top]
    rwa [hq_top] at hfq_lt_top

Goal state after:
case neg
α : 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 = ∞
⊢ eLpNorm f p μ < ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
⊢ a * b = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q ↔ a = ∞ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ∞ ∨ a ^ p = b ^ q

Tactic:
by_cases! h0 : a = 0 ∨ b = 0
  · rcases h0 with rfl | rfl <;> simp [hpq.pos, hpq.symm.pos, eq_comm]
  by_cases! h : a = ⊤ ∨ b = ⊤
  · rcases h with rfl | rfl <;> simp [hpq.pos, hpq.symm.pos, h0, div_eq_mul_inv]
  rw [← coe_toNNReal h.left, ← coe_toNNReal h.right, ← coe_mul, ← coe_rpow_of_nonneg _ hpq.nonneg,
    ← coe_rpow_of_nonneg _ hpq.symm.nonneg, ← ofNNReal_toNNReal, ← ofNNReal_toNNReal,
    ← coe_div (by simp [hpq.pos]), ← coe_div (by simp [hpq.symm.pos]), ← coe_add, coe_inj, coe_inj]
  simp [young_inequality_real_eq_iff a.toNNReal b.toNNReal hpq]

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
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
tendstoInMeasure_iff_dist,

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ (∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
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))
⊢ TendstoInMeasure μ f atTop g

Tactic:
by
  have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
  refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
  refine tendstoInMeasure_of_tendsto_ae_of_measurable_edist
    (fun n ↦ ((hf n).stronglyMeasurable_mk.edist hg.stronglyMeasurable_mk).measurable) ?_
  have hf_eq_ae : ∀ᵐ x ∂μ, ∀ n, (hf n).mk (f n) x = f n x :=
    ae_all_iff.mpr fun n => (hf n).ae_eq_mk.symm
  filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg
  rw [← hxg, funext fun n => hxf n]
  exact hxfg

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
⊢ ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝ → ↑↑g₁ a✝ ≤ ↑↑g₂ a✝ → ↑↑(f + g₁) a✝ ≤ ↑↑(f + g₂) a✝

Tactic:
h2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
rw [Subsingleton.elim emb Embedding.fintype]
  refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α <;> clear! α
  · let := Fintype.ofEquiv _ e.symm
    rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
  · rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]
    exact ⟨Embedding.ofIsEmpty, fun x ↦ DFunLike.ext _ _ isEmptyElim⟩
  · classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 ↦ -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
ht' : (1 + ↑x⁻¹ * t)⁻¹ʳ = ∑ i ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * (1 + ↑x⁻¹ * t)⁻¹ʳ
| (∑ i ∈ range n, (-(↑x⁻¹ * t)) ^ i) * ↑x⁻¹ + (-(↑x⁻¹ * t)) ^ n * (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
← neg_mul,

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 ↦ -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
ht' : (1 + ↑x⁻¹ * t)⁻¹ʳ = ∑ i ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * (1 + ↑x⁻¹ * t)⁻¹ʳ
| (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case inr
𝕜 : 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
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
⊢ C * ‖x‖ * ‖y‖ ≤ C * 1 * ‖y‖

Tactic:
hx.2.le

Goal state after:
case inr
𝕜 : 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
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
⊢ C * 1 * ‖y‖ ≤ C * 1 * ‖y‖
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
f T : M →L[R] M
hT : IsUnit T
hf : IsIdempotentElem f
this : IsUnit (toLinearMapRingHom T)
⊢ Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker

Tactic:
lift T to (M →L[R] M)ˣ using hT

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
f : M →L[R] M
hf : IsIdempotentElem f
T : (M →L[R] M)ˣ
this : IsUnit (toLinearMapRingHom ↑T)
⊢ Commute f ↑T ↔ Submodule.map (↑↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑↑T) (↑f).ker = (↑f).ker
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
hc : IsClosedMap f
h_cont : Continuous[inst✝¹, inst✝] f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
exact (hc.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
    h_cont.rangeFactorization Set.rangeFactorization_surjective

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) = μ.real s + μ.real t

Tactic:
by
  rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hm : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s \ t) = μ.real (s ∪ t) - μ.real t

Tactic:
by
  rw [union_comm, ← measureReal_add_sdiff hm h₂ h₁]
  ring

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ Integrable (↑↑(indicatorConstLp p hs hμs c)) μ

Tactic:
by
  rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn,
    integrable_const_iff, isFiniteMeasure_restrict]
  exact .inr hμs

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

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

Tactic:
· simpa [aemeasurable_withDensity_ennreal_iff hf, enorm_smul] using H.enorm

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable (fun x ↦ (f x).toNNReal • g x) μ ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
simp_rw [NNReal.smul_def, ENNReal.toReal]

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
⊢ False

Tactic:
have : μ.restrict v v < ∞ := lt_of_le_of_lt (measure_mono inter_subset_right)
    (Integrable.measure_gt_lt_top hv.norm εpos)

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 < ∞
⊢ False
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
⊢ Integrable (fun x ↦ RCLike.im (f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢
  exact hf.im

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
⊢ ‖{ toFun := fun m ↦ (f m).mkContinuous (C * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ }.mkContinuous
        (max C 0) ⋯‖ ≤
    max C 0

Tactic:
exact mkContinuous_norm_le _ (le_max_right _ _) _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, μ (S i) ≠ ∞
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

Tactic:
by
  classical
  revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  rw [←
    h_add (S a) (⋃ i ∈ s, S i) (hS_meas a) (measurableSet_biUnion _ fun i _ => hS_meas i)
      (hps a (Finset.mem_insert_self a s))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • μ s = ∞ → μ s = ∞
⊢ DominatedFinMeasAdditive μ T (c.toReal * C)

Tactic:
refine ⟨hT.1.of_eq_top_imp_eq_top (μ := c • μ) h, fun s hs hμs => ?_⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • μ s = ∞ → μ s = ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ‖T s‖ ≤ c.toReal * C * μ.real s
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ f.extendOfNorm e = g

Tactic:
by
  apply ContinuousLinearMap.extend_unique
  · simpa using! h_dense
  · exact isUniformEmbedding_subtype_val.isUniformInducing
  ext ⟨y, x, hxy⟩
  rw [compLeftInverse_apply_of_bdd _ _ ⟨C, h_norm⟩ x y hxy]
  simp [← hxy, ← H]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : Nonempty α
T : Set α → F →L[ℝ] F'
x : F
m : MeasurableSpace α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

Tactic:
simp only [setToSimpleFunc, range_const, Set.mem_singleton, preimage_const_of_mem,
    sum_singleton, ← Function.const_def, coe_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x ↦ -u x) ~[l] fun x ↦ -v x

Tactic:
rw [IsEquivalent]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ ((fun x ↦ -u x) - fun x ↦ -v x) =o[l] fun x ↦ -v x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = L1.integral (Integrable.toL1 (⇑f) hfi)

Tactic:
← L1.SimpleFunc.toLp_one_eq_toL1,

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = L1.integral ↑(f.toLp ⋯)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖((fun x ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖

Tactic:
by
      simp [sub_smul, sub_add]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h_eq : ∀ (x : α), |f x| = 2 * max (-f x) 0 + f x
⊢ ∫ (a : α), 2 * max (-f a) 0 + f a ∂μ = 2 * ∫ (x : α), max (-f x) 0 ∂μ + ∫ (x : α), f x ∂μ

Tactic:
integral_add (by fun_prop) hf,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h_eq : ∀ (x : α), |f x| = 2 * max (-f x) 0 + f x
⊢ ∫ (a : α), 2 * max (-f a) 0 ∂μ + ∫ (a : α), f a ∂μ = 2 * ∫ (x : α), max (-f x) 0 ∂μ + ∫ (x : α), f x ∂μ