mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
⊢ IsVonNBounded R S

Tactic:
isVonNBounded_iff_absorbing_le,

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
⊢ absorbing R S ≤ 𝓝 0
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
⊢ Continuous[x✝¹, x✝] ⇑f

Tactic:
have : IsTopologicalAddGroup E := hp.topologicalAddGroup

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
⊢ Continuous[x✝¹, x✝] ⇑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∞
hM : ∀ (x : E), ‖f x‖ₑ ≤ M * ‖x‖ₑ
⊢ ‖f‖ₑ ≤ M

Tactic:
rcases eq_top_or_lt_top M with rfl | h'M
  · simp
  lift M to NNReal using h'M.ne
  simp only [← ofReal_norm, ENNReal.ofReal_le_coe]
  apply opNorm_le_bound _ (by positivity) (fun x ↦ ?_)
  specialize hM x
  simp only [← ofReal_norm, ← ENNReal.ofReal_coe_nnreal] at hM
  rwa [← ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_le_ofReal_iff (by positivity)] at hM

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyCoherentSpace X
s : Set X
⊢ IsOpen[inst✝¹] s ↔
    ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst✝¹] f → IsOpen (f ⁻¹' s)

Tactic:
refine ⟨fun hs _ _ _ _ hf ↦ hs.preimage hf, fun hs ↦ isOpen_iff |>.mpr ?_⟩

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst✝¹] f → IsOpen (f ⁻¹' s)
⊢ ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsOpenMap ⇑(CompactCoherentification.mk X)

Tactic:
intro A hA

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
hA : IsOpen[inst✝] A
⊢ IsOpen[instTopologicalSpace] (⇑(CompactCoherentification.mk X) '' A)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)

Tactic:
apply continuous_map_of_continuousOn
  intros
  exact hf.continuousOn

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖y‖ * ‖x‖

Tactic:
exact (flip f).le_opNorm₂ y x

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
x : α
⊢ Inseparable (s.piecewise f (⇑f') x) (f' x)

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
x : α
hx : x ∈ s
⊢ Inseparable (s.piecewise f (⇑f') x) (f' x)

case neg
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
x : α
hx : x ∉ s
⊢ Inseparable (s.piecewise f (⇑f') x) (f' x)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mp
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
⊢ (∃ b, ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a) →
    ∃ x,
      ∃ (hx : 0 ≤ x),
        ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
          (∀ᶠ (a : ι) in f, ↑(u a) ≤ ↑(NNReal.mk x_1 hx_1)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk x_1 hx_1)

Tactic:
rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, fun x _ ↦ by simpa [*] using hb _⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
⊢ c • (f + g) = c • f + c • g

Tactic:
by ext x; exact smul_add (c x) (f x) (g x)

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (uniformOn ↑s) ↑t = ↑(#(s ∩ t)) / ↑(#s)

Tactic:
rw [uniformOn, cond_apply hs, Measure.count_apply_finset' hs, ← coe_inter,
    Measure.count_apply_finset']

Goal state after:
Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (↑(#s))⁻¹ * ↑(#(s ∩ t)) = ↑(#(s ∩ t)) / ↑(#s)

Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ MeasurableSet ↑(s ∩ t)
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : Measurable g
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf hgf_co hg_bdd)
  refine limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)
  rw [eventually_map] at h_le ⊢
  rw [ae_map_iff hf (measurableSet_le hg measurable_const)]
  exact h_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) f
⊢ μ {y | essSup f μ < f y} = 0

Tactic:
by
  simp_rw [← not_le]
  exact ae_le_essSup hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁴ : SMul 𝕜 γ
inst✝³ : ContinuousConstSMul 𝕜 γ
inst✝² : SMul 𝕜' γ
inst✝¹ : ContinuousConstSMul 𝕜' γ
inst✝ : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ mk (a • b • f) ⋯ = mk (b • a • f) ⋯

Tactic:
smul_comm

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

Goal state before:
pp: case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
x : α
⊢ ‖s.piecewise f g x‖ₑ = s.piecewise (fun x ↦ ‖f x‖ₑ) (fun x ↦ ‖g x‖ₑ) x

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ ‖s.piecewise f g x‖ₑ = s.piecewise (fun x ↦ ‖f x‖ₑ) (fun x ↦ ‖g x‖ₑ) x

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ ‖s.piecewise f g x‖ₑ = s.piecewise (fun x ↦ ‖f x‖ₑ) (fun x ↦ ‖g x‖ₑ) x
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : 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 : α
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖

Tactic:
by_cases hx : x ∈ s

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

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.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ∞

Tactic:
rw [lintegral_rpow_enorm_eq_rpow_eLpNorm' hq0_lt]
  exact ENNReal.rpow_lt_top_of_nonneg (le_of_lt hq0_lt) (ne_of_lt hfq)

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

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

Tactic:
by
  apply ENNReal.sub_eq_of_eq_add (ne_of_lt ?_) (inv_eq p q r)
  calc
    q⁻¹ ≤ r⁻¹ := HolderTriple.inv_le_inv q p r
    _ < ∞ := by simpa using pos_iff_ne_zero.mpr hr

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

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr₀ : r ≠ 0
hr : r ≠ ∞
⊢ r * (p⁻¹ + q⁻¹) = 1⁻¹

Tactic:
inv_add_inv_eq_inv p q r,

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

Goal state before:
pp: case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 < 0 + p

Tactic:
zero_add

Goal state after:
case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 < p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : False ∨ s = 0
⊢ s = 0

Tactic:
false_or

Goal state after:
s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : s = 0
⊢ s = 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 0 + p < 1

Tactic:
zero_add

Goal state after:
case inl
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ p < 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

Tactic:
false_or

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

Goal state before:
pp: p q : ℝ≥0∞
h : p.toReal.HolderConjugate q.toReal
⊢ p.HolderConjugate q

Tactic:
by
  rw [Real.HolderConjugate] at h
  exact HolderTriple.of_toReal (toReal_one ▸ h)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
hq0_lt : 0 < q
hf_zero : f =ᵐ[μ] 0
⊢ eLpNorm' 0 q μ = 0

Tactic:
eLpNorm'_zero hq0_lt

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
hq0_lt : 0 < q
hf_zero : f =ᵐ[μ] 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
simp only [smul_eq_mul, antivaryOn_iff_smul_rearrangement]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ w i * z i = w i * x

Tactic:
rw [hwi, zero_mul, zero_mul]

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

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

Tactic:
zero_add

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

Goal state before:
pp: case inr.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
hq : 0 < q
h2p : 1 < 1 / p
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1 := by simp [hpq]

Goal state after:
case inr.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
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:

Tactic:
∫⁻ a, ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ
          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ := by simp [hi₀]
        _ = ∫⁻ a, f i₀ a ^ p i₀ * (∏ i ∈ s, f i a ^ q i) ^ (1 - p i₀) ∂μ := by
            simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
              div_mul_cancel₀ (h := h2pi₀)]
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∫⁻ a, ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀) := by
            apply ENNReal.lintegral_mul_norm_pow_le
            · exact hf i₀ <| mem_insert_self ..
            · exact s.aemeasurable_fun_prod fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _
            · exact h2p i₀ <| mem_insert_self ..
            · exact hpi₀
            · apply add_sub_cancel
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ q i) ^ (1 - p i₀) := by
            gcongr -- behavior of gcongr is heartbeat-dependent, which makes code really fragile...
            exact ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q
        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
            simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
              div_mul_cancel₀ (h := h2pi₀)]
        _ = ∏ i ∈ insert i₀ s, (∫⁻ a, f i a ∂μ) ^ p i := by simp [hi₀]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_1
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∀ i ∈ s, 0 < w i / ∑ i ∈ s, w i

Tactic:
exact fun i hi ↦ div_pos (hw i hi) hw'

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ μ Set.univ ^ (1 / p.toReal) < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (by simp [hp_pos.le]) (by finiteness)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1}
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
simpa only [mul_one] using
      mul_le_mul_right (NNReal.rpow_le_one hg (le_of_lt hpq.symm.one_div_pos)) _

Goal state after:
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
f : α → E
hf : MemLp f p μ
⊢ ↑‖MemLp.toLp f hf‖₊ = eLpNorm f p μ

Tactic:
nnnorm_toLp f hf,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ ↑(eLpNorm f p μ).toNNReal = eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
⊢ ‖f‖ ≤ ‖g‖

Tactic:
by
  rw [norm_def, norm_def]
  exact ENNReal.toReal_mono (by finiteness) (eLpNorm_mono_ae h)

Goal state after:
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
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : eLpNorm (↑g) p μb < ∞
f : α → β
hf : MeasurePreserving f μ μb
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ < ∞

Tactic:
rwa [eLpNorm_compMeasurePreserving]

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

Goal state before:
pp: case hmn
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ⋯
S : ℕ → Set α := ⋯
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := ⋯
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ k ≤ n + 1

Tactic:
omega

Goal state after:
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
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(c • f) =ᵐ[ν] (RingHom.id ℝ) c • ↑↑f

Tactic:
grw [Lp.coeFn_smul]

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
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
this : μ ≪ ν
⊢ c • ↑↑f =ᵐ[ν] (RingHom.id ℝ) c • ↑↑f
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ g =ᵐ[μ] h

Tactic:
obtain ⟨ns', h2, h2'⟩ := (hh.comp h1).exists_seq_tendsto_ae'

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
⊢ g =ᵐ[μ] h