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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : 1 < t
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ interior s

Tactic:
apply hs.openSegment_interior_closure_subset_interior hx ht

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : 1 < t
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y) t)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_2
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
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k s

Tactic:
· rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂
    apply AffineSubspace.ext_of_direction_eq
    · have : Submodule.span k b = Submodule.span k (insert 0 b) := by simp
      simp only [direction_affineSpan, ← hb₂, Equiv.coe_vaddConst, Set.singleton_union,
        vectorSpan_eq_span_vsub_set_right k (Set.mem_insert p _), this]
      congr
      change (Equiv.vaddConst p).symm '' insert p (Equiv.vaddConst p '' b) = _
      rw [Set.image_insert_eq, ← Set.image_comp]
      simp
    · use p
      simp only [Equiv.coe_vaddConst, Set.singleton_union, Set.mem_inter_iff]
      exact ⟨mem_affineSpan k (Set.mem_insert p _), mem_affineSpan k hp⟩

Goal state after:
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 ha,

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.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
⊢ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) <
    c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x)

Tactic:
gcongr; refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc <;> positivity

Goal state after:
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, ∃ k ∈ t, w j ≠ 0 ∧ w k ≠ 0 ∧ p j ≠ p k

Tactic:
by
  grind [hf.convexOn.map_sum_le h₀ h₁ hmem |>.not_lt_iff_eq, hf.map_sum_eq_iff_of_nonneg 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
⊢ ContinuousSMul 𝕜 E

Tactic:
by
  rw [hp.withSeminorms_eq]
  exact ModuleFilterBasis.continuousSMul _

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: case inr
𝕜₁ : 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
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst : AddCommGroup F] [inst_1 : Module 𝕜₂ F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F], T2Space F → CompleteSpace (E →SLᵤ[σ, 𝔖] F)
hF : ¬T2Space F
⊢ CompleteSpace (E →SLᵤ[σ, 𝔖] F)

Tactic:
rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
    exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]

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

Goal state before:
pp: case h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst✝¹⁴ : SeminormedAddCommGroup E
inst✝¹³ : SeminormedAddCommGroup F
inst✝¹² : SeminormedAddCommGroup Fₗ
inst✝¹¹ : SeminormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜₂
inst✝⁸ : NontriviallyNormedField 𝕜₃
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : y ∈ ⇑ℓ '' s
⊢ ‖y‖ ≤ ‖ℓ‖ * M

Tactic:
obtain ⟨σ, hσ⟩ := (mem_image _ _ _).1 hy

Goal state after:
case h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst✝¹⁴ : SeminormedAddCommGroup E
inst✝¹³ : SeminormedAddCommGroup F
inst✝¹² : SeminormedAddCommGroup Fₗ
inst✝¹¹ : SeminormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜₂
inst✝⁸ : NontriviallyNormedField 𝕜₃
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : y ∈ ⇑ℓ '' s
σ : E
hσ : σ ∈ s ∧ ℓ σ = y
⊢ ‖y‖ ≤ ‖ℓ‖ * M
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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
⊢ 1⁻¹ * ‖f x‖₊ < ‖x‖₊⁻¹ * ‖f x‖₊

Tactic:
gcongr; exact hr.pos

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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
⊢ sSup ((fun x ↦ ‖f x‖) '' sphere 0 1) = ‖f‖

Tactic:
by
  simpa only [NNReal.coe_sSup, Set.image_image] using! NNReal.coe_inj.2 f.sSup_sphere_eq_nnnorm

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

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]

Goal state after:
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ ⊥) f = ⊥
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun x ↦ u x * a) f = a * limsup u f

Tactic:
by
  simpa [mul_comm] using limsup_const_mul_of_ne_top ha_top

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

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f

Tactic:
simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ ⊥) f = ⊥
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > ↑r
this : 0 < x
a : α
ha : ENNReal.ofReal (u a) < ENNReal.ofReal x
⊢ u a < x

Tactic:
exact (toReal_lt_of_lt_ofReal ha).trans_le' (by simp [toReal_ofReal'])

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

Goal state before:
pp: case neg.inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∫⁻ (a : α), ‖s.piecewise f g a‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
← lintegral_add_compl _ hs,

Goal state after:
case neg.inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ + ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∉ s
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖

Tactic:
· rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
        Real.norm_eq_abs, abs_of_nonneg hc]
      exact hf x hx

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∉ s
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝¹ : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst✝ : p.HolderTriple q' r
⊢ q⁻¹ = q'⁻¹

Tactic:
← inv_sub_inv_eq_inv q p hr,

Goal state after:
p q r : ℝ≥0∞
inst✝¹ : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst✝ : p.HolderTriple q' r
⊢ r⁻¹ - p⁻¹ = q'⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: ⊢ StrictConvexOn ℝ univ rexp

Tactic:
apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ
  rintro x y z - - hxy hyz
  trans exp y
  · have h1 : 0 < y - x := by linarith
    have h2 : x - y < 0 := by linarith
    rw [div_lt_iff₀ h1]
    calc
      exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
      _ = exp y * (1 - exp (x - y)) := by ring
      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
      _ = exp y * (y - x) := by ring
  · have h1 : 0 < z - y := by linarith
    rw [lt_div_iff₀ h1]
    calc
      exp y * (z - y) < exp y * (exp (z - y) - 1) := by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']
      _ = exp (z - y) * exp y - exp y := by ring
      _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ p⁻¹⁻¹ = ∞

Tactic:
← one_sub_inv 1 p

Goal state after:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ (1 - 1⁻¹)⁻¹ = ∞
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

Tactic:
rcases le_or_gt (1 + p * s) 0 with hs2 | hs2

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

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
⊢ 1 + p * s < (1 + s) ^ p
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q + 1 = p

Tactic:
← ENNReal.div_self (ne_zero q p) hq,

Goal state after:
case inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q + q / q = p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ConvexOn ℝ univ fun x ↦ b ^ x

Tactic:
convert! convexOn_exp.comp_linearMap (LinearMap.mul ℝ ℝ (Real.log b)) using 1
  ext x
  simp [Real.rpow_def_of_pos hb]

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp, hf.lintegral_map]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

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

Tactic:
refine
      NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal)
        (fun i => (z i).toNNReal) ?_ hp

Goal state after:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ ∑ i ∈ s, (w i).toNNReal = 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_lt_top.ne

Goal state after:
case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ x ∈ s, f x ^ p / p.toNNReal + ∑ x ∈ s, g x ^ q / q.toNNReal =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal

Tactic:
sum_div,

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ x ∈ s, f x ^ p / p.toNNReal + ∑ x ∈ s, g x ^ q / q.toNNReal =
    ∑ i ∈ s, f i ^ p / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
⊢ ∃ C ≤ A + B, HasSum (fun i ↦ (f i + g i) ^ p) (C ^ p)

Tactic:
have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'

Goal state after:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
⊢ ∃ C ≤ A + B, HasSum (fun i ↦ (f i + g i) ^ p) (C ^ p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim p μ ≤ liminf (fun n ↦ eLpNorm (f n) p μ) atTop

Tactic:
by
  obtain rfl | hp0 := eq_or_ne p 0
  · simp
  by_cases hp_top : p = ∞
  · simp_rw [hp_top]
    exact eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top h_lim
  simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
  have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
  exact eLpNorm'_lim_le_liminf_eLpNorm' hp_pos hf h_lim

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x ↦ RCLike.re (f x)) p μ
him : MemLp (fun x ↦ RCLike.im (f x)) p μ
x : α
⊢ f x = ((fun x ↦ ↑(RCLike.re (f x))) + fun x ↦ RCLike.I * ↑(RCLike.im (f x))) x

Tactic:
rw [Pi.add_apply, mul_comm, RCLike.re_add_im]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
⊢ f = g ↔ prodEquiv.symm f = prodEquiv.symm g

Tactic:
Equiv.apply_eq_iff_eq

Goal state after:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
⊢ f = g ↔ f = g
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | IsUnit x}

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | IsUnit x}
Module: Mathlib.Analysis.Normed.Module.Span

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
x : E
c : 𝕜
⊢ ‖(toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖

Tactic:
by
  rw [mul_comm]
  exact norm_smul _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E → F
g : F → G
hg : IsBoundedLinearMap 𝕜 g
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left✝¹ : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left✝ : 0 < Mg
hMg : ∀ (x : F), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ Mg * ‖f x‖ ≤ Mg * Mf * ‖x‖

Tactic:
hMf,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E → F
g : F → G
hg : IsBoundedLinearMap 𝕜 g
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left✝¹ : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left✝ : 0 < Mg
hMg : ∀ (x : F), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ Mg * (Mf * ‖x‖) ≤ Mg * Mf * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
⊢ ∃ M, 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖

Tactic:
by
    let ⟨C, hC_pos, hC⟩ := h.bound
    -- Using `C * ‖x‖` is tempting but `x` might be 0 and the constant must be positive!
    refine ⟨C * max ‖x‖ 1, by positivity, fun y ↦ (hC x y).trans ?_⟩
    rcases max_cases ‖x‖ 1 with hx | hx
    · grw [hx.1]
    · grw [hx.1, hx.2.le]

Goal state after: