mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (w i) = SignType.sign (w j)

Tactic:
hr i hi,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * (w₂ i - w₁ i) + w₁ i) = SignType.sign (w j)
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
⊢ IsTopologicalAddGroup E

Tactic:
hp.withSeminorms_eq

Goal state after:
𝕜 : 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
⊢ IsTopologicalAddGroup E
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
⊢ ContinuousSMul 𝕜 E

Tactic:
hp.withSeminorms_eq

Goal state after:
𝕜 : 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
⊢ ContinuousSMul 𝕜 E
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
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
⊢ IsTopologicalAddGroup (E →SLᵤ[σ, 𝔖] F)

Tactic:
by
  let : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  infer_instance

Goal state after:
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 : ι'
⊢ Continuous[x✝¹, _] ⇑((q i).comp f)

Tactic:
rcases hf i with ⟨s, C, hC⟩

Goal state after:
𝕝 : 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 ≤ C • s.sup p
⊢ Continuous[x✝¹, _] ⇑((q i).comp f)
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
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
inst✝¹² : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹¹ : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜₃ G
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun x ↦ ⇑L '' x) 𝔖 𝔗
this : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    f ∘SL L

Tactic:
have : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁✝ : 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
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
inst✝¹² : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹¹ : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜₃ G
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun x ↦ ⇑L '' x) 𝔖 𝔗
this✝ : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this : IsUniformAddGroup G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    f ∘SL L
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
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
inst✝¹⁴ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹³ : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst✝³ : IsTopologicalAddGroup F
inst✝² : IsTopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    L ∘SL f

Tactic:
have : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜₁✝ : 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
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
inst✝¹⁴ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹³ : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst✝³ : IsTopologicalAddGroup F
inst✝² : IsTopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝ : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this : IsUniformAddGroup G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖] fun f ↦
    L ∘SL f
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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
h'M : ↑M < ∞
x : E
hM : ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (↑M * ‖x‖)
⊢ ‖f x‖ ≤ ↑M * ‖x‖

Tactic:
ENNReal.ofReal_le_ofReal_iff (by positivity)

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
h'M : ↑M < ∞
x : E
hM : ‖f x‖ ≤ ↑M * ‖x‖
⊢ ‖f x‖ ≤ ↑M * ‖x‖
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
⊢ Continuous fun a ↦ a⁻¹

Tactic:
let : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
    have : IsUniformGroup β := isUniformGroup_of_commGroup
    rw [continuous_iff_continuousAt]
    intro f
    rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn]
    exact fun K hK =>
      uniformContinuous_inv.comp_tendstoUniformlyOn
        (tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)

Goal state after:
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
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ * c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } *
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝

Tactic:
exact (algebraMap R A).map_mul _ _

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

Goal state before:
pp: case inr.inr.mpr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y) → ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y

Tactic:
rintro h (_ | x) hx
    · simpa [lt_top_iff_ne_top]
    filter_upwards [h₁, h x (by simpa [ofReal_lt_coe_iff hr] using hx)] with i hi
    simp [← lt_ofReal_iff_toReal_lt hi]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : Measure.count[t | s] = 1
hsf : s.Finite
⊢ s ⊆ t

Tactic:
cond_apply hsf.measurableSet,

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (Measure.count s)⁻¹ * Measure.count (s ∩ t) = 1
hsf : s.Finite
⊢ s ⊆ t
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ essSup f μ ≤ essSup f (μ.restrict s)

Tactic:
apply le_of_forall_lt (fun c hc ↦ ?_)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
⊢ c < essSup f (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

Tactic:
exact le_rfl

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

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

Tactic:
rcases eq_or_lt_of_le hxy with (rfl | hxy)
  · simp
  rcases lt_or_gt_of_ne hxa with hxa | hxa
  · rcases lt_or_gt_of_ne hya with hya | hya
    · convert! hf.secant_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;> simp
    · convert! hf.slope_mono_adjacent hx hy hxa hya using 1
      rw [← neg_div_neg_eq]; simp
  · exact hf.secant_mono_aux2 ha hy hxa hxy

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

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑(p - 1))⁻¹

Tactic:
rw [← coe_inv (tsub_pos_of_lt hp).ne']

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + ↑(p - 1)⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

Tactic:
add_sub_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 ^ (p - 1) * (y - x) / y ^ p < (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 < y - x
⊢ -1 ≤ x / y - 1

Tactic:
le_sub_iff_add_le,

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

Tactic:
add_sub_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 ^ (p - 1) * (z - y) / y ^ p < (1 + (z / 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 ≤ z / y - 1

Tactic:
le_sub_iff_add_le,

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 + 1 ≤ z / y
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 ≤ z / y - 1

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

Tactic:
· rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]
      exact Or.inl ⟨hz, hy.le⟩

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

Goal state before:
pp: 𝕜 : 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
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ openSegment 𝕜 x z

Tactic:
rw [openSegment_eq_Ioo (hxy.trans hz.2)]

Goal state after:
𝕜 : 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
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ Set.Ioo x z
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = eLpNorm (↑g) p ν

Tactic:
rw [eLpNorm_congr_ae (g.coeFn_compMeasurePreserving _)]

Goal state after:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑g ∘ f) p μ = eLpNorm (↑g) p ν
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‖ₑ ^ p.toReal) atTop < ∞
hppos : 0 < p.toReal
⊢ liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n ↦ ‖f n x‖ₑ) atTop ^ p.toReal

Tactic:
change
      liminf (fun n => ENNReal.orderIsoRpow p.toReal hppos (‖f n x‖ₑ)) atTop =
        ENNReal.orderIsoRpow p.toReal hppos (liminf (fun n => (‖f n x‖ₑ)) atTop)

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‖ₑ ^ p.toReal) atTop < ∞
hppos : 0 < p.toReal
⊢ liminf (fun n ↦ (ENNReal.orderIsoRpow p.toReal hppos) ‖f n x‖ₑ) atTop =
    (ENNReal.orderIsoRpow p.toReal hppos) (liminf (fun n ↦ ‖f n x‖ₑ) atTop)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1

Tactic:
simp_rw [funMulInvSnorm_rpow hp0_lt]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.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
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

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

Goal state after:
case e'_2.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
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ ∑ i ∈ s, w i * z j = ∑ i ∈ s, w i * z i
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁷ : CommRing 𝕜
inst✝¹⁶ : LinearOrder 𝕜
inst✝¹⁵ : IsStrictOrderedRing 𝕜
inst✝¹⁴ : CommRing E
inst✝¹³ : LinearOrder E
inst✝¹² : IsStrictOrderedRing E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : LinearOrder F
inst✝⁹ : IsOrderedAddMonoid F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 G
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : IsOrderedModule 𝕜 F
inst✝ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_convexOn_iff, ← smul_neg]
  exact hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

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

Tactic:
have ⟨k, hk⟩ : s.Nonempty := by grind [s.eq_empty_or_nonempty]

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

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : MemLp f p μ
hg : MemLp g p μ
⊢ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ) < ∞

Tactic:
apply ENNReal.mul_lt_top (LpAddConst_lt_top p)
      exact ENNReal.add_lt_top.2 ⟨hf.2, hg.2⟩

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

Goal state before:
pp: case inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr✝ : ∞.HolderTriple q r
hpqr : 1 / r = 1 / ∞ + 1 / q
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g q μ

pp: case inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr✝ : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ

Tactic:
· have : r = q := by simpa using hpqr
    exact this ▸ eLpNorm_le_eLpNorm_top_mul_eLpNorm r f hg b c h

Goal state after:
case inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr✝ : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ