mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h : ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
i : ι
hi : i ∈ t
this : f (∑ k ∈ t, w k • p i) = ∑ k ∈ t, w k • f (p i)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)

Tactic:
convert this using 3 <;> grind

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

Goal state before:

Tactic:
_ = ∑ g : ∀ i, κ i, (∏ i, w i (g i)) • f i (g i) := by
      simp only [Finset.sum_apply, Pi.smul_apply]
    _ = ∑ j : κ i, ∑ g : {g : ∀ k, κ k // g i = j},
          (∏ k, w k (g.1 k)) • f i ((g : ∀ i, κ i) i) := by
      rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]
    _ = ∑ j : κ i, (∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)) • f i j := by
      simp_rw [sum_smul]
      congr! with j _ g _
      exact g.2
    _ = ∑ j : κ i, w i j • f i j := ?_
    _ = x i := hf _

Goal state after:
case refine_2
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
⊢ ∑ j, (∑ g, ∏ k, w k (↑g k)) • f i j = ∑ j, w i j • f i j
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case neg
𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x✝ : F
hx : ¬‖x✝‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ 1 ≤ ‖c‖ / ε * (normSeminorm 𝕜 F) x

Tactic:
← div_le_iff₀' this,

Goal state after:
case neg
𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x✝ : F
hx : ¬‖x✝‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ 1 / (‖c‖ / ε) ≤ (normSeminorm 𝕜 F) x
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
let _ : NormedSpace 𝕜 E := { norm_smul_le := fun a b ↦ le_of_eq (map_smul_eq_mul (s.sup p) a b) }

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), ‖f x‖ = ‖g x‖
c : ℝ
hc : c ≥ 0
h₂ : ∀ (x : E), ‖f x‖ ≤ c * ‖x‖
z : E
⊢ ‖g z‖ ≤ c * ‖z‖

Tactic:
by
      rw [← h z]
      exact h₂ z

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

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = (algebraMap R C(α, R)) (f default)
⊢ (algebraMap R C(α, R)) (f default) ∈ s₁ ↔ (algebraMap R C(α, R)) (f default) ∈ s₂

Tactic:
simp only [Subalgebra.algebraMap_mem]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
⊢ (uniformOn s) t = 1

Tactic:
have := isProbabilityMeasure_uniformOn hs hs'

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ (uniformOn s) t = 1
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜ᵐᵒᵖ γ
inst✝ : IsCentralScalar 𝕜 γ
a : 𝕜
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ MulOpposite.op a • mk f hf = a • mk f hf

Tactic:
by simp_rw [smul_mk, op_smul_eq_smul]

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ioo (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Tactic:
rw [← pi_univ_Icc]

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ioo (f i) (g i)) =ᵐ[Measure.pi μ] univ.pi fun i ↦ Icc (f i) (g i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ioc (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Tactic:
rw [← pi_univ_Icc]

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ioc (f i) (g i)) =ᵐ[Measure.pi μ] univ.pi fun i ↦ Icc (f i) (g i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ico (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Tactic:
rw [← pi_univ_Icc]

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ico (f i) (g i)) =ᵐ[Measure.pi μ] univ.pi fun i ↦ Icc (f i) (g i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulRightInvariant
⊢ (Measure.pi μ).IsMulRightInvariant

Tactic:
by
  refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
  rw [map_apply (measurable_mul_const _) (MeasurableSet.univ_pi hs),
    show (· * v) ⁻¹' univ.pi s = univ.pi fun i => (· * v i) ⁻¹' s i by rfl, pi_pi]
  simp_rw [measure_preimage_mul_right]

Goal state after:
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
⊢ MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) (Measure.pi μ)
    ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i))

Tactic:
set e := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm

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
⊢ MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) (Measure.pi μ)
    ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i))
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
⊢ eLpNorm 0 p μ = 0

Tactic:
by_cases h_top : p = ∞

Goal state after:
case pos
α : 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

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: case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
h0 : ¬p = 0
⊢ eLpNorm f p 0 = 0

Tactic:
by_cases h_top : p = ∞

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

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: case neg
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by_cases h_top : p = ∞

Goal state after:
case pos
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

case neg
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : 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
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h_top : p = ∞

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 p μ ≤ c • eLpNorm g p μ

case neg
α : 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 p μ ≤ c • eLpNorm g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm (fun x ↦ c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
by_cases h_top : p = ∞

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
h_top : p = ∞
⊢ eLpNorm (fun x ↦ c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm (fun x ↦ c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : 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
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h_top : p = ∞

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 p μ ≤ c • eLpNorm g p μ

case neg
α : 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 p μ ≤ c • eLpNorm g p μ
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
⊢ ∏ i, (μ i) (Fin.cons s (Fin.cons t finZeroElim) i) = (μ 0) s * (μ 1) t

Tactic:
Fin.prod_univ_two

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.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
← lt_div_iff₀ hp1,

Goal state after:
case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) < log (1 + p * s) / p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
← lt_div_iff₀ hp1,

Goal state after:
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) < log (1 + p * s) / p
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
convert! hf.slope_strict_mono_adjacent hx hy hxa hya using 1

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
⊢ (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun x ↦ ‖f x‖₊) → eLpNormEssSup f μ < ∞

Tactic:
by rintro ⟨C, hC⟩; exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
⊢ eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
simp [EventuallyEq, eLpNormEssSup_eq_essSup_enorm]

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✝ : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
by_cases h_top : p = ∞

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p ≠ ∞ →
    ∑ i ∈ s, w i * z i ^ p ≠ ∞ → ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Tactic:
· -- second, suppose both `(∑ i ∈ s, w i * z i) ^ p ≠ ⊤` and `∑ i ∈ s, (w i * z i ^ p) ≠ ⊤`,
    -- and prove `((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, (w i * z i ^ p)).toNNReal`,
    -- by using `NNReal.rpow_arith_mean_le_arith_mean_rpow`.
    intro h_top_rpow_sum _
    -- show hypotheses needed to put the `.toNNReal` inside the sums.
    have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
      haveI h_top_sum : ∑ i ∈ s, w i * z i ≠ ⊤ := by
        intro h
        rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
        exact h_top_rpow_sum rfl
      fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne
    have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ := by
      intro i hi
      specialize h_top i hi
      rwa [Ne, ← h_top_iff_rpow_top i hi]
    -- put the `.toNNReal` inside the sums.
    simp_rw [toNNReal_sum h_top_rpow, toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul,
      toNNReal_rpow]
    -- use corresponding nnreal result
    refine
      NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal)
        (fun i => (z i).toNNReal) ?_ hp
    -- verify the hypothesis `∑ i ∈ s, (w i).toNNReal = 1`, using `∑ i ∈ s, w i = 1` .
    have h_sum_nnreal : ∑ i ∈ s, w i = ↑(∑ i ∈ s, (w i).toNNReal) := by
      push_cast
      congr! with i hi
      refine (coe_toNNReal (lt_top_of_sum_ne_top ?_ hi).ne).symm
      exact hw'.symm ▸ ENNReal.one_ne_top
    rwa [← coe_inj, ← h_sum_nnreal]

Goal state after:
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 : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
this : ∏ i ∈ s, z k ^ w i = ∑ i ∈ s, w i * z k
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i

Tactic:
convert this using 3 <;> grind

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_1
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, f i ^ p) ^ (r / p) ≤ (∑' (i : ι), f i ^ p) ^ (r / p)

Tactic:
gcongr
      exact hf.sum_le_tsum _ (fun _ _ => zero_le)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ (∑ i ∈ s, w i * f i) / ↑(#s) ≤ ((∑ i ∈ s, w i) / ↑(#s)) ^ (1 - p⁻¹) * ((∑ i ∈ s, w i * f i ^ p) / ↑(#s)) ^ p⁻¹

Tactic:
rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]

Goal state after:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ (∑ i ∈ s, w i * f i) / ↑(#s) ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ / ↑(#s)

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

case h
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 1 - p⁻¹ + p⁻¹ ≠ 0

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i * f i ^ p

case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i

case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case inl
α : 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 : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
lift c to ℝ≥0 using hc

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