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
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, p j ≠ ∑ i ∈ t, w i • p i

Tactic:
by
  apply hf.convexOn.map_sum_le (h₀ · · |>.le) h₁ hmem |>.lt_iff_ne.trans
  contrapose!
  exact hf.map_sum_eq_iff h₀ h₁ hmem

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
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
U : Set E
⊢ IsOpen[inst✝] U ↔ ∀ x ∈ U, U ∈ 𝓝 x

Tactic:
isOpen_iff_mem_nhds

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✝ ∈ (↑f).range

Tactic:
rw [← Submodule.add_mem_iff_left (f : E →ₛₗ[σ₁₂] F).range (h _ <| mem_ball_self hr)]

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 ∈ (↑f).range
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded p (fun i ↦ (Finset.Iic i).sup p) LinearMap.id

pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun i ↦ (Finset.Iic i).sup p) p LinearMap.id

Tactic:
· intro i
    refine ⟨Finset.Iic i, 1, ?_⟩
    rw [one_smul]
    rfl

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun i ↦ (Finset.Iic i).sup p) p LinearMap.id
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
⊢ ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖

Tactic:
have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0

Goal state after:
𝕜 : 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)
⊢ ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
inst✝ : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ PolynormableSpace 𝕜 E

Tactic:
let _ : TopologicalSpace E := induced f inferInstance
  exact f.withSeminorms_induced (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace

Goal state after:
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 β
⊢ ∀ (f g : α → β) (b : β), f =ᶠ[l] g → (f =ᶠ[l] fun x ↦ b) → g =ᶠ[l] fun x ↦ b

Tactic:
exact fun f g b hfg hf ↦ (hfg.symm).trans hf

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ IsOpen[⨆ K,
          ⨆ (_ : IsCompact K),
            TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ }]
      (⇑(CompactCoherentification.mk X) ⁻¹' A) ↔
    ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)

Tactic:
isOpen_iSup_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ (∀ (i : Set X),
      IsCompact i →
        IsOpen[TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ }]
          (⇑(CompactCoherentification.mk X) ⁻¹' A)) ↔
    ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace] (A.domRestrict (⇑(CompactCoherentification.mk Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst✝] (A.domRestrict f)

Tactic:
let := isCompact_iff_compactSpace.1 hA

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
this : CompactSpace ↑A := isCompact_iff_compactSpace.mp hA
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace] (A.domRestrict (⇑(CompactCoherentification.mk Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst✝] (A.domRestrict f)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ CompactlyCoherentSpace (𝐤X)

Tactic:
by
  refine .of_isOpen_forall_compactSpace fun U hU ↦ isOpen_iff.mpr fun K hK ↦ ?_
  rw [← preimage_comp]
  have : CompactSpace K := isCompact_iff_compactSpace.mp hK
  exact hU K _ (continuous_rng_of_compactSpace.mpr continuous_subtype_val)

Goal state after:
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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
⊢ Continuous[instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖, Pi.topologicalSpace] fun f i ↦
    ContinuousLinearMap.proj i ∘SL f

Tactic:
by
      apply continuous_pi (A := fun i ↦ E →Lᵤ[𝕜, 𝔖] F i) fun i ↦ ?_
      exact (ContinuousLinearMap.proj i : (Π j, F j) →L[𝕜] F i).postcompUniformConvergenceCLM 𝔖
        |>.continuous

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
⊢ μ[|univ] = μ

Tactic:
by
  simp [cond, measure_univ, Measure.restrict_univ]

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ∃ᶠ (x : α) in f, ¬u x = 0 x
⊢ ∃ᶠ (x : α) in f, ∞ ≤ if u x = 0 then 0 else ∞

Tactic:
exact hu.mono fun x hx => by simpa

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ (uniformOn {ω}) t = if ω ∈ t then 1 else 0

Tactic:
by
  rw [uniformOn, cond_apply (measurableSet_singleton ω), Measure.count_singleton, inv_one,
    one_mul]
  split_ifs
  · rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]
  · simpa

Goal state after:
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
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
by
  have hg_mk_co : IsCoboundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsCoboundedUnder, ← map_congr hg.ae_eq_mk]
  have hg_mk_bdd : IsBoundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsBoundedUnder, ← map_congr hg.ae_eq_mk]
  have h_eq := ae_eq_comp hf hg.ae_eq_mk
  have hg_mk_f : IsBoundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsBoundedUnder, ← map_congr h_eq]
  have hg_mk_f_co : IsCoboundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsCoboundedUnder, ← map_congr h_eq]
  rw [essSup_congr_ae hg.ae_eq_mk,
    essSup_map_measure_of_measurable hg.measurable_mk hf hg_mk_co hg_mk_f hg_mk_f_co hg_mk_bdd]
  exact essSup_congr_ae h_eq.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ f ≤ f ⊔ g

Tactic:
rw [← coeFn_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ ↑f ≤ᵐ[μ] ↑(f ⊔ g)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ g ≤ f ⊔ g

Tactic:
rw [← coeFn_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ ↑g ≤ᵐ[μ] ↑(f ⊔ g)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ f ⊓ g ≤ f

Tactic:
rw [← coeFn_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᵐ[μ] ↑f
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ f ⊓ g ≤ g

Tactic:
rw [← coeFn_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᵐ[μ] ↑g
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✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (map (TProd.elim' ⋯) (Measure.tprod (sortedUniv ι) μ)) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
    MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
    List.prod_toFinset, sortedUniv_toFinset] <;>
  exact sortedUniv_nodup ι

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)
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

Tactic:
refine Finset.prod_congr rfl fun j hj ↦ ?_

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
j : ι
hj : j ∈ Finset.univ.erase i
⊢ (μ j) (update (fun j ↦ univ) i s j) = (μ j) univ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ∞

Tactic:
lintegral_rpow_enorm_eq_rpow_eLpNorm' hq0_lt

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
⊢ eLpNorm' f q μ ^ q < ∞
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a * x + b * z

Tactic:
linear_combination b * hxz - x * hab

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a * x + b * z

Tactic:
linear_combination b * hxz - x * hab

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

Goal state before:
pp: case inr.inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ∞ ≠ 0
⊢ eLpNorm f ∞ μ < ∞

Tactic:
simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder]
    exact .le_of_finite

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

Goal state before:
pp: case inr.refine_1
𝕜 : 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
⊢ y ∈ s

Tactic:
apply hf.1.segment_subset hx hu.1

Goal state after:
case inr.refine_1
𝕜 : 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
⊢ y ∈ segment 𝕜 x u
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
simp only [smul_eq_mul, antivary_iff_forall_smul_nonpos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case hnc
h : 0 ∈ Set.Ioo 0 1
⊢ False

Tactic:
exact lt_irrefl _ h.1

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
apply le_antisymm this at h

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

Goal state before:
pp: case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi : none ∈ insertNone s
⊢ AEMeasurable (fun t ↦ none.elim (g t) fun j ↦ f j t) μ

pp: case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi : some i ∈ insertNone s
⊢ AEMeasurable (fun t ↦ (some i).elim (g t) fun j ↦ f j t) μ

Tactic:
· exact hg

Goal state after:
case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi : some i ∈ insertNone s
⊢ AEMeasurable (fun t ↦ (some i).elim (g t) fun j ↦ f j t) μ
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : (f + g) a = 0
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)

Tactic:
rw [h_zero, ENNReal.zero_rpow_of_pos hpq.pos]

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : (f + g) a = 0
⊢ 0 ≤ 0 * 0 ^ (p - 1)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

Tactic:
exact lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow hpq hf (hf.add hg)

Goal state after:
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
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n ↦ f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun m ↦ ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))

Tactic:
refine (ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_

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
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n ↦ f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun m ↦ ‖f m a‖ₑ) atTop (𝓝 ↑‖f_lim a‖₊)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto f fi (𝓝 f_lim) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
rw [tendsto_iff_dist_tendsto_zero]
  simp_rw [dist_def]
  rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
  rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
  exact Lp.eLpNorm_ne_top _

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i * g i = |f i * g i|

pp: case e'_4.e'_5.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
x✝ : ι
a✝ : x✝ ∈ s
⊢ f x✝ = |f x✝|

pp: case e'_4.e'_6.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
x✝ : ι
a✝ : x✝ ∈ s
⊢ g x✝ = |g x✝|

Tactic:
· rw [abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))]

Goal state after:
case e'_4.e'_5.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
x✝ : ι
a✝ : x✝ ∈ s
⊢ f x✝ = |f x✝|

case e'_4.e'_6.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
x✝ : ι
a✝ : x✝ ∈ s
⊢ g x✝ = |g x✝|
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1] <;> apply sum_congr rfl

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, (f x + g x) ^ p = |f x + g x| ^ p

case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p

case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, g x ^ p = |g x| ^ p