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

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s
⊢ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
I

Goal state after:
case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s
I : Finset ι
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
⊢ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
I

Goal state after:
case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
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
x x' : E
y : F
⊢ (f (x + x')) y = (f x) y + (f x') y

Tactic:
rw [f.map_add, add_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding ((fun f ↦ (UniformOnFun.ofFun {s | IsVonNBounded 𝕜' s}) ⇑f) ∘ restrictScalars 𝕜')
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 : ‖f x‖ₑ ≤ ↑M * ‖x‖ₑ
⊢ ‖f x‖ ≤ ↑M * ‖x‖

Tactic:
simp only [← ofReal_norm, ← ENNReal.ofReal_coe_nnreal] at hM

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 : ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal ↑M * ENNReal.ofReal ‖x‖
⊢ ‖f x‖ ≤ ↑M * ‖x‖
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a ↦ (F i) a) (⇑f) p

Tactic:
simp [isUniformEmbedding_uniformFunOfFun.isInducing.tendsto_nhds_iff,
    UniformFun.tendsto_iff_tendstoUniformly, Function.comp_def]

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

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

Tactic:
rw [← coeFn_le] at hf hg ⊢

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
⊢ ↑g a✝ ≤ ↑f' a✝ → ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝ → ↑(f ⊔ g) a✝ ≤ ↑f' a✝

Tactic:
hag

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

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

Tactic:
rw [← coeFn_le] at hf hg ⊢

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
⊢ ↑f' a✝ ≤ ↑g a✝ → ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝ → ↑f' a✝ ≤ ↑(f ⊓ g) a✝

Tactic:
hag

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
⊢ ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝ → ↑f' a✝ ≤ ↑(f ⊓ g) a✝
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurablePow ℝ≥0∞ ℝ

Tactic:
refine ⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩

Goal state after:
case refine_1
⊢ Measurable fun p ↦ (↑p.1, p.2).1 ^ (↑p.1, p.2).2

case refine_2
⊢ Measurable fun x ↦ (∞, x).1 ^ (∞, x).2
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

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

Tactic:
obtain rfl | h'p := eq_or_ne p ∞

Goal state after:
case inr.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hp : ∞ ≠ 0
⊢ eLpNorm (s.indicator fun x ↦ c) ∞ μ ≤ ‖c‖ₑ * μ s ^ (1 / ∞.toReal)

case inr.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
this : (piPremeasure fun i ↦ (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))
⊢ Measure.map (⇑e) (Measure.pi μ) = μ default

Tactic:
simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]

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

Goal state before:
pp: s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ 0 < 1 + p * s

Tactic:
← neg_lt_iff_pos_add'

Goal state after:
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ -1 < p * s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

Tactic:
rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
    h.inv_add_inv_eq_one]

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

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

Tactic:
obtain rfl | hq := eq_or_ne q ∞

Goal state after:
case inr.inl
p : ℝ≥0∞
hp : p ≠ ∞
h : p.HolderConjugate ∞
⊢ p * ∞ = p + ∞

case inr.inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
hq : q ≠ ∞
⊢ p * q = p + q
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
h : p.HolderConjugate q
⊢ p / q = p - 1

Tactic:
obtain rfl | hq := eq_or_ne q ∞

Goal state after:
case inl
p : ℝ≥0∞
h : p.HolderConjugate ∞
⊢ p / ∞ = p - 1

case inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q = p - 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = cosh x + t * sinh x

Tactic:
by rw [cosh_eq, sinh_eq]; ring

Goal state after:
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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
by
  by_cases hp0 : p.toReal = 0
  · simp only [hp0, ENNReal.rpow_zero]
    filter_upwards with _
    rw [liminf_const (1 : ℝ≥0∞)]
    exact ENNReal.one_lt_top
  have hp : p ≠ 0 := fun h => by simp [h] at hp0
  have hp' : p ≠ ∞ := fun h => by simp [h] at hp0
  refine
    ae_lt_top (.liminf fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
      (lt_of_le_of_lt
          (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
          (lt_of_le_of_lt ?_ (by finiteness : (R : ℝ≥0∞) ^ p.toReal < ∞))).ne
  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp hp', one_div] at hbdd
  simp_rw [liminf_eq, eventually_atTop]
  exact
    sSup_le fun b ⟨a, ha⟩ =>
      (ha a le_rfl).trans ((ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hp hp')).1 (hbdd _))

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : 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 : ∑ i ∈ s, w i * z i = ∞
⊢ False

Tactic:
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum

Goal state after:
ι : 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 : ∞ ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h : ∑ i ∈ s, w i * z i = ∞
⊢ False
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * b * (x - y) ^ 2 = a • x ^ 2 + b • y ^ 2 - (a • x + b • y) ^ 2

Tactic:
obtain rfl := eq_sub_of_add_eq hab; simp only [smul_eq_mul]; ring

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ p⁻¹ ≠ ∞

Tactic:
simpa using h.1.ne'

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1

Tactic:
ENNReal.inv_lt_one,

Goal state after:
case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ 1 < ENNReal.ofReal p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 < w₁
hw₂ : 0 < w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ p₁ ^ w₁ * p₂ ^ w₂ < w₁ * p₁ + w₂ * p₂ ↔ p₁ ≠ p₂

Tactic:
by
  have := geom_mean_lt_arith_mean_weighted_iff_of_pos univ ![w₁, w₂] ![p₁, p₂]
  simp at this
  grind

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

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
let q2 := p2.conjExponent

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a.toNNReal * b.toNNReal = a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ a.toNNReal ^ p = b.toNNReal ^ q

Tactic:
simp [young_inequality_real_eq_iff a.toNNReal b.toNNReal hpq]

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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ eLpNorm' (fun x ↦ ↑c • ‖f x‖ * ‖g x‖) r μ ≤ ↑c * eLpNorm' f p μ * eLpNorm' g q μ

Tactic:
by
      simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
      rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
      gcongr
      simpa only [eLpNorm', enorm_mul, enorm_norm] using!
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
⊢ (∑' (i : ι), (f i * g i) ^ r) ^ (1 / r) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
convert!
    rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos') |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg
  have hr := hpqr.pos'.ne'
  simp only [← rpow_mul, mul_rpow]
  field_simp

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0 := by
      simpa [ENNReal.rpow_eq_zero_iff, hpq.pos, hpq.symm.pos, asymm hpq.pos, asymm hpq.symm.pos,
        sum_eq_zero_iff_of_nonneg] using H
    have : ∀ i ∈ s, f i * g i = 0 := fun i hi => by rcases H with H | H <;> simp [H i hi]
    simp [sum_eq_zero this]

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

Goal state before:
pp: case zero
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg 0 ≤ k
⊢ μ {x | 2⁻¹ ^ 0 ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ 0

Tactic:
exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
⊢ eLpNorm (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
simp only [q_zero, ENNReal.toReal_zero, Real.rpow_zero]

Goal state after:
case pos
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
⊢ eLpNorm (fun x ↦ 1) (p / 0) μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
rw [eLpNorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F✝
g✝ : E → F✝
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((c • B g).compLp f) x = (c • B g) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
⊢ ↑↑(c • (B g).compLp f) x = (c • ↑↑((B g).compLp f)) x →
    ↑↑((compLpₗ p μ (B (c • g))) f) x = ↑↑(((RingHom.id 𝕜) c • compLpₗ p μ (B g)) f) x

Tactic:
hsmul

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F✝
g✝ : E → F✝
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((c • B g).compLp f) x = (c • B g) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hsmul : ↑↑(c • (B g).compLp f) x = (c • ↑↑((B g).compLp f)) x
⊢ ↑↑((compLpₗ p μ (B (c • g))) f) x = ↑↑(((RingHom.id 𝕜) c • compLpₗ p μ (B g)) f) x
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : PseudoEMetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, Tendsto ns atTop u ∧ TendstoInMeasure μ (fun n ↦ f (ns n)) atTop g

Tactic:
obtain ⟨ns, h_tendsto_ns⟩ : ∃ ns : ℕ → ι, Tendsto ns atTop u := exists_seq_tendsto u
  exact ⟨ns, h_tendsto_ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩

Goal state after:
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
by
  rw [Subsingleton.elim emb Embedding.fintype]
  refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α <;> clear! α
  · let := Fintype.ofEquiv _ e.symm
    rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
  · rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]
    exact ⟨Embedding.ofIsEmpty, fun x ↦ DFunLike.ext _ _ isEmptyElim⟩
  · classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]

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✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 = ‖ContinuousLinearMap.id 𝕜 E‖

Tactic:
ContinuousLinearMap.norm_id

Goal state after:
𝕜 : 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 σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 = 1