mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ 𝓝 0 = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)

Tactic:
nhds_induced,

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ comap (⇑f) (𝓝 (f 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)
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
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : l.Germ M
c : α → M
⊢ ↑c • 0 = 0

Tactic:
by simp only [← coe_zero, ← coe_smul', smul_zero]

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

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

Tactic:
nhds_induced,

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

Goal state before:
pp: f : Filter ℝ
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ sInf {a | ∀ᶠ (n : ℝ) in f, n ≤ a} = 0

Tactic:
sInf_of_not_bddBelow

Goal state after:
f : Filter ℝ
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ 0 = 0

f : Filter ℝ
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ¬BddBelow {a | ∀ᶠ (n : ℝ) in f, n ≤ a}
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ f.limsInf = 0

Tactic:
by
  rw [limsInf]
  convert! sSup_empty
  simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

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

Goal state before:
pp: case inr.inl
α : 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 : r < 0
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun a ↦ (u a).toReal) f ≤ r

Tactic:
exact iff_of_false (hr.trans_le toReal_nonneg).not_ge
      (hr.trans_le <| le_limsup_of_frequently_le (by simpa)).not_ge

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  obtain rfl | h'p := eq_or_ne p ∞
  · simp only [eLpNorm_exponent_top, ENNReal.toReal_top, _root_.div_zero, ENNReal.rpow_zero,
      mul_one]
    exact eLpNormEssSup_indicator_const_le _ _
  let t := toMeasurable μ s
  calc
    eLpNorm (s.indicator fun _ => c) p μ ≤ eLpNorm (t.indicator fun _ ↦ c) p μ :=
      eLpNorm_mono_enorm (enorm_indicator_le_of_subset (subset_toMeasurable _ _) _)
    _ = ‖c‖ₑ * μ t ^ (1 / p.toReal) :=
      eLpNorm_indicator_const (measurableSet_toMeasurable ..) hp h'p
    _ = ‖c‖ₑ * μ s ^ (1 / p.toReal) := by rw [measure_toMeasurable]

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ log z - log y < y⁻¹ * (z - y)

Tactic:
have hyz' : 0 < z / y := by positivity

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
⊢ log z - log y < y⁻¹ * (z - y)
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
s t : Set α
f : α → E
x : α
⊢ ‖(s.indicator f - t.indicator f) x‖ = ‖(s ∆ t).indicator f x‖

Tactic:
by simp [Set.apply_indicator_symmDiff norm_neg]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ MemLp f p μ'

Tactic:
refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩
  grw [eLpNorm_le_of_measure_le_smul hμ'_le]
  exact ENNReal.mul_lt_top (Ne.lt_top (by simp [hc])) hf.2

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 : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Tactic:
by
  have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy
  simp only [Pi.neg_apply] at key
  linear_combination key

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

Goal state before:
pp: E : Type u_4
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ AEStronglyMeasurable f μ

Tactic:
exact (hf.stronglyMeasurable_of_hasCompactSupport h'f).aestronglyMeasurable

Goal state after:
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 : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x) ≤
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y)

Tactic:
gcongr _ + (a * b) • ?_; exact hfg.smul_add_smul_le_smul_add_smul hx hy

Goal state after:
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
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y) ≤
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x)

Tactic:
gcongr _ + (a * b) • ?_; exact hfg.smul_add_smul_le_smul_add_smul hx hy

Goal state after:
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 μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
· refine Eq.trans_le ?_ zero_le
    exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.nonneg hf hf_zero

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
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 : 0 + q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

pp: case inr
α : 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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
· rw [zero_add] at hpq
    simp [hpq]

Goal state after:
case inr
α : 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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, z j ≠ ∑ i ∈ s, w i * z i

Tactic:
contrapose!
  rw [← geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz]
  exact geom_mean_le_arith_mean_weighted s w z (hw · · |>.le) hw' hz |>.ge_iff_eq

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, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, w j ≠ 0 ∧ z j ≠ ∑ i ∈ s, w i * z i

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

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case mp
ι : 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 : ∑ i ∈ s, w i * z i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

Tactic:
exact (lt_self_iff_false _).mp h

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0
⊢ w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
    Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
    mul_assoc] using! geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃, w₄] ![p₁, p₂, p₃, p₄]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f - g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
by
  simpa only [sub_eq_add_neg, eLpNorm_neg] using eLpNorm_add_le' hf hg.neg p

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

Goal state before:
pp: α : 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
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p + 1 / q).toReal
⊢ 1 / r.toReal = 1 / p.toReal + 1 / q.toReal

Tactic:
rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this

Goal state after:
α : 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
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p).toReal + (1 / q).toReal
⊢ 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
inst✝ : Fact (1 ≤ p)
f : ↥(Lp E p ν)
⊢ ‖(LpToLpOfMeasureLeSMulₗ hc h) f‖ ≤ c.toReal ^ (1 / p).toReal * ‖f‖

Tactic:
simp only [← toReal_enorm]
  rw [ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
  grw [enorm_LpToLpOfMeasureLeSMulₗ_apply_le]
  simp [ENNReal.mul_eq_top, hc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
⊢ (fun t ↦ (1 - t)⁻¹ʳ) =O[𝓝 0] fun _t ↦ 1

Tactic:
by
  simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
  refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by simp, fun t ht ↦ ?_⟩
  rw [dist_zero_right] at ht
  have ht' : ‖t‖ < 1 := by linarith
  simp only [inverse_one_sub t ht', norm_one, mul_one]
  change ‖∑' n : ℕ, t ^ n‖ ≤ _
  have := tsum_geometric_le_of_norm_lt_one t ht'
  have : (1 - ‖t‖)⁻¹ ≤ 2 := inv_le_of_inv_le₀ (by simp) (by linarith)
  linarith

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

case neg
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖f x‖ ≤ C * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ Subsingleton E ∨ 0 < ‖↑e.symm‖

Tactic:
right

Goal state after:
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ 0 < ‖↑e.symm‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : Semiring 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : Module 𝕜 F
f : E → F
𝕜' : Type u_5
c : 𝕜'
inst✝³ : SeminormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
x : E
⊢ ‖c‖ * ‖f x‖ ≤ ‖c‖ * (M * ‖x‖)

Tactic:
hM

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : Semiring 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : Module 𝕜 F
f : E → F
𝕜' : Type u_5
c : 𝕜'
inst✝³ : SeminormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
x : E
⊢ ‖c‖ * (M * ‖x‖) ≤ ‖c‖ * (M * ‖x‖)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: case refine_1
𝕜 : Type u_1
ι✝ : Type u_2
E : ι✝ → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)
inst✝⁵ : (i : ι✝) → AddCommGroup (E i)
inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ {s | IsVonNBounded 𝕜 s}.Nonempty

pp: case refine_2
𝕜 : Type u_1
ι✝ : Type u_2
E : ι✝ → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)
inst✝⁵ : (i : ι✝) → AddCommGroup (E i)
inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) {s | IsVonNBounded 𝕜 s}

Tactic:
· exact ⟨∅, isVonNBounded_empty _ _⟩

Goal state after:
case refine_2
𝕜 : Type u_1
ι✝ : Type u_2
E : ι✝ → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)
inst✝⁵ : (i : ι✝) → AddCommGroup (E i)
inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) {s | IsVonNBounded 𝕜 s}
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set F
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
φ : ((i : ι) → E i) →L[𝕜] (i : ι) → E₁ i := ContinuousLinearMap.piMap f
⊢ ∃ ia,
    (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux x ∈ {f | MapsTo ⇑f (U, V).1 (U, V).2}

Tactic:
exact ⟨(φ '' U, V), ⟨hU.image φ, hV⟩, fun g hg ↦ hg.comp (mapsTo_image _ _)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → δ
hf : MeasurableEmbedding f
g : δ → ε
⊢ Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Tactic:
by
  simp_rw [← memLp_one_iff_integrable]
  exact hf.memLp_map_measure_iff

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊔ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢
  exact hf.sup hg

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0

Tactic:
simp [hε']

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε = ∞
⊢ μ {x | ε < ‖f x‖ₑ} < ∞

Tactic:
simp [hε']

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

Goal state before:
pp: case h1.inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
j : ι
a✝ : j ∈ univ
⊢ (if j = j then ‖m₁ j - m₂ j‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ update (fun x ↦ max ‖m₁‖ ‖m₂‖) j ‖m₁ - m₂‖ j

Tactic:
simp only [ite_true, Function.update_self]
          exact norm_le_pi_norm (m₁ - m₂) _

Goal state after: