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

Goal state before:
pp: case mp
α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c → a = 0 ∧ c = 0

pp: case mpr
α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c

Tactic:
· intro h
    exact
      ⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
        (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩

Goal state after:
case mpr
α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ ↔ c = 0 ∨ μ Set.univ < ∞

Tactic:
rw [memLp_const_iff_enorm enorm_ne_top hp_ne_zero hp_ne_top]; simp

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ (if p = 0 then 0 else if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ∞ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝ : p = 0
⊢ 0 ≤ 0

case pos
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝¹ : ¬p = 0
h✝ : p = ∞
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

case neg
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝¹ : ¬p = 0
h✝ : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C

Tactic:
rw [← mul_comm]
  exact eLpNorm_le_of_ae_nnnorm_bound (hfC.mono fun x hx => hx.trans C.le_coe_toNNReal)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ MemLp f p μ

Tactic:
apply (memLp_const_enorm hC).of_le_enorm (ε' := ℝ≥0∞) hf <| hfC.mono fun _x hx ↦ ?_
  rw [enorm_eq_self]; exact hx

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Tactic:
eLpNorm'_smul_measure ENNReal.toReal_nonneg

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ

Tactic:
eLpNorm_smul_measure_of_ne_top

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
⊢ c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ

case hp_ne_top
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
⊢ 1 ≠ ∞
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.refine_1
𝕜 : 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
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ segment 𝕜 x u

Tactic:
segment_eq_Icc (hxy.le.trans hu.2)

Goal state after:
case inr.refine_1
𝕜 : 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
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ Set.Icc x u
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 : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f y < f x
⊢ StrictAntiOn f (s ∩ Set.Iic x)

Tactic:
have := hf.comp_affineMap (-.id ..) |>.strictMonoOn (by simpa) (neg_lt_neg hxy) (by simpa)
  simpa [Function.comp_def] using this.comp_strictAntiOn strictMonoOn_id.neg fun _ _ ↦ by simpa

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / ∑ i ∈ s, w i

Tactic:
convert geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz
  · rw [← finsetProd_rpow _ _ (fun i hi => rpow_nonneg (hz _ hi) _) _]
    refine Finset.prod_congr rfl (fun _ ih => ?_)
    rw [div_eq_mul_inv, rpow_mul (hz _ ih)]
  · simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]
  · exact fun _ hi => div_nonneg (hw _ hi) (le_of_lt hw')
  · simp_rw [div_eq_mul_inv, ← Finset.sum_mul]
    exact mul_inv_cancel₀ (by linarith)

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
simp [add_eq_zero.mp h_zero, hp_pos.ne']

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
hf1 : ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
hg1 : ∫⁻ (c : α), funMulInvSnorm g q μ c ^ q ∂μ = 1
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1

Tactic:
exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
hp : 1 ≤ 1
⊢ (∑ i ∈ s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i ∈ s, f i ^ 1) ^ (1 / 1) + (∑ i ∈ s, g i ^ 1) ^ (1 / 1)

pp: case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
· simp [Finset.sum_add_distrib]

Goal state after:
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
← lintegral_add_left' (hf.pow_const p)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)
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
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
suffices ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ by
            -- Squeezed for performance reasons
            simpa only [ge_iff_le, enorm, ← ENNReal.coe_add, ENNReal.coe_le_coe] using! this

Goal state after:
α : 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
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
h_inv_n_le_k : 2⁻¹ ^ n ≤ 2 * 2⁻¹ ^ k
⊢ edist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k

Tactic:
exact le_trans hNx.le h_inv_n_le_k

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
hfg : TendstoInMeasure μ f atTop g
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
by
  /- Since `f` tends to `g` in measure, it has a subsequence `k ↦ f (ns k)` such that
    `μ {|f (ns k) - g| ≥ 2⁻ᵏ} ≤ 2⁻ᵏ` for all `k`. Defining
    `s := ⋂ k, ⋃ i ≥ k, {|f (ns k) - g| ≥ 2⁻ᵏ}`, we see that `μ s = 0` by the
    first Borel-Cantelli lemma.

    On the other hand, as `s` is precisely the set for which `f (ns k)`
    doesn't converge to `g`, `f (ns k)` converges almost everywhere to `g` as required. -/
  have h_lt_ε_real (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ k : ℕ, 2 * (2 : ℝ≥0∞)⁻¹ ^ k < ε := by
    obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ≥0∞)⁻¹ ^ k < ε := ENNReal.exists_inv_two_pow_lt hε.ne'
    refine ⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩
    rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]
    · positivity
    · simp
  set ns := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
  use ns
  let S := fun k => { x | (2 : ℝ≥0∞)⁻¹ ^ k ≤ edist (f (ns k) x) (g x) }
  have hμS_le : ∀ k, μ (S k) ≤ (2 : ℝ≥0∞)⁻¹ ^ k :=
    fun k => ExistsSeqTendstoAe.seqTendstoAeSeq_spec hfg k (ns k) le_rfl
  set s := Filter.atTop.limsup S with hs
  have hμs : μ s = 0 := by
    refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))
    simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top
  have h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) := by
    refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_
    rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
    simp only [S, Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.compl_iInter, Set.compl_iUnion,
      Set.mem_iUnion, Set.mem_iInter, Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hx
    obtain ⟨N, hNx⟩ := hx
    obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
    refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩
    specialize hNx n ((le_max_left _ _).trans hn_ge)
    have h_inv_n_le_k : (2 : ℝ≥0∞)⁻¹ ^ n ≤ 2 * (2 : ℝ≥0∞)⁻¹ ^ k := by
      nth_rw 2 [← pow_one (2 : ℝ≥0∞)]
      rw [mul_comm, ← ENNReal.inv_pow, ← ENNReal.inv_pow, ENNReal.inv_le_iff_le_mul, ← mul_assoc,
        mul_comm (_ ^ n), mul_assoc, ← ENNReal.inv_le_iff_le_mul, inv_inv, ← pow_add]
      · gcongr
        · simp
        · omega
      all_goals simp
    exact le_trans hNx.le h_inv_n_le_k
  rw [ae_iff]
  refine ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => ?_) hμs⟩
  rw [Set.mem_ofPred_eq, ← @Classical.not_not (x ∈ s), not_imp_not]
  exact h_tendsto x

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✝ : α
⊢ ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝ → ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝ → ↑↑g₁ a✝ ≤ ↑↑g₂ a✝ → ↑↑(f + g₁) a✝ ≤ ↑↑(f + g₂) a✝

Tactic:
h1

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✝
⊢ ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝ → ↑↑g₁ a✝ ≤ ↑↑g₂ a✝ → ↑↑(f + g₁) a✝ ≤ ↑↑(f + g₂) a✝
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 : ¬Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ edist (f (ns n) x) (g x)}).toNNReal

Tactic:
obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_notMem.1 h2

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 : ¬Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
s : Set ℝ≥0
hs : s ∈ 𝓝 0
h4 : ∃ᶠ (x : ℕ) in atTop, (μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}).toNNReal ∉ s
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ edist (f (ns n) x) (g x)}).toNNReal
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ∑ i, ‖↑(Set.range ⇑i)ᶜ‖ = (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖

Tactic:
← ih

Goal state after:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ∑ i, ‖↑(Set.range ⇑i)ᶜ‖ = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
refine le_trans ?_ hn

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal
Module: Mathlib.Topology.Algebra.Module.Simple

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
⊢ IsClosed ↑l.ker ∨ Dense ↑l.ker

Tactic:
by
  rcases l.surjective_or_eq_zero with (hl | rfl)
  · exact (LinearMap.ker l).isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)
  · rw [LinearMap.ker_zero]
    left
    exact isClosed_univ

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := ⋯
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ O ⁻¹' {x | IsUnit x} → f' ∈ range toContinuousLinearMap

Tactic:
rintro ⟨w, hw⟩

Goal state after:
case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
⊢ f' ∈ range toContinuousLinearMap
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : μ s₂ = 0
h'₂ : μ s₂ ≠ ∞
⊢ μ.real s₁ = 0

Tactic:
simp [Measure.real, measure_mono_null h h₂]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : μ u ≠ ∞
⊢ μ s + μ t ≠ ∞

Tactic:
exact ENNReal.add_ne_top.2 ⟨measure_ne_top_of_subset h's hu, measure_ne_top_of_subset h't hu⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᵐ[μ] fun a ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 ↦ x) =ᵐ[μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Tactic:
refine EventuallyEq.trans ?_ h_compLp.symm

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᵐ[μ] fun a ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 ↦ x) =ᵐ[μ] fun a ↦ (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ Integrable (fun x_1 ↦ f x) (μ.restrict {x}) ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞

Tactic:
integrable_const_iff_enorm,

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ ‖f x‖ₑ = 0 ∨ IsFiniteMeasure (μ.restrict {x}) ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞

α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ ‖f x‖ₑ ≠ ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊔ g) 1 μ

Tactic:
exact hf.sup hg

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 : α → β
hf : AEStronglyMeasurable f μ
⊢ Integrable (fun a ↦ ‖f a‖) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]

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

Goal state before:
pp: case inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖

Tactic:
have : 0 < (‖c‖ / ε) ^ Fintype.card ι := pow_pos (div_pos (zero_lt_one.trans hc) ε0) _

Goal state after:
case inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ Integrable (fun x ↦ f x • c) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff,
    hasFiniteIntegral_iff_enorm, enorm_smul]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ → (∫⁻ (a : α), ‖f a‖ₑ * ‖c‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞)