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

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f g : α →ₛ E
⊢ Disjoint (support ⇑f) (support ⇑g) →
    (∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)) →
      (∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)) → ∀ (hf : MemLp (⇑(f + g)) p μ), P ((f + g).toLp hf)

Tactic:
hfg

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
⊢ (∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)) →
    (∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)) → ∀ (hf : MemLp (⇑(f + g)) p μ), P ((f + g).toLp hf)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
⊢ f ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range Subtype.val)

Tactic:
rw [mem_closure_iff_seq_limit]

Goal state after:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ g ∈ closure[instTopologicalSpaceSubtype] (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))

Tactic:
rw [mem_closure_iff_seq_limit]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : 0 ≤ f y
⊢ 0 ≤ μ.real (⇑f ⁻¹' {f y}) • f y

Tactic:
positivity

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

Goal state before:
pp: α : 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 α
T T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T f = setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc]
  refine sum_congr rfl fun x _ => ?_
  by_cases hx0 : x = 0
  · simp [hx0]
  · rw [h (f ⁻¹' {x}) (SimpleFunc.measurableSet_fiber _ _)
        (SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hx0)]

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

Goal state before:
pp: α : 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 α
T T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x

Tactic:
rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.indicator (Function.const α x) ⁻¹' {x} = s

Tactic:
rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ (0 ⁻¹' {x}) = s

case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
⊢ Disjoint (support ⇑f) (support ⇑g) →
    (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)

Tactic:
hfg

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
⊢ (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)
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) μ
⊢ ∫ (x : α), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
← f.integral_eq_integral hfi,

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 = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Tactic:
rw [integrable_congr hfg] at hfi

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

Tactic:
rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
        hε with ⟨g, _, Pg⟩
    exact ⟨g, by simp, Pg⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
this : f =ᵐ[μ] fun x ↦ ‖f x‖
⊢ ENNReal.ofReal (∫ (a : α), ‖f a‖ ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
ofReal_integral_norm_eq_lintegral_enorm hfi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
this : f =ᵐ[μ] fun x ↦ ‖f x‖
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
x✝ : X
⊢ 0 x✝ ≤ (fun a ↦ ‖f a‖) x✝

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
a : α
ha : ∀ (i : ℕ), F a ≤ f i a
i : ℕ
⊢ f' i a ≤ F' a

Tactic:
simp [f', F', ha i]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
x : α
⊢ 0 x ≤ (fun a ↦ ‖f a‖ ^ p.toReal) x

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
⊢ ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
by
  rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ
  · simpa [measureReal_def, hμ] using integral_nonneg_of_ae hf_nonneg
  · have := Fact.mk hμ
    calc
      ε * μ.real { x | ε ≤ f x } = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
      _ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
        integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
          ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici
      _ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
⊢ 0 x ≤ (fun a ↦ ‖g a‖ ^ q) x

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
⊢ 0 x ≤ (fun a ↦ ‖f a‖ ^ p) x

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
⊢ 0 x ≤ (fun a ↦ ‖f a‖ * ‖g a‖) x

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ 0 ≤ dist c₁ c₂ * dist f 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
f g : α →ᵇ R
⊢ 0 ≤ ‖f‖ * ‖g‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: case hc
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ 0 ≤ max ‖f‖ ‖g‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: case hc
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ 0 ≤ ‖f + g‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' :
  x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
⊢ infDist x Kᶜ = dist x x

Tactic:
Metric.infDist_zero_of_mem_closure hx'.2,

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' :
  x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
⊢ 0 = dist x x
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ 0 ≤ ‖⇑f‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ 0 ≤ ‖f‖

Tactic:
positivity

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

Goal state before:
pp: case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
⊢ dist g f < ε / 2 / c'.toReal → dist (Integrable.toL1 ↑↑g ⋯) (Integrable.toL1 ↑↑f ⋯) < ε

Tactic:
hfg

Goal state after:
case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : dist g f < ε / 2 / c'.toReal
⊢ dist (Integrable.toL1 ↑↑g ⋯) (Integrable.toL1 ↑↑f ⋯) < ε
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_ae
α : 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 α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
⊢ f₂ =ᵐ[μ] g₂ → Integrable f₂ μ → setToFun μ T hT f₂ = setToFun μ' T hT' f₂ → setToFun μ T hT g₂ = setToFun μ' T hT' g₂

Tactic:
hfg

Goal state after:
case pos.h_ae
α : 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 α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
⊢ Integrable f₂ μ → setToFun μ T hT f₂ = setToFun μ' T hT' f₂ → setToFun μ T hT g₂ = setToFun μ' T hT' g₂
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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 α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
hF : ¬CompleteSpace F
⊢ 0 ≤ C * ‖f‖

Tactic:
positivity

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

Goal state before:
pp: case neg
α : 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 α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hF : ¬CompleteSpace F
⊢ 0 ≤ max C 0 * ‖f‖

Tactic:
positivity

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

Goal state before:
pp: case neg
α : 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
hF : ¬CompleteSpace F
⊢ 0 ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
positivity

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

Goal state before:
pp: case neg
α : 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hF : ¬CompleteSpace F
⊢ 0 ≤ max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
positivity

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

Goal state before:
pp: case neg
α : 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : ¬CompleteSpace F
⊢ 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
positivity

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

Goal state before:
pp: case neg
α : 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
positivity

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, f ∂μ ∂μ = ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, g ∂μ ∂μ

Tactic:
hfg

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, g ∂μ ∂μ = ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, g ∂μ ∂μ
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
refine ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
a b : R
h : IsTop b
x : R
hx : x ∈ Ioi a
⊢ x ∈ Ioc a b

Tactic:
by exact ⟨hx, h _⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
⊢ f.outer (Ioc a b) ≤ f.length (Ioc a b)

Tactic:
apply outer_le_length

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
⊢ ↑K ⊆ ⋃ i, ↑(U i)

Tactic:
← Opens.coe_iSup

Goal state after:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
⊢ ↑K ⊆ ↑(⨆ i, U i)