mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ((c₁ + c₂) • f) x = (c₁ • f + c₂ • f) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
f : C(α, M)
⊢ 0 • f = 0

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
f : C(α, M)
x : α
⊢ (0 • f) x = 0 x
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous[inst✝¹, inst✝] g
f : α →ₘ[μ] β
⊢ ↑(comp g hg f) =ᵐ[μ] g ∘ ↑f

Tactic:
rw [comp_eq_mk]
  apply coeFn_mk

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
⊢ (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

Tactic:
rcases g

Goal state after:
case mk
α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) f hf).toGerm =
    (toGerm (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compTendsto f ⋯
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : 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∞
⊢ (fun x ↦ ε ≤ ‖f x‖ₑ) = fun x ↦ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
ext x

Goal state after:
α : 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∞
x : α
⊢ ε ≤ ‖f x‖ₑ ↔ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun x i ↦ f i (x i)) ⁻¹' univ.pi s = univ.pi fun i ↦ f i ⁻¹' s i

Tactic:
ext x

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
x : (i : ι) → X i
⊢ x ∈ (fun x i ↦ f i (x i)) ⁻¹' univ.pi s ↔ x ∈ univ.pi fun i ↦ f i ⁻¹' s i
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
⊢ ⇑e_meas ⁻¹' univ.pi s = (univ.pi fun i ↦ s (some i)) ×ˢ s none

Tactic:
ext x

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
⊢ x ∈ ⇑e_meas ⁻¹' univ.pi s ↔ x ∈ (univ.pi fun i ↦ s (some i)) ×ˢ s none
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : 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 : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
← ENNReal.rpow_le_rpow_iff hp,

Goal state after:
α : 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 : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : 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 : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
← ENNReal.rpow_le_rpow_iff hp,

Goal state after:
α : 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 : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

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

Tactic:
simp [hp]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
← ENNReal.rpow_le_rpow_iff hp,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (c * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
suffices p = 0 by simpa [this]

Goal state after:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ p = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : p = 0
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
simp [hp]

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

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p < ∞ ↔ 1 < q

Tactic:
rw [lt_top_iff_ne_top, ne_top_iff_ne_one _ q, ne_comm, lt_iff_le_and_ne]

Goal state after:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_12
b : ℝ
hb : 0 < b
⊢ (fun x ↦ b ^ x) = rexp ∘ ⇑((LinearMap.mul ℝ ℝ) (log b))

Tactic:
ext x

Goal state after:
case e'_12
b : ℝ
hb : 0 < b
x : ℝ
⊢ b ^ x = (rexp ∘ ⇑((LinearMap.mul ℝ ℝ) (log b))) x
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : ι → α
⊢ Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j

Tactic:
by
  simp only [smul_eq_mul, monovary_iff_smul_rearrangement]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : 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, z i ^ (w i / ∑ i ∈ s, w i)

Tactic:
← finsetProd_rpow _ _ (fun i hi => rpow_nonneg (hz _ hi) _) _

Goal state after:
case e'_3
ι : 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, z i ^ (w i / ∑ i ∈ s, w i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

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

Tactic:
rw [eLpNorm', ← ENNReal.rpow_one (eLpNormEssSup f μ)]

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ eLpNormEssSup f μ ^ 1 * μ Set.univ ^ (1 / q)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

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

Tactic:
ext x

Goal state after:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst✝ : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
x : α
⊢ (∑ i ∈ s, f i) x = ∑ i ∈ s, f i x
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x ↦ ‖f_lim x‖ₑ) μ = essSup (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) μ

Tactic:
refine essSup_congr_ae (h_lim.mono fun x hx => ?_)

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ (fun x ↦ ‖f_lim x‖ₑ) x = (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) x
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ edist (MemLp.toLp f hf) (MemLp.toLp g hg) = eLpNorm (f - g) p μ

Tactic:
edist_def

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf) - ↑↑(MemLp.toLp g hg)) p μ = eLpNorm (f - g) p μ
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case inr
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ c * (eLpNorm (↑↑g) p μ).toReal

Tactic:
have := eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg h hc p

Goal state after:
case inr
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
this : eLpNorm (↑↑f) p μ = 0 ∧ eLpNorm (↑↑g) p μ = 0
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ c * (eLpNorm (↑↑g) p μ).toReal
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
inst✝⁶ : NormedRing 𝕜
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜' E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜' E
inst✝ : Fact (1 ≤ p)
r : 𝕜
f : ↥(Lp E p μ)
⊢ ‖r • f‖ₑ ≤ ‖r‖ₑ * ‖f‖ₑ

Tactic:
simpa only [eLpNorm_congr_ae (coeFn_smul _ _), enorm_def]
      using eLpNorm_const_smul_le (c := r) (f := f) (p := p)

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

Goal state before:
pp: case e'_6
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ (fun x ↦ ‖f x‖ₑ) = fun x ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal

Tactic:
ext x

Goal state after:
case e'_6
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ₑ = ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_6
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ (fun x ↦ ‖f x‖) = fun x ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
ext x

Goal state after:
case e'_6
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ {
      toFun := fun x ↦
        match x with
        | Sum.inl a => (inl.trans f) a
        | Sum.inr b => (inr.trans f) b,
      inj' := ⋯ } =
    f

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
x : α ⊕ β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      x =
    f x
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
⊢ (fun x ↦ { toFun := fun x_1 ↦ x, inj' := ⋯ }) ((fun f ↦ f default) x✝) = x✝

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ ((fun x ↦ { toFun := fun x_1 ↦ x, inj' := ⋯ }) ((fun f ↦ f default) x✝)) x = x✝ x
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (1 - -(↑x⁻¹ * t))⁻¹ʳ * ↑x⁻¹ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
sub_neg_eq_add

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Ring.Units

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

Tactic:
sub_neg_eq_add

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

Goal state before:
pp: case h
𝕜 : 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
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
⊢ ↑(((unitsEquiv 𝕜 E) w).trans e) = f'

Tactic:
ext x

Goal state after:
case h
𝕜 : 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'
x : E
⊢ ↑(((unitsEquiv 𝕜 E) w).trans e) x = f' x
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
N : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse ⇑f₂ ⇑f₁
p : N →L[R] N := f₁ ∘SL f₂
⊢ IsIdempotentElem p

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
N : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse ⇑f₂ ⇑f₁
p : N →L[R] N := f₁ ∘SL f₂
x : N
⊢ (p * p) x = p x
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
N : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse ⇑f₂ ⇑f₁
p : N →L[R] N := f₁ ∘SL f₂
⊢ IsIdempotentElem p

Tactic:
by ext x; simp [p, h (f₂ x)]

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

Goal state before:
pp: case inr
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u < ∞
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

Tactic:
· exact le_trans (measureReal_mono (symmDiff_triangle s t u)
        (measure_union_ne_top (by finiteness) (by finiteness)))
      (measureReal_union_le (s ∆ t) (t ∆ u))

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

Goal state before:
pp: E : Type u_2
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
⊢ MemLp f p μ

Tactic:
by
  have : MemLp f ∞ μ :=
    ⟨h2f, eLpNormEssSup_le_of_ae_enorm_bound hfC |>.trans_lt hC.lt_top⟩
  exact this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) hf.measure_ne_top le_top

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
try assumption

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

Tactic:
try assumption

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

Goal state before:
pp: case hμ
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0

Tactic:
try assumption

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
try assumption

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ 0

Tactic:
try assumption

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

Goal state before:
pp: case h_top
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ ∞

Tactic:
try assumption

Goal state after: