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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
x✝² : x ∈ s
y : E
x✝¹ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ a * ‖x‖ + ‖b‖ * ‖y‖ = a * ‖x‖ + b * ‖y‖

Tactic:
Real.norm_of_nonneg hb

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
x✝² : x ∈ s
y : E
x✝¹ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ a * ‖x‖ + b * ‖y‖ = a * ‖x‖ + b * ‖y‖
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
⊢ edist x y ≤ ediam s

Tactic:
rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ ediam s
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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
i : ι
hi : i ∈ u
⊢ i ∈ cons j (cons k u hk✝) ⋯

Tactic:
by simp [hi]

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

Goal state before:
pp: case hsmul_right
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
⊢ ∀ (m₀ : H) {i : Set E}, i ∈ 𝓝 0 → ∀ᶠ (x : 𝕜) in 𝓝 0, x • m₀ ∈ {u | ∀ (x : α), φ u x ∈ i}

Tactic:
· intro u U hU
    simp only [Set.mem_ofPred_eq, map_smul, Pi.smul_apply]
    simpa only [Set.mapsTo_range_iff] using (h u hU).eventually_nhds_zero (mem_of_mem_nhds hU)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩
  refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩
  refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_
  rw [hU, Real.mul_self_sqrt (le_of_lt hr)]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = p.moduleFilterBasis.filter
⊢ 𝓝 0 = p.moduleFilterBasis.filter

Tactic:
exact h

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = p.moduleFilterBasis.filter
⊢ WithSeminorms p

Tactic:
by
  refine
    ⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩
  rw [AddGroupFilterBasis.nhds_zero_eq]
  exact h

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_1 ∈ ball x r, x_1 ∈ Set.range ⇑f
x✝ : F
a✝ : x✝ ∈ ball 0 r
⊢ x✝ + x ∈ (↑f).range

Tactic:
apply h

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_1 ∈ ball x r, x_1 ∈ Set.range ⇑f
x✝ : F
a✝ : x✝ ∈ ball 0 r
⊢ x✝ + x ∈ ball x r
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
ι : Type u_6
p : Filter ι
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
a : ι → E →SLᵤ[σ, 𝔖] F
a₀ : E →SLᵤ[σ, 𝔖] F
⊢ Tendsto ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ a) p (𝓝 ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) a₀)) ↔
    ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 ↦ (a x1) x2) (⇑a₀) p s

Tactic:
UniformOnFun.tendsto_iff_tendstoUniformlyOn

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
ι : Type u_6
p : Filter ι
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
a : ι → E →SLᵤ[σ, 𝔖] F
a₀ : E →SLᵤ[σ, 𝔖] F
⊢ (∀ s ∈ 𝔖,
      TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ a)
        ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) a₀)) p s) ↔
    ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 ↦ (a x1) x2) (⇑a₀) p s
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
F : Type u_7
ι : Type u_9
inst✝⁷ : NormedField 𝕝
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
E : Type u_11
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕝 E
inst✝ : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ⇑f

Tactic:
rw [← Seminorm.const_isBounded (Fin 1)] at hf
  exact continuous_of_isBounded (norm_withSeminorms 𝕝 E) hq f hf

Goal state after:
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 ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] ⇑q
V : Set E
hV : V ∈ p.basisSets
hε : id V ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] ⇑q
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l✝ : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (a b : α → β), a ≈ b → (∃ b, a =ᶠ[l] fun x ↦ b) = ∃ b_1, b =ᶠ[l] fun x ↦ b_1

Tactic:
by
    suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from
      fun f g h ↦ propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩
    exact fun f g b hfg hf ↦ (hfg.symm).trans hf

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (id i) a) (⇑f) l K) ↔
    Tendsto (toUniformOnFunIsCompact ∘ id) l (𝓝 f.toUniformOnFunIsCompact)

Tactic:
UniformOnFun.tendsto_iff_tendstoUniformlyOn

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (id i) a) (⇑f) l K) ↔
    ∀ s ∈ {K | IsCompact K},
      TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | IsCompact K}) ∘ toUniformOnFunIsCompact ∘ id)
        ((UniformOnFun.toFun {K | IsCompact K}) f.toUniformOnFunIsCompact) l s
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun x ↦ a * x) ⋯ ⋯
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
exact g_iso.limsup_apply.symm

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
⊢ (uniformOn s) t + (uniformOn s) tᶜ = 1

Tactic:
by
  rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
    (isProbabilityMeasure_uniformOn hs hs').measure_univ]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

pp: case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

pp: case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u

Tactic:
· simp [uniformOn_self ht ht']

Goal state after:
case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
⊢ (m i) (s i) = 0

Tactic:
by simp [hi]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.indicator f) μ = essSup f (μ.restrict s)

Tactic:
simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]
  exact limsup_const_bot.trans_le zero_le

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ (dirac x) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
Fintype.prod_empty,

Goal state after:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ (dirac x) (univ.pi s) = 1
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✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x)) * (μ i) (update (fun j ↦ univ) i s i) =
    (∏ j ∈ Finset.univ.erase i, (μ j) univ) * (μ i) s

Tactic:
congrm ?_ * ?_

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x) = ∏ j ∈ Finset.univ.erase i, (μ j) univ

case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (μ i) (update (fun j ↦ univ) i s i) = (μ i) s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case neg.e_a.e_f
α : 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 = ∞
⊢ (fun x ↦ s.indicator (fun a ↦ ‖f a‖ₑ) x ^ p.toReal) = fun a ↦ s.indicator (fun x ↦ ‖f x‖ₑ ^ p.toReal) a

Tactic:
rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero,
    Function.comp_def]

Goal state after:
case neg.e_a.e_f
α : 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 = ∞
⊢ 0 ^ p.toReal = 0
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 : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ (Measure.pi μ) (univ.pi fun j ↦ eval j '' K) < ∞

Tactic:
rw [Measure.pi_pi]

Goal state after:
ι : 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 : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ∏ i, (μ i) (eval i '' K) < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0

Tactic:
constructor
  · intro h
    exact
      ⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
        (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩
  · rintro ⟨rfl, rfl⟩
    rw [mul_zero]

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ eLpNorm' f q μ ≤ eLpNorm' g q μ

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm]

Goal state after:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 + p * -1 < (1 + -1) ^ p

Tactic:
rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]

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

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

Tactic:
rpow_def_of_pos hs1,

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

Goal state before:
pp: s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
by
  have hp' : 0 < p := zero_lt_one.trans hp
  rcases eq_or_lt_of_le hs with rfl | hs
  · rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
  have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
  rcases le_or_gt (1 + p * s) 0 with hs2 | hs2
  · exact hs2.trans_lt (rpow_pos_of_pos hs1 _)
  have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp
  have hs4 : 1 + p * s ≠ 1 := by
    contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
  rw [rpow_def_of_pos hs1, ← exp_log hs2]
  apply exp_strictMono
  rcases lt_or_gt_of_ne hs' with hs' | hs'
  · rw [← div_lt_iff₀ hp', ← div_lt_div_right_of_neg hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · gcongr
      exact mul_lt_of_one_lt_left hs' hp
  · rw [← div_lt_iff₀ hp', ← div_lt_div_iff_of_pos_right hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · gcongr
      exact lt_mul_of_one_lt_left hs' hp

Goal state after:
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✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ∞
⊢ essSup (fun x ↦ ‖f x‖ₑ) (μ.restrict s) = essSup (fun x ↦ ‖f x‖ₑ) μ

Tactic:
exact ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx

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

Goal state before:
pp: case 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
⊢ (1 + s) ^ p < 1 + p * s

Tactic:
rpow_def_of_pos hs1,

Goal state after:
case 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
⊢ rexp (log (1 + s) * p) < 1 + p * s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ
hp : 0 ≤ p
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ

Tactic:
by
  simp [eLpNorm', ENNReal.mul_rpow_of_nonneg, hp]

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
hr : 0 < r ∧ r < ∞
⊢ p.HolderTriple q r

Tactic:
simpa [hp.2.ne, hq.2.ne, hr.2.ne] using h.ennrealOfReal

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • log x + b • log y < log (a • x + b • y)

Tactic:
have hx' : 0 < -x := by linarith

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ a • log x + b • log y < log (a • x + b • y)
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
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → ∀ k ∈ s, w k ≠ 0 → z j = z k

Tactic:
have :
      ∏ i ∈ s with w i ≠ 0, z i ^ w i = ∑ i ∈ s with w i ≠ 0, w i * z i ↔
        ∀ j ∈ {x ∈ s | w x ≠ 0}, ∀ k ∈ {x ∈ s | w x ≠ 0}, z j = z k :=
    geom_mean_eq_arith_mean_weighted_iff_of_pos _ w z (by grind)
      (sum_filter_ne_zero _ |>.trans hw') (hz _ <| mem_of_mem_filter · ·)
  grind [prod_filter_of_ne, sum_filter_of_ne, rpow_zero]

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

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
@ENNReal.mul_rpow_of_nonneg _ _ (1 / p) (by simp [hp0]),

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2)) ^ (1 / p) * ((∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (p⁻¹ + q⁻¹)

pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0

Tactic:
hpq.inv_add_inv_eq_one,

Goal state after:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ 1

case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0