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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
⊢ Continuous fun p ↦ p.1 * p.2

Tactic:
by
    refine continuous_of_continuous_uncurry _ ?_
    have h1 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.fst x.snd :=
      continuous_eval.comp (continuous_fst.prodMap continuous_id)
    have h2 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.snd x.snd :=
      continuous_eval.comp (continuous_snd.prodMap continuous_id)
    exact h1.mul h2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
L : SummationFilter γ
hf : HasProd f g L
x : α
⊢ HasProd (fun i ↦ (f i) x) (g x) L

Tactic:
let ev : C(α, β) →* β := (Pi.evalMonoidHom _ x).comp coeFnMonoidHom

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
L : SummationFilter γ
hf : HasProd f g L
x : α
ev : C(α, β) →* β := (Pi.evalMonoidHom (fun a ↦ β) x).comp coeFnMonoidHom
⊢ HasProd (fun i ↦ (f i) x) (g x) L
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
cases nonempty_encodable (ι → ℕ)

Goal state after:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
⊢ IsCountablySpanning (univ.pi '' univ.pi C)
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᵐ[μ] AEMeasurable.mk g hg ∘ f
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
have hg_mk_f : IsBoundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsBoundedUnder, ← map_congr h_eq]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᵐ[μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
⊢ ↑(const α b) x = b

Tactic:
by
  simp only [cast]
  split_ifs with h
  case neg => exact h.elim ⟨b, rfl⟩
  have := Classical.choose_spec h
  set b' := Classical.choose h
  simp_rw [const, mk_eq_mk, EventuallyEq, ← const_def, eventually_const] at this
  rw [Function.const, this]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) (univ.pi s) ≤ ∏ i, (μ i) (s i)

Tactic:
rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
    apply OuterMeasure.pi_pi_le

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

Goal state before:
pp: case neg.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f ∞ (μ.restrict s)
hg : MemLp g ∞ (μ.restrict sᶜ)
hp_zero : ¬∞ = 0
⊢ eLpNorm (s.piecewise f g) ∞ μ < ∞

pp: case neg.inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ eLpNorm (s.piecewise f g) p μ < ∞

Tactic:
· rw [eLpNorm_top_piecewise f g hs]
    exact max_lt hf.2 hg.2

Goal state after:
case neg.inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ eLpNorm (s.piecewise f g) p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : 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 = ∞
hg' : eLpNorm' g p μ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 := by
        simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
        rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
        exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx

Goal state after:
case pos
α : 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 = ∞
hg' : eLpNorm' g p μ = 0
this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
f : α → ε
⊢ eLpNormEssSup f 0 = 0

Tactic:
by
  simp [eLpNormEssSup]

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

Goal state before:
pp: case refine_1
𝕜 : 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 : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1

Tactic:
· field

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

Goal state before:
pp: case refine_1
𝕜 : 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 : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1

Tactic:
· field

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm f p μ < ∞

Tactic:
← eLpNorm_enorm

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm (fun x ↦ ‖f x‖ₑ) p μ < ∞
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y ≠ 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ z / y - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ z / y ≠ 1
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ openSegment 𝕜 y v

Tactic:
rw [openSegment_eq_Ioo (hu2.trans huv)]
      exact ⟨hu2, huv⟩

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
⊢ y ∈ Iio 0 → x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)

Tactic:
(hy : y < 0)

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: E : Type u_4
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
⊢ MemLp f ∞ μ

Tactic:
borelize E
  rcases hf.bounded_above_of_compact_support h'f with ⟨C, hC⟩
  apply memLp_top_of_bound ?_ C (Filter.Eventually.of_forall hC)
  exact (hf.stronglyMeasurable_of_hasCompactSupport h'f).aestronglyMeasurable

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 : ι → β
⊢ Monovary f (⇑OrderDual.toDual ∘ g) ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Tactic:
rw [monovary_iff_forall_smul_nonneg]

Goal state after:
ι : 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 : ι → β
⊢ (∀ (i j : ι), 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔
    ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
by
  rw [one_div, ← @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1])]
  rw [inv_inv]
  exact add_rpow_le_rpow_add _ _ hp1

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / p.toReal - 1) < ∞

Tactic:
apply ENNReal.rpow_lt_top_of_nonneg _ ENNReal.ofNat_ne_top

Goal state after:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ 1 / p.toReal - 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
← arith_mean_weighted_of_constant s w (fun _ => z j) (z j) hw' fun _ _ => congrFun rfl

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ ∑ i ∈ s, w i * z j = ∑ i ∈ s, w i * z i
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ 2 ^ (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞ ∧ 2 ^ (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞

Tactic:
constructor <;> finiteness

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
⊢ eLpNorm f ∞ μ < ∞

Tactic:
hq_top

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f ∞ μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
⊢ eLpNorm f ∞ μ < ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
calc
    _ = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i) := ?_
    _ ≤ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) *
          (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) :=
        inner_le_Lp_mul_Lq _ _ _ (.symm <| Real.holderConjugate_iff.mpr ⟨hp, by simp⟩)
    _ = _ := ?_

Goal state after:
case inr.calc_1
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)

case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
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 : ↥(Lp E p μ)
⊢ dist f g = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

Tactic:
dist_eq_eLpNorm_neg_add,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (eLpNorm (-↑↑f + ↑↑g) p μ).toReal = (eLpNorm (↑↑f - ↑↑g) p μ).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
    rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg (norm_nonneg _), ← Real.rpow_mul (abs_nonneg _),
      ENNReal.toReal_inv, mul_inv_cancel₀, abs_of_nonneg (norm_nonneg _), Real.rpow_one]
    simp [ENNReal.toReal_eq_zero_iff, q_zero, q_top]

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ MemLp f p μ

Tactic:
have A : ∀ x, ‖f x‖ ≤ K' * ‖g (f x)‖ := by
    intro x
    -- TODO: add `AntilipschitzWith.le_mul_nnnorm_sub` and `AntilipschitzWith.le_mul_norm`
    rw [← dist_zero_right, ← dist_zero_right, ← g0]
    apply hg'.le_mul_dist
  have B : AEStronglyMeasurable f μ :=
    (hg'.isUniformEmbedding hg).isEmbedding.aestronglyMeasurable_comp_iff.1 hL.1
  exact hL.of_le_mul B (Filter.Eventually.of_forall A)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a.inl
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
i : ι
hi : i ∈ s
hw : w i = 0
⊢ w i * f i = ↑(w i).toNNReal * ↑(f i).toNNReal

Tactic:
simp [hw]

Goal state after:
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✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((B (g + h)).compLp f) x = (B (g + h)) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
⊢ ↑↑((B h).compLp f) x = (B h) (↑↑f x) →
    ↑↑((B g).compLp f + (B h).compLp f) x = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x →
      ↑↑((compLpₗ p μ (B (g + h))) f) x = ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f) x

Tactic:
hh

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((B (g + h)).compLp f) x = (B (g + h)) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hh : ↑↑((B h).compLp f) x = (B h) (↑↑f x)
⊢ ↑↑((B g).compLp f + (B h).compLp f) x = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x →
    ↑↑((compLpₗ p μ (B (g + h))) f) x = ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f) x
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✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((B (g + h)).compLp f) x = (B (g + h)) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hh : ↑↑((B h).compLp f) x = (B h) (↑↑f x)
⊢ ↑↑((B g).compLp f + (B h).compLp f) x = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x →
    ↑↑((compLpₗ p μ (B (g + h))) f) x = ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f) x

Tactic:
hadd

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((B (g + h)).compLp f) x = (B (g + h)) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hh : ↑↑((B h).compLp f) x = (B h) (↑↑f x)
hadd : ↑↑((B g).compLp f + (B h).compLp f) x = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x
⊢ ↑↑((compLpₗ p μ (B (g + h))) f) x = ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f) 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)⁻¹ʳ
| (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
ht',

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)⁻¹ʳ
| (∑ i ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * (1 + ↑x⁻¹ * t)⁻¹ʳ) * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖

Tactic:
by_cases hx : f x = 0

Goal state after:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖

case neg
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖