mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  (MeasurableEquiv.piEquivPiSubtypeProd α p).symm
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
this : ⇑e ⁻¹' univ.pi s = (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i
⊢ (∏ i, (μ ↑i) (s ↑i)) * ∏ i, (μ ↑i) (s ↑i) = ∏ i, (μ i) (s i)

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  (MeasurableEquiv.piEquivPiSubtypeProd α p).symm
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
this : ⇑e ⁻¹' univ.pi s = (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i
⊢ (∏ i, (μ ↑i) (s ↑i)) * ∏ i, (μ ↑i) (s ↑i) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ Function.support (f - g) ⊆ s

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ Function.support (f - g) ⊆ s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm 0 p μ = 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm 0 p μ = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
⊢ 0 < ∞

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
⊢ 0 < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ i) (s i) = ∏ i, (μ i) (s i)

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm f p 0 = 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm f p 0 = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
]

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i ↦ (μ i).prod (ν i))
      (⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β) ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t))

Tactic:
]

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i ↦ (μ i).prod (ν i))
      (⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β) ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t))
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
]

Goal state after:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ = ‖c‖ₑ

Tactic:
]

Goal state after:
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, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
obtain ⟨s, hsm, hs, hε⟩ :
        ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in sᶜ, (‖f a‖ₑ) ^ p.toReal ∂μ < ε ^ p.toReal := by
      apply exists_setLIntegral_compl_lt
      · exact ((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne
      · simp [*]

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
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ

Tactic:
]

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i ↦ (μ i).prod (ν i)) (univ.pi fun i ↦ s i ×ˢ t i)

Tactic:
]

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i ↦ (μ i).prod (ν i)) (univ.pi fun i ↦ s i ×ˢ t i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)

pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ q ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)

α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ q ≠ ∞
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
⊢ ∫⁻ (x : α) in sᶜ, ‖f x‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal

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
⊢ 0 < p.toReal

Tactic:
]

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
⊢ ∫⁻ (x : α) in sᶜ, ‖f x‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal

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
⊢ 0 < p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
]

Goal state after:
case e_a
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
hp_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ = ‖c‖ₑ

Tactic:
]

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

Goal state before:
pp: case e_a
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ε
hμ : μ ≠ 0
⊢ ‖c‖ₑ = ‖c‖ₑ

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ

Tactic:
]

Goal state after:
case pos
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ‖c‖ₑ = 0
⊢ ∫⁻ (a : α), ‖c‖ₑ ^ p.toReal ∂μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
]

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ‖c‖ₑ = 0
⊢ ∫⁻ (a : α), ‖c‖ₑ ^ p.toReal ∂μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case mpr
α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
b : α
hb : b < 0
ha hc : 0 ≤ 0
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
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 z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) =
    ((μ i).prod (Measure.pi fun i_1 ↦ μ (i.succAbove i_1))) (s i ×ˢ univ.pi fun i_1 ↦ s (i.succAbove i_1))

Tactic:
]

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) =
    ((μ i).prod (Measure.pi fun i_1 ↦ μ (i.succAbove i_1))) (s i ×ˢ univ.pi fun i_1 ↦ s (i.succAbove i_1))
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ ‖c‖ₑ < ∞ ∧ μ Set.univ ^ (1 / p.toReal) < ∞ ∨ ‖c‖ₑ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
]

Goal state after:
case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ ‖c‖ₑ < ∞ ∧ μ Set.univ ^ (1 / p.toReal) < ∞ ∨ ‖c‖ₑ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ (μ default) (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ (μ default) (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞

Tactic:
]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : 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‖₊
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
]

Goal state after:
α : 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‖₊
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
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 ≠ ∞
⊢ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞

Tactic:
]

Goal state after:
α : 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 ≠ ∞
⊢ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * (μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) = (μ 0) s * (μ 1) t

Tactic:
]

Goal state after:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * (μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) = (μ 0) s * (μ 1) t
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Measure.dirac (e fun a ↦ isEmptyElim a) = Measure.dirac ()

Tactic:
]

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:
]

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‖₊