mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
⊢ x ∈ (convexHull 𝕜) (s.pi t)

Tactic:
by
  classical
  cases nonempty_fintype ι
  wlog hs : s = Set.univ generalizing s t
  · rw [← pi_univ_ite]
    refine this (fun i _ ↦ ?_) rfl
    split_ifs with hi
    · exact h i hi
    · simp
  subst hs
  simp only [Set.mem_univ, mem_convexHull_iff_exists_fintype, true_implies] at h
  choose κ _ w f hw₀ hw₁ hft hf using h
  refine mem_convexHull_of_exists_fintype (fun k : Π i, κ i ↦ ∏ i, w i (k i)) (fun g i ↦ f _ (g i))
    (fun g ↦ prod_nonneg fun _ _ ↦ hw₀ _ _) ?_ (fun _ _ _ ↦ hft _ _) ?_
  · rw [← Fintype.prod_sum]
    exact prod_eq_one fun _ _ ↦ hw₁ _
  ext i
  calc
    _ = ∑ g : ∀ i, κ i, (∏ i, w i (g i)) • f i (g i) := by
      simp only [Finset.sum_apply, Pi.smul_apply]
    _ = ∑ j : κ i, ∑ g : {g : ∀ k, κ k // g i = j},
          (∏ k, w k (g.1 k)) • f i ((g : ∀ i, κ i) i) := by
      rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]
    _ = ∑ j : κ i, (∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)) • f i j := by
      simp_rw [sum_smul]
      congr! with j _ g _
      exact g.2
    _ = ∑ j : κ i, w i j • f i j := ?_
    _ = x i := hf _
  congr! with j _
  calc
    ∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)
      = ∑ g ∈ piFinset fun k ↦ if hk : k = i then hk ▸ {j} else univ, ∏ k, w k (g k) :=
      Finset.sum_bij' (fun g _ ↦ g) (fun g hg ↦ ⟨g, by simpa using mem_piFinset.1 hg i⟩)
        (by aesop) (by simp) (by simp) (by simp) (by simp)
    _ = w i j := by
      rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one] <;> simp +contextual [hw₁]

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

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ p.moduleFilterBasis.filter = ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
by
  refine le_antisymm (le_iInf fun i => ?_) ?_
  · rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
        (Metric.nhds_basis_ball.comap _)]
    intro ε hε
    refine ⟨(p i).ball 0 ε, ?_, ?_⟩
    · rw [← (Finset.sup_singleton : _ = p i)]
      exact p.basisSets_mem {i} hε
    · rw [id, (p i).ball_zero_eq_preimage_ball]
  · rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]
    rintro U (hU : U ∈ p.basisSets)
    rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩
    rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]
    exact fun i _ =>
      Filter.mem_iInf_of_mem i
        ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
          Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior

Tactic:
have hw1' : ∑ i, (u : Set (Fin (n + 1))).indicator w i = 1 := by
      simpa [Finset.sum_indicator_subset _ u.subset_univ] using hw1

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case pos.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 σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
x : E
hx : x ∈ ball 0 ε
⊢ ‖x‖ < ε

Tactic:
· rwa [ball_zero_eq] at hx

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

Goal state before:
pp: 𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module 𝕜₃ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →L[𝕜₃] F →SL[σ₂₃] G
c : 𝕜₃
x : E
y : F
⊢ (f (c • x)) y = c • (f x) y

Tactic:
by
  rw [f.map_smul, smul_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
⊢ ‖pi L‖ ≤ C

Tactic:
by
  refine opNorm_le_bound _ hC (fun x ↦ ?_)
  refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun i ↦ ?_)
  exact (L i).le_of_opNorm_le (hL i) _

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 σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ comap (⇑f) (⨅ i, comap (⇑(q i)) (𝓝 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)

Tactic:
Filter.comap_iInf

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 σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ ⨅ i, comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)
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
⊢ Continuous[instTopologicalSpace, inst✝] f ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K

Tactic:
continuous_coinduced_dom,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : 𝐤X → Y
⊢ Continuous[⨆ K,
          ⨆ (_ : IsCompact K),
            TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝¹] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ },
        inst✝]
      (f ∘ ⇑(CompactCoherentification.mk X)) ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K
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
⊢ (∀ (i : Set X),
      IsCompact i →
        Continuous[TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝¹] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ },
            inst✝]
          (f ∘ ⇑(CompactCoherentification.mk X))) ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K

Tactic:
continuous_coinduced_dom,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : 𝐤X → Y
⊢ (∀ (i : Set X),
      IsCompact i →
        Continuous[{ IsOpen := fun s ↦ ∃ t, IsOpen[inst✝¹] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯,
              isOpen_inter := ⋯, isOpen_sUnion := ⋯ },
            inst✝]
          ((f ∘ ⇑(CompactCoherentification.mk X)) ∘ Subtype.val)) ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K
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
⊢ ‖f.flip‖₊ = ‖f‖₊

Tactic:
simp [← NNReal.coe_inj]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
⊢ μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)

Tactic:
by
  rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

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

Tactic:
rintro ⟨b, hb₀, hb⟩
    refine ⟨b, fun x hx ↦ ?_⟩
    obtain hx₀ | hx₀ := le_total x 0
    · exact hx₀.trans hb₀
    · exact hb _ hx₀ hx

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✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂Measurable g hg f₁ f₂) =ᵐ[μ] fun a ↦ g (↑f₁ a) (↑f₂ a)

Tactic:
by
  rw [comp₂Measurable_eq_mk]
  apply coeFn_mk

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

pp: case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)

Tactic:
exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ ↑c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one, enorm,
    ← ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top,
    ← ENNReal.coe_mul]

Goal state after:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ↑(‖f a‖₊ ^ p) ∂μ ≤ ∫⁻ (a : α), ↑(c ^ p * ‖g a‖₊ ^ p) ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: 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
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
eLpNorm_mono this,

Goal state after:
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
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ eLpNorm' (fun x ↦ c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, lintegral_const,
    ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)]

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ∞
⊢ (p - 1) * p⁻¹ = q⁻¹

Tactic:
have := pos p q |>.ne'
  rw [ENNReal.sub_mul (by simp_all), ENNReal.mul_inv_cancel this (by lia)]
  simp [one_sub_inv p q]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  · exact (eLpNorm_smul_measure_of_ne_zero hc f p μ).le

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

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

Tactic:
by simpa only [coe_toNNReal_eq_toReal] using h.coe

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

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

Tactic:
by simpa only [coe_toNNReal_eq_toReal] using h.coe

Goal state after:
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✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
· simp [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp, hf.lintegral_map]

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

Goal state before:
pp: t : ℝ
ht : |t| ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
rw [abs_le] at ht
  calc
    _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
    _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
        convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) <| by ring
    _ = _ := by rw [cosh_eq, sinh_eq]; ring

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
this : ∑ i ∈ s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ x

Tactic:
← hx i his hi

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
this : ∑ i ∈ s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ z i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
have hp_pos : 0 < p := by positivity

Goal state after:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
have hp_pos : 0 < p := by positivity

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
rcases hq.eq_or_lt with rfl | hq

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 + 0 = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mpr
ι : 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
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
· rw [← arith_mean_weighted_of_constant s w _ (z j) hw' fun i _ => congrFun rfl]
        apply sum_congr rfl
        intro x hx
        simp only [log_injOn_pos (hz' j hj) (hz' x hx), h j hj, h x hx]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
have hp_pos : 0 < p := by positivity

Goal state after:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
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 : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f q μ ≤ eLpNorm' f q μ * μ Set.univ ^ 0

Tactic:
ENNReal.rpow_zero,

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f q μ ≤ eLpNorm' f q μ * 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : 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, w i / ∑ i ∈ s, w i = 1

Tactic:
div_eq_mul_inv (w _) (∑ i ∈ s, w i),

Goal state after:
case refine_2
ι : 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
⊢ ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ = 1
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
      by_cases h_zero : (f + g) a = 0
      · rw [h_zero, ENNReal.zero_rpow_of_pos hpq.pos]
        exact zero_le
      by_cases h_top : (f + g) a = ⊤
      · rw [h_top, ENNReal.top_rpow_of_pos hpq.sub_one_pos, ENNReal.top_mul_top]
        exact le_top
      refine le_of_eq ?_
      nth_rw 2 [← ENNReal.rpow_one ((f + g) a)]
      rw [← ENNReal.rpow_add _ _ h_zero h_top, add_sub_cancel]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ (∑ i ∈ s, (f i * g i) ^ r) ^ (1 / r) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
by
  convert
    rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos' : 0 < 1 / r) |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq s f g hpqr
  have hr := hpqr.pos'.ne'
  simp only [← rpow_mul, mul_rpow]
  field_simp

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
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : f ∈ {f | eLpNorm (↑f) p μ < ∞}
⊢ eLpNorm (-↑f) p μ < ∞

Tactic:
eLpNorm_neg

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
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : f ∈ {f | eLpNorm (↑f) p μ < ∞}
⊢ eLpNorm (↑f) p μ < ∞
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 : ↥(Lp E p μ)
hf : MemLp (↑↑f) p μ
⊢ MemLp.toLp (↑↑f) hf = f

Tactic:
by
  simp [MemLp.toLp]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
← Real.rpow_mul hf'

Goal state after:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
hf' : 0 ≤ ∑' (i : ι), f i ^ p
hg' : 0 ≤ ∑' (i : ι), g i ^ q
hr : 0 < r
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    (∑' (i : ι), f i ^ p) ^ (r / p * (1 / r)) * (∑' (i : ι), g i ^ q) ^ (r / q * (1 / r))
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 : ↥(Lp E p μ)
⊢ (eLpNorm (-↑↑f) p μ).toNNReal = (eLpNorm (↑↑f) p μ).toNNReal

Tactic:
eLpNorm_neg

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑f) p μ).toNNReal = (eLpNorm (↑↑f) p μ).toNNReal