mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case hms
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
exact ht

Goal state after:
case hms
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s)
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ + c₂), continuous_toFun := ⋯ } =
    { toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } +
      { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ }

Tactic:
ext _; exact (algebraMap R A).map_add _ _

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

Goal state before:
pp: ⊢ Measurable fun x ↦ Real.arcsin (x.im / ‖x‖)

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Measurable fun x ↦ Real.arcsin ((-x).im / ‖x‖) + Real.pi

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Measurable fun x ↦ Real.arcsin ((-x).im / ‖x‖) - Real.pi

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable fun x ↦ ↑(f x)

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Measurable fun p ↦ cexp (log p.1 * p.2)

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Measurable fun p ↦ ↑p.1 ^ ↑p.2

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Measurable fun p ↦ ↑p.1 ^ p.2

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Measurable fun p ↦ ↑(p.1 ^ p.2)

Tactic:
by fun_prop

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 γ
inst✝² : LinearOrder γ
inst✝¹ : OrderClosedTopology γ
inst✝ : Zero γ
f : α →ₘ[μ] γ
⊢ Continuous[inst✝³, inst✝³] fun x ↦ max x 0

Tactic:
by fun_prop

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 γ
inst✝² : LinearOrder γ
inst✝¹ : OrderClosedTopology γ
inst✝ : Zero γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ max (f x) 0) μ

Tactic:
by fun_prop

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ (Measure.pi μ).FiniteSpanningSetsIn (univ.pi '' univ.pi C)

Tactic:
refine ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).getD default i),
    fun n => ?_, fun n => ?_, ?_⟩ <;>
  -- TODO (kmill) If this let comes before the refine, while the noncomputability checker
  -- correctly sees this definition is computable, the Lean VM fails to see the binding is
  -- computationally irrelevant. The `noncomputable section` doesn't help because all it does
  -- is insert `noncomputable` for you when necessary.
  let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).getD default

Goal state after:
case refine_1
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (univ.pi fun i ↦ (hμ i).set ((decode n).getD default i)) ∈ univ.pi '' univ.pi C

case refine_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (Measure.pi μ) (univ.pi fun i ↦ (hμ i).set ((decode n).getD default i)) < ∞

case refine_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (⋃ i, univ.pi fun i_1 ↦ (hμ i_1).set ((decode i).getD default i_1)) = univ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ Measurable (eval i)

Tactic:
by fun_prop

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : MeasurableSet s
h2s : (μ i) s = 0
⊢ Measurable (eval i)

Tactic:
by fun_prop

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ioi (f i)) =ᵐ[Measure.pi μ] Ici f

Tactic:
rw [← pi_univ_Ici]; exact pi_Ioi_ae_eq_pi_Ici

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' : ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ = 0
⊢ AEMeasurable (fun a ↦ ‖g a‖ₑ ^ p) μ

Tactic:
by fun_prop

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 ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ eLpNorm (fun x ↦ c) p μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
have hp : 0 < p.toReal := ENNReal.toReal_pos hp_ne_zero hp_ne_top

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
⊢ eLpNorm (fun x ↦ c) p μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
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
s : Set ((i : ι) → X i)
⊢ (μ default) (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)

Tactic:
congr 1

Goal state after:
case e_6
ι : 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 := ⋯
s : Set ((i : ι) → X i)
⊢ eval default '' s = ⇑e.symm ⁻¹' s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
congr 1

Goal state after:
case neg.e_a
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
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:
exact_mod_cast h.coe.one_div_add_one_div

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

Goal state before:
pp: p q r : ℝ≥0
h : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
by exact_mod_cast h.coe.inv_inv_add_inv

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 ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
have : 0 ≤ p.toReal⁻¹ := by positivity

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
this : 0 ≤ p.toReal⁻¹
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ ‖f x‖₊) (ae μ), (fun x1 x2 ↦ x1 ≤ x2) x (eLpNormEssSup f μ).toNNReal

Tactic:
simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ ‖f x‖₊) (ae μ), ↑x ≤ eLpNormEssSup f μ
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (a • -x + b • -y) = log (-(a • x + b • y))

Tactic:
congr 1

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • -x + b • -y = -(a • x + b • y)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0

Tactic:
refine lintegral_congr_ae ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f * g =ᵐ[μ] 0
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 • f x • g x + b • f y • g y ≤ (a • f x + b • f y) • (a • g x + b • g y)

Tactic:
calc a • f x • g x + b • f y • g y
        = (a * (a + b)) • (f x • g x) + (b * (a + b)) • (f y • g y) := by simp_rw [hab, mul_one]
    _ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by
        simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel
    _ ≤ (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g y + f y • g x) := by
        gcongr _ + (a * b) • ?_; exact hfg.smul_add_smul_le_smul_add_smul hx hy
    _ = _ := ?_

Goal state after:
𝕜 : 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 y + f y • g x) =
    (a • f x + b • f y) • (a • g x + b • g y)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
add_zero

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

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p✝ : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
⊢ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 = (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
congr 1

Goal state after:
case e_a
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p✝ : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
⊢ ∏ i ∈ s, 1 = ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x ↦ x ^ -[n+1]

Tactic:
zpow_negSucc,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x ↦ (x ^ (n + 1))⁻¹
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

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
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
· exact (lt_self_iff_false _).mp h

Goal state after:
ι : 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q

Tactic:
have h_nnnorm_le_eLpNorm_ess_sup := enorm_ae_le_eLpNormEssSup f μ

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_nnnorm_le_eLpNorm_ess_sup : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst✝ : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ MemLp (∑ i ∈ s, f i) p μ

Tactic:
by
  convert! memLp_finsetSum s hf using 1
  ext x
  simp

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 1 / q ≤ 1 / p - 0

Tactic:
sub_zero,

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 1 / q ≤ 1 / p
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 α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ AEMeasurable (fun x ↦ ‖g x‖ₑ ^ p.toReal) μ

Tactic:
by fun_prop

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

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

Tactic:
refine (lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ liminf (fun i ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop = liminf (fun n ↦ eLpNorm' (f n) p μ) atTop ^ p
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf : (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun x ↦ μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 ↑0)

Tactic:
exact h ε hε

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun x ↦ μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (ENNReal.toNNReal 0))

Tactic:
exact h ε hε

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n - f_lim)) p μ ≠ ∞

Tactic:
exact Lp.eLpNorm_ne_top _

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 g : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑(-f + g)) p μ).toReal = (eLpNorm (-↑↑f + ↑↑g) p μ).toReal

Tactic:
congr 1

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(-f + g)) p μ = eLpNorm (-↑↑f + ↑↑g) p μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: 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

Tactic:
skip

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
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4.e'_5
ι : 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) ^ (1 / p) = (∑ i ∈ s, |f i| ^ p) ^ (1 / p)

Tactic:
congr 1

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

Goal state before:
pp: case e'_4.e'_6
ι : 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) ^ (1 / p) = (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Tactic:
congr 1

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