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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
⊢ BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))

Tactic:
by
    have : ∀ᶠ x in 𝓝 0, ∀ k, q i (f k x) ≤ 1 := by
      filter_upwards [Metric.equicontinuousAt_iff_right.mp (H.equicontinuous 0) 1 one_pos]
        with x hx k
      simpa using! (hx k).le
    have bdd : BddAbove (range fun k ↦ (q i).comp (f k)) :=
      Seminorm.bddAbove_of_absorbent (absorbent_nhds_zero this)
        (fun x hx ↦ ⟨1, forall_mem_range.mpr hx⟩)
    rw [← Seminorm.coe_iSup_eq bdd]
    refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩
    filter_upwards [this] with x hx
    simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using! hx

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set E × ℝ
s : Set E
r : ℝ
x✝ : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
⊢ ∃ r_1 > 0, ContinuousLinearMap.seminorm.ball 0 r_1 ⊆ {f | ∀ x ∈ (s, r).1, f x ∈ closedBall 0 (s, r).2}

Tactic:
· rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, hε⟩
    rcases exists_pos_mul_lt hr ε with ⟨δ, hδ₀, hδ⟩
    refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
    simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢
    rw [mul_comm] at hδ
    exact le_trans (le_of_opNorm_le_of_le _ hf.le (hε _ hx)) hδ.le

Goal state after:
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), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ‖x‖₊ ≠ 0

Tactic:
← NNReal.coe_ne_zero

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
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ↑‖x‖₊ ≠ 0
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
⊢ IsLeast {C | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊

Tactic:
by
  simpa only [← opNNNorm_le_iff] using! isLeast_Ici

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ((s.sup q).comp f) x = (s.sup (q.comp f)) x

Tactic:
Seminorm.comp_apply,

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ (s.sup q) (f x) = (s.sup (q.comp f)) x
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ * ‖L‖ ≤ 1 * ‖L‖

Tactic:
gcongr; apply norm_compL_le

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'
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x

Tactic:
have := hlc.1

Goal state after:
α : 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
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ u)) t * (uniformOn s) u

Tactic:
rw [← Set.inter_comm]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (u ∩ t) = (uniformOn (s ∩ u)) t * (uniformOn s) u
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
    (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t))

Tactic:
rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_assoc]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| Measure.count s * (Measure.count s)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ +
    Measure.count t * (Measure.count t)⁻¹ * Measure.count (t ∩ u) * (Measure.count (s ∪ t))⁻¹
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:
by
  rw [← coeFn_le] at hf hg ⊢
  filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf
  rw [ha_inf]
  exact le_inf haf hag

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure

Tactic:
rw [OuterMeasure.le_pi]

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ ∀ (s : (i : ι) → Set (α i)),
    (univ.pi s).Nonempty → (pi' μ).toOuterMeasure (univ.pi s) ≤ ∏ i, (μ i).toOuterMeasure (s i)
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 : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ map (eval i) (Measure.pi μ) = μ i

Tactic:
Measure.pi_map_eval,

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ (∏ j ∈ Finset.univ.erase i, (μ j) univ) • μ i = μ i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case inr
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : μ s ≠ ∞
⊢ MemLp (fun x ↦ c) p (μ.restrict s)

Tactic:
have := Fact.mk hμ.lt_top

Goal state after:
case inr
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : μ s ≠ ∞
this : Fact (μ s < ∞)
⊢ MemLp (fun x ↦ c) p (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : MeasurableSpace α
f : α → ε
⊢ eLpNorm' f 0 0 = 1

Tactic:
simp [eLpNorm']

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (f - g) p μ = eLpNorm (g - f) p μ

Tactic:
by simp [← eLpNorm_neg (f := f - g)]

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

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)

pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ q ≠ ∞

Tactic:
· congr
    rw [← ENNReal.rpow_mul]
    suffices hp_cancel : q * (1 / q) = 1 by rw [hp_cancel, ENNReal.rpow_one]
    rw [one_div, mul_inv_cancel₀ hq_ne_zero]

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ q ≠ ∞
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

Tactic:
rw [div_lt_iff₀ h]

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ log z - log y < y⁻¹ * (z - y)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

Tactic:
· have h : 0 < y - x := by linarith
    rw [lt_div_iff₀ h]
    have hxy' : 0 < x / y := by positivity
    have hxy'' : x / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
    calc
      y⁻¹ * (y - x) = 1 - x / y := by field
      _ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy'']
      _ = -(log x - log y) := by rw [log_div hx.ne' hy.ne']
      _ = log y - log x := by ring

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

Goal state before:
pp: p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ p.HolderTriple q r

Tactic:
have hr := h.pos'

Goal state after:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
⊢ p.HolderTriple q r
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
convert! hf.secant_strict_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq]

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)

case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
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 ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by
  by_cases hp_zero : p = 0
  · simp only [hp_zero, eLpNorm_exponent_zero]
  by_cases hp_top : p = ∞
  · simp_rw [hp_top, eLpNorm_exponent_top]
    exact eLpNormEssSup_map_measure hg hf
  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top,
    lintegral_map' (hg.enorm.pow_const p.toReal) hf, Function.comp_apply]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
rcases eq_or_lt_of_le (hz i hi) with hz | hz
      · simp [A i hi hz.symm]
      · rw [exp_log hz]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1

Tactic:
by
  simp_rw [funMulInvSnorm_rpow hp0_lt]
  rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]
  rwa [inv_ne_top]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
have :
      ∏ i ∈ s with w i ≠ 0, z i ^ w i = ∑ i ∈ s with w i ≠ 0, w i * z i ↔
        ∀ j ∈ {x ∈ s | w x ≠ 0}, ∀ k ∈ {x ∈ s | w x ≠ 0}, z j = z k :=
    geom_mean_eq_arith_mean_weighted_iff_of_pos _ w z (by grind)
      (sum_filter_ne_zero _ |>.trans hw') (hz _ <| mem_of_mem_filter · ·)

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
this :
  ∏ i ∈ s with w i ≠ 0, z i ^ w i = ∑ i ∈ s with w i ≠ 0, w i * z i ↔
    ∀ j ∈ {x ∈ s | w x ≠ 0}, ∀ k ∈ {x ∈ s | w x ≠ 0}, z j = z k
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → ∀ k ∈ s, w k ≠ 0 → z j = z k
Module: Mathlib.Analysis.MeanInequalities

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

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

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

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

Tactic:
classical
  induction s using Finset.induction generalizing p with
  | empty =>
    simp at hp
  | insert i₀ s hi₀ ih =>
    rcases eq_or_ne (p i₀) 1 with h2i₀ | h2i₀
    · simp only [hi₀, not_false_eq_true, prod_insert]
      have h2p : ∀ i ∈ s, p i = 0 := by
        simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
          using hp
      calc ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ
          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ := by
            congr! 3 with x
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 := by simp [h2i₀]
        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
            congr 1
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
    · have hpi₀ : 0 ≤ 1 - p i₀ := by
        simp_rw [sub_nonneg, ← hp, single_le_sum h2p (mem_insert_self ..)]
      have h2pi₀ : 1 - p i₀ ≠ 0 := by
        rwa [sub_ne_zero, ne_comm]
      let q := fun i ↦ p i / (1 - p i₀)
      have hq : ∑ i ∈ s, q i = 1 := by
        rw [← Finset.sum_div, ← sum_insert_sub hi₀, hp, div_self h2pi₀]
      have h2q : ∀ i ∈ s, 0 ≤ q i :=
        fun i hi ↦ div_nonneg (h2p i <| mem_insert_of_mem hi) hpi₀
      calc ∫⁻ 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: ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
⊢ (∏ i ∈ s, z i ^ w i)⁻¹ ≤ ∏ i ∈ s, (z i)⁻¹ ^ w i

Tactic:
← Finset.prod_inv_distrib

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
⊢ ∏ x ∈ s, (z x ^ w x)⁻¹ ≤ ∏ i ∈ s, (z i)⁻¹ ^ w i
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h1
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
x : ι
a✝ : x ∈ s
⊢ (z x ^ w x)⁻¹ ≤ (z x)⁻¹ ^ w x

Tactic:
rw [Real.inv_rpow]; apply fun i hi ↦ le_of_lt (hz i hi); assumption

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 α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ↑c * (eLpNorm g ∞ μ * eLpNorm f p μ) = ↑c * (eLpNorm f p μ * eLpNorm g ∞ μ)

Tactic:
mul_comm (eLpNorm _ _ _)

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ↑c * (eLpNorm f p μ * eLpNorm g ∞ μ) = ↑c * (eLpNorm f p μ * eLpNorm g ∞ μ)
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:
by
      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: