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

Goal state before:
pp: case neg
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ (ε ^ p.toReal)⁻¹ * eLpNorm f p μ ^ p.toReal

Tactic:
← ENNReal.mul_le_mul_iff_right hεpow hεpow',

Goal state after:
case neg
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ ε ^ p.toReal * μ {x | ε ≤ ‖f x‖ₑ} ≤ ε ^ p.toReal * ((ε ^ p.toReal)⁻¹ * eLpNorm f p μ ^ p.toReal)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
⊢ (Measure.pi μ) U ≠ 0

Tactic:
obtain ⟨s, ⟨hs, hsU⟩⟩ := isOpen_pi_iff'.1 U_open a ha

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst✝¹ a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : univ.pi s ⊆ U
⊢ (Measure.pi μ) U ≠ 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ∞
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
refine ⟨s, hsm, hs, ?_⟩

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ∞
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ eLpNorm (sᶜ.indicator f) p μ < ε
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ

Tactic:
by
  simp_rw [eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply, enorm_smul,
    ENNReal.essSup_const_mul]

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

Goal state before:
pp: case h₁
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ ↑C ≤ ‖f x‖ₑ

Tactic:
coe_le_enorm

Goal state after:
case h₁
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ C ≤ ‖f x‖₊
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) (Measure.pi μ) (Measure.dirac ())

Tactic:
set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit
  refine ⟨e.measurable, ?_⟩
  rw [Measure.pi_of_empty, Measure.map_dirac' e.measurable]

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
by
  simp [inv_add_inv_eq_inv p q r]

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
hyz : a * x + b * z < z
key : (f (a * x + b * z) - f x) * (z - (a * x + b * z)) ≤ (a * x + b * z - x) * (f z - f (a * x + b * z))
⊢ f (a * x + b * z) ≤ a * f x + b * f z

Tactic:
apply le_of_mul_le_mul_left ?_ (sub_pos.2 hxz)

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
hyz : a * x + b * z < z
key : (f (a * x + b * z) - f x) * (z - (a * x + b * z)) ≤ (a * x + b * z - x) * (f z - f (a * x + b * z))
⊢ (z - x) * f (a * x + b * z) ≤ (z - x) * (a * f x + b * f z)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:

Tactic:
exp y * (z - y) < exp y * (exp (z - y) - 1) := by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']
      _ = exp (z - y) * exp y - exp y := by ring
      _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl

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

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Iio 0) log

Tactic:
refine ⟨convex_Iio _, ?_⟩
  intro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
  have hx' : 0 < -x := by linarith
  have hy' : 0 < -y := by linarith
  have hxy' : -x ≠ -y := by contrapose hxy; linarith
  calc
    a • log x + b • log y = a • log (-x) + b • log (-y) := by simp_rw [log_neg_eq_log]
    _ < log (a • -x + b • -y) := strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab
    _ = log (-(a • x + b • y)) := by congr 1; simp only [smul_eq_mul]; ring
    _ = _ := by rw [log_neg_eq_log]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

Tactic:
by rw [monovaryOn_iff_forall_smul_nonneg]; rfl

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)
a : α
⊢ (f * g) a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)

Tactic:
Pi.mul_apply,

Goal state after:
α : 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)
a : α
⊢ f a * g a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case insert.inl
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
simp only [hi₀, not_false_eq_true, prod_insert]

Goal state after:
case insert.inl
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ^ (1 / p)

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ (∫⁻ (a : α), (f a * g a) ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p) / ↑p.toNNReal + ↑(b.toNNReal ^ q) / ↑q.toNNReal

Tactic:
←
    @coe_div (Real.toNNReal p) _ (by simp [hpq.pos]),

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p / p.toNNReal) + ↑(b.toNNReal ^ q) / ↑q.toNNReal
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 μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), ↑((f * g) a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), ↑(f a * g a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
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
inst✝ : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ.real {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
rw [tendstoInMeasure_iff_norm]
  congr! with ε hε hε_top
  simp_rw [measureReal_def, ENNReal.tendsto_toReal_zero_iff (fun _ ↦ measure_ne_top _ _)]

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)

pp: case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
· have hf : (fun i => (μ { x | ε ≤ edist (f i x) (g x) }).toNNReal) =
        ENNReal.toNNReal ∘ (fun i ↦ (μ { x | ε ≤ edist (f i x) (g x) })) := rfl
    rw [hf, ENNReal.tendsto_toNNReal_iff' (hfin ε)]
    exact h ε hε

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4.e'_5.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
x✝ : ι
a✝ : x✝ ∈ s
⊢ f x✝ = |f x✝|

pp: case e'_4.e'_6.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
x✝ : ι
a✝ : x✝ ∈ s
⊢ g x✝ = |g x✝|

Tactic:
all_goals
    exact Eq.symm (abs_of_nonneg (by grind))

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i ↦ f (i + 1) x - f i x

Tactic:
have h1 :
      ∀ n, eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i :=
      eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' hf hp1 h_cau

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 : ∀ (n : ℕ), eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ ∀ᵐ (x : α) ∂μ, Summable fun i ↦ f (i + 1) x - f i x
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
⊢ Disjoint (Set.range ⇑a) (Set.range ⇑f) ↔ Set.range ⇑f ⊆ (Set.range ⇑a)ᶜ

Tactic:
Set.subset_compl_iff_disjoint_right,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
⊢ Disjoint (Set.range ⇑a) (Set.range ⇑f) ↔ Disjoint (Set.range ⇑f) (Set.range ⇑a)
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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m_1 ↦ eLpNorm (f n - f m_1) p μ) atTop
N1 : ℕ
⊢ eLpNorm (f n - f (max N N1)) p μ ≤ ε

Tactic:
exact (h_cau N n (max N N1) hn (le_max_left _ _)).le.trans h_B

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

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

Tactic:
mul_smul,

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
⊢ IsBoundedLinearMap 𝕜 fun e ↦ f e - g e

Tactic:
by simpa [sub_eq_add_neg] using add hf (neg hg)

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

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

Tactic:
rw [measureReal_sdiff' h₂ h₁ (measure_ne_top_of_subset h h₁), union_eq_self_of_subset_right h]

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₃ : ∀ x ∈ s, l x ≠ 0
hl : Dense ↑l.ker
x : E
hx : x ∈ s
this : x ∈ interior (↑l.ker)ᶜ
⊢ False

Tactic:
hl.interior_compl

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₃ : ∀ x ∈ s, l x ≠ 0
hl : Dense ↑l.ker
x : E
hx : x ∈ s
this : x ∈ ∅
⊢ False
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case mp
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ → IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Tactic:
exact fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩

Goal state after:
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 = finrank 𝕜 E
⊢ finrank 𝕜 ↥f.ker = n

Tactic:
finrank_eq_card_basis ξ,

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.range + finrank 𝕜 ↥f.ker = Fintype.card ι
⊢ finrank 𝕜 ↥f.ker = n