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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] (⋂₀ S)

Tactic:
h.isOpen_iff

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, ∃ t, IsOpen[inst✝²] t ∧ f ⁻¹' t = s
⊢ ∃ t, IsOpen[inst✝²] t ∧ f ⁻¹' t = ⋂₀ S
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ ∃ t ⊆ ∅, affineSpan k t = affineSpan k ∅ ∧ AffineIndependent k Subtype.val

Tactic:
exact ⟨∅, Set.empty_subset ∅, rfl, affineIndependent_of_subsingleton k _⟩

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

Goal state before:
pp: case mpr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
x : E
⊢ (∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i, w i • z i = x) → x ∈ (convexHull R) s

Tactic:
rintro ⟨ι, _, w, z, hw₀, hw₁, hz, hx⟩
    exact mem_convexHull_of_exists_fintype w z hw₀ hw₁ hz hx

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
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ {f | MapsTo (⇑f) s U} ∈ absorbing R S

Tactic:
Filter.mem_absorbing,

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
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ Absorbs R {f | MapsTo (⇑f) s U} S
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : AddCommGroup E
inst✝⁵ : NormedField 𝕝
inst✝⁴ : Module 𝕝 E
inst✝³ : AddCommGroup F
inst✝² : NormedField 𝕝₂
inst✝¹ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝ : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x✝¹, _] ⇑((q i).comp f)

Tactic:
exact continuous_of_le
    (continuous_finsetSup fun i _ ↦ (hp.continuous_seminorm i).const_smul C) hC

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
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝³ : DistribSMul 𝕜' F
inst✝² : SMulCommClass 𝕜₂ 𝕜' F
inst✝¹ : SeminormedAddCommGroup 𝕜'
inst✝ : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c‖ * ‖f x✝‖ ≤ ‖c‖ * ‖f‖ * ‖x✝‖

Tactic:
mul_assoc,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝³ : DistribSMul 𝕜' F
inst✝² : SMulCommClass 𝕜₂ 𝕜' F
inst✝¹ : SeminormedAddCommGroup 𝕜'
inst✝ : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c‖ * ‖f x✝‖ ≤ ‖c‖ * (‖f‖ * ‖x✝‖)
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
c : R
x : E
y : F
⊢ (f (c • x)) y = σ₁₃ c • (f x) y

Tactic:
rw [f.map_smulₛₗ, smul_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ * ‖f y‖₊⁻¹ < 1
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Tactic:
mul_assoc,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (‖y‖₊ * ‖f y‖₊⁻¹) < 1
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
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 : α → β
M : Type u_5
G : Type u_6
inst✝ : AddGroupWithOne G
x✝ : ℕ
⊢ ↑(Int.negSucc x✝) = (fun x ↦ Neg.neg ∘ x) ↑(x✝ + 1)

Tactic:
simp [Function.comp_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddGroupWithOne G
x✝ : ℕ
⊢ -1 + -↑x✝ = fun x ↦ -1 + -↑x✝
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst✝ : CompactSpace ↑s
⊢ (Continuous[inst✝¹, UniformFun.topologicalSpace (↑s) β] fun x ↦
      UniformFun.ofFun ⇑{ toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    ∀ s_1 ∈ {s},
      Continuous[inst✝¹, UniformFun.topologicalSpace (↑s_1) β]
        (⇑UniformFun.ofFun ∘ s_1.domRestrict ∘ ⇑(toFun {s}) ∘ fun x ↦ (ofFun {s}) (f x))

Tactic:
simp [Function.comp_def]

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

Goal state before:
pp: case hbc
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ ‖c x‖ ≤ ‖c‖ * ‖x‖

Tactic:
apply le_opNorm

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hμs : μ s = 0
⊢ μ[|s] = 0

Tactic:
by simp [hμs]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t

Tactic:
mul_assoc,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] = (μ s)⁻¹ * (μ[s | t] * μ t)
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
k : R
a : α
⊢ ((algebraMap R C(α, A)) k) a = k • 1

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
k : R
a : α
⊢ (k • 1) a = k • 1
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ MeasurableSet (⋂ i, eval i ⁻¹' s i)

Tactic:
apply MeasurableSet.iInter

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)
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 γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂Measurable g hg f₁ f₂) =ᵐ[μ] fun a ↦ g (↑f₁ a) (↑f₂ a)

Tactic:
comp₂Measurable_eq_mk

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯) =ᵐ[μ] fun a ↦ g (↑f₁ a) (↑f₂ a)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

Tactic:
rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
    have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
    simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞),
      Finset.prod_eq_zero_iff, piPremeasure]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : MeasurableSingletonClass Ω
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : Finite Ω
f : ι → Set Ω
⊢ uniformOn (Set.univ.pi f) = Measure.pi fun i ↦ uniformOn (f i)

Tactic:
by
  refine (MeasureTheory.Measure.pi_eq fun t ht ↦ ?_).symm
  lift f to ι → Finset Ω using by simp [Set.toFinite]
  lift t to ι → Finset Ω using by simp [Set.toFinite]
  classical
  simp [← Fintype.coe_piFinset, uniformOn_apply_finset, ← Fintype.piFinset_inter,
    ENNReal.prod_div_distrib_of_ne_top]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ MeasurableSet ((fun b ↦ b i) ⁻¹' s)

Tactic:
apply boundedBy_caratheodory

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (fun i ↦ (μ i).toOuterMeasure) (t ∩ (fun b ↦ b i) ⁻¹' s) +
        piPremeasure (fun i ↦ (μ i).toOuterMeasure) (t \ (fun b ↦ b i) ⁻¹' s) ≤
      piPremeasure (fun i ↦ (μ i).toOuterMeasure) t
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
⊢ Measure.pi μ = dirac x

Tactic:
by
  have : ∀ a, SigmaFinite (μ a) := isEmptyElim
  refine pi_eq fun s _ => ?_
  rw [Fintype.prod_empty, dirac_apply_of_mem]
  exact isEmptyElim (α := α)

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

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simp [h_top, eLpNormEssSup_eq_essSup_enorm]
  simp [eLpNorm_eq_eLpNorm' h0 h_top]

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

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
have h1 : 0 < y - x := by linarith

Goal state after:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (rexp y - rexp x) / (y - x) < rexp y
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
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
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
Module: Mathlib.Analysis.Convex.Slope

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

Tactic:
rcases lt_or_gt_of_ne hya with hya | hya

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

case inr.inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl
𝕜 : 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
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
rcases lt_or_gt_of_ne hya with hya | hya

Goal state after:
case inl.inl
𝕜 : 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 : y < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

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)
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
⊢ 1 - p * y⁻¹ * (y - x) < (1 + (x / y - 1)) ^ p

Tactic:
mul_assoc,

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
⊢ 1 - p * (y⁻¹ * (y - x)) < (1 + (x / y - 1)) ^ 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 < z - y
⊢ 1 + p * y⁻¹ * (z - y) < (1 + (z / y - 1)) ^ p

Tactic:
mul_assoc,

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
⊢ 1 + p * (y⁻¹ * (z - y)) < (1 + (z / y - 1)) ^ p
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]

Goal state after:
case inr.inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ∞ ≠ 0
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun x ↦ ‖f x‖₊
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ∞
x : α
hx : liminf (fun n ↦ ‖f n x‖ₑ) atTop ^ p.toReal < ∞
hppos : 0 < p.toReal
this : liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n ↦ ‖f n x‖ₑ) atTop ^ p.toReal
⊢ liminf (fun x_1 ↦ ‖f x_1 x‖ₑ) atTop ^ 1 < ∞

Tactic:
← mul_inv_cancel₀ hppos.ne.symm,

Goal state after:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ∞
x : α
hx : liminf (fun n ↦ ‖f n x‖ₑ) atTop ^ p.toReal < ∞
hppos : 0 < p.toReal
this : liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n ↦ ‖f n x‖ₑ) atTop ^ p.toReal
⊢ liminf (fun x_1 ↦ ‖f x_1 x‖ₑ) atTop ^ (p.toReal * p.toReal⁻¹) < ∞
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by
  simp only [smul_eq_mul, monovaryOn_iff_forall_smul_nonneg]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∑ i ∈ s, w i * z i) * (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x

Tactic:
mul_assoc,

Goal state after:
case e'_4
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∑ i ∈ s, w i * z i) * (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * ((∑ i ∈ s, w i)⁻¹ * z x)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ 1

Tactic:
by
  calc
    (∫⁻ a : α, (f * g) a ∂μ) ≤
        ∫⁻ a : α, f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ :=
      lintegral_mono fun a => young_inequality (f a) (g a) hpq
    _ = 1 := by
      simp only [div_eq_mul_inv]
      rw [lintegral_add_left']
      · rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]
        simp [hpq.symm.pos]
      · exact (hf.pow_const _).mul_const _

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
simp [hpq]

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

Tactic:
simp [hpq]

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

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
⊢ (1 / p)⁻¹ + (1 / q)⁻¹ = 1

Tactic:
simp [hpq]

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
⊢ ∑ i ∈ s, w i * z i ≤ ∏ i ∈ s, z i ^ w i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
← geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz

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
⊢ ∑ i ∈ s, w i * z i ≤ ∏ i ∈ s, z i ^ w i ↔ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ (n⁻¹ * ∑ i ∈ s, w i / z i)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
Finset.mul_sum _ _ n⁻¹

Goal state after:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹