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

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ (B a) (c • x) ∈ U

Tactic:
exact @hVW ⟨_, _⟩ ⟨ha, hc hx⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕜₂
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
𝕜 : Type u_11
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝², _] ⇑p
inst✝ : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ ∃ p₂, Continuous[inst✝⁵, _] ⇑p₂ ∧ p ≤ p₂.comp f

Tactic:
by
  obtain ⟨s, C, -, hqC⟩ := Seminorm.bound_comp_of_isInducing hp
    (PolynormableSpace.withSeminorms 𝕜₂ F) hf
  have := (PolynormableSpace.withSeminorms 𝕜₂ F).topologicalAddGroup
  exact ⟨_, Continuous.const_smul (continuous_finsetSup fun i _ => i.2) C, hqC⟩

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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this : ∀ (i : ι), IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
have : @IsTopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ (𝓝 0).IsCountablyGenerated

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ (⨅ i, comap (⇑(p i)) (𝓝 0)).IsCountablyGenerated
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

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

Tactic:
refine of_isOpen fun A hA ↦ h A fun K _ _ f hf ↦ ?_

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ (∀ (i : Set X),
      IsCompact i →
        IsClosed[TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ }]
          (⇑(CompactCoherentification.mk X) ⁻¹' A)) ↔
    ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)

Tactic:
← isClosed_coinduced

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯ =ᵐ[μ] ↑(Quotient.out f)

Tactic:
exact (AEStronglyMeasurable.ae_eq_mk _).symm

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y

Tactic:
by
  by_cases n : x = y
  · subst n
    exact ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩
  obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n
  replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
  let a := v x
  let b := v y
  let f' : s :=
    ((b - a) * (f x - f y)⁻¹) • (algebraMap _ s (f x) - (⟨f, hf⟩ : s)) + algebraMap _ s a
  refine ⟨f', f'.prop, ?_, ?_⟩
  · simp [a, b, f']
  · simp [a, b, f', inv_mul_cancel_right₀ hxy]

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

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂0, f a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae 0) fun i ↦ (f i).toReal
⊢ (essSup f 0).toReal = essSup (fun a ↦ (f a).toReal) 0

Tactic:
simp [essSup, limsup, limsSup]

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

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

Tactic:
inv_mul_cancel₀,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ 1

α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ q ≠ 0
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
rintro j - _; gcongr; apply sdiff_subset

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h✝ : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
x : α
x✝ : ‖g x‖ₑ = 0 ∧ ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h : ‖g x‖ₑ = 0
h' : ‖f x‖ₑ ≤ c * ‖g x‖ₑ
⊢ ‖f x‖ₑ = 0

Tactic:
by simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  (MeasurableEquiv.piEquivPiSubtypeProd α p).symm
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
this : ⇑e ⁻¹' univ.pi s = (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i
⊢ (∏ i, (μ ↑i) (s ↑i)) * ∏ i, (μ ↑i) (s ↑i) = ∏ i, (μ i) (s i)

Tactic:
exact Fintype.prod_subtype_mul_prod_subtype p fun i => μ i (s i)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
p : ℝ≥0∞
c : ε''
hc : ‖c‖ₑ ≠ ∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
by
  simp_all [MemLp, aestronglyMeasurable_const,
    eLpNorm_const_lt_top_iff_enorm hc hp_ne_zero hp_ne_top]

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
⊢ y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
hyz

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
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
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
have hy : 0 < y := hx.trans hxy

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ 0 < 1 → 1 < p → p⁻¹ ≠ ∞

Tactic:
by simp_all

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

Goal state before:
pp: p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
by exact_mod_cast h.coe.one_div_add_one_div

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

Goal state before:
pp: p q : ℝ≥0
h : p.HolderConjugate q
this : ↑1 ≤ ↑p
⊢ q = p / (p - 1)

Tactic:
exact_mod_cast NNReal.coe_sub this ▸ coe_one ▸ h.coe.conjugate_eq

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
⊢ y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)

Tactic:
hyz

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
⊢ (∫⁻ (a : α), ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) + fun x ↦ ‖g x‖ₑ) a ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr with a

Goal state after:
case h₁
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
a : α
⊢ ‖(f + g) a‖ₑ ≤ ((fun x ↦ ‖f x‖ₑ) + fun x ↦ ‖g x‖ₑ) a
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
⊢ (∫⁻ (a : α), ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) + fun x ↦ ‖g x‖ₑ) a ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr with a

Goal state after:
case h₁
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
a : α
⊢ ‖(f + g) a‖ₑ ≤ ((fun x ↦ ‖f x‖ₑ) + fun x ↦ ‖g x‖ₑ) a
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
⊢ eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

Tactic:
by
  refine le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)
  simp_rw [Pi.add_apply]
  exact enorm_add_le _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ

Tactic:
gcongr with a

Goal state after:
case hfg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)
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 ↦ b (f x) (g x)) r μ ≤ eLpNorm' (fun x ↦ ↑c • ‖f x‖ * ‖g x‖) r μ

Tactic:
simp only [eLpNorm']
      gcongr ?_ ^ _
      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
      gcongr
      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
      simpa using! ha

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
conv_rhs at h => enter [2]; rw [mul_comm]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
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}
⊢ (fun g ↦ ∑ i ∈ s, f i * g i) g ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
apply le_trans (inner_le_Lp_mul_Lq s f g hpq)

Goal state after:
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)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)

Tactic:
gcongr with a

Goal state after:
case hfg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
a : α
⊢ (f + g) a ^ p ≤ f a ^ p + g a ^ p
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
refine le_trans (sum_le_sum fun i _ ↦ ?_) (by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq)
  simp only [← abs_mul, le_abs_self]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1]

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, (f i + g i) ^ p = ∑ i ∈ s, |f i + g i| ^ p

case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p

case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, g i ^ p = ∑ i ∈ s, |g i| ^ p
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ ¬ε ≤ edist (f n x) (g x)

Tactic:
edist_comm,

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, edist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ ¬ε ≤ edist (g x) (f n x)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ∞

Tactic:
refine lt_of_le_of_lt ?_ ENNReal.one_lt_top

Goal state after:
case left
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ ≤ 1
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜₁ : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_8
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedSpace 𝕜₁ E
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₃₂ : 𝕜₃ →+* 𝕜₂
inst✝⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomIsometric σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomIsometric σ₁₂
e : F ≃ₛₗᵢ[σ₂₃] G
f : E →SL[σ₁₂] F
r : ℝ≥0
⊢ ‖↑↑e ∘SL f‖₊ ≤ r ↔ ‖f‖₊ ≤ r

Tactic:
simp [opNNNorm_le_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = ((↑(f x))⁻¹ * ↑(f x)) • g x

Tactic:
inv_mul_cancel₀,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = 1 • g x

α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞

Tactic:
· exact measure_ne_top_of_subset sdiff_subset h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞

Tactic:
· exact measure_ne_top_of_subset sdiff_subset h

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
⊢ IntegrableOn f t μ

Tactic:
let u := { x ∈ s | f x ≠ 0 }

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
⊢ IntegrableOn f t μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
calc
      ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ := norm_le_insert _ _
      _ ≤ ‖f₀ a‖ + g a := by gcongr

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

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
l : Filter α
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ

Tactic:
by
  refine ⟨?_, fun h ↦ h.filter_mono inf_le_left⟩
  rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hf⟩
  refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩
  filter_upwards [hu] with x hx using (and_iff_left hx).symm

Goal state after: