mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

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

pp: 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

Tactic:
· calc
      Measure.pi μ (Set.pi univ fun i => (hμ i).set (e n i)) ≤
          Measure.pi μ (Set.pi univ fun i => toMeasurable (μ i) ((hμ i).set (e n i))) :=
        measure_mono (pi_mono fun i _ => subset_toMeasurable _ _)
      _ = ∏ i, μ i (toMeasurable (μ i) ((hμ i).set (e n i))) :=
        (pi_pi_aux μ _ fun i => measurableSet_toMeasurable _ _)
      _ = ∏ i, μ i ((hμ i).set (e n i)) := by simp only [measure_toMeasurable]
      _ < ∞ := ENNReal.prod_lt_top fun i _ => (hμ i).finite _

Goal state after:
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.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
obtain rfl | hp := eq_or_ne p 0
  · simp
  obtain rfl | h'p := eq_or_ne p ∞
  · simp only [eLpNorm_exponent_top, ENNReal.toReal_top, _root_.div_zero, ENNReal.rpow_zero,
      mul_one]
    exact eLpNormEssSup_indicator_const_le _ _
  let t := toMeasurable μ s
  calc
    eLpNorm (s.indicator fun _ => c) p μ ≤ eLpNorm (t.indicator fun _ ↦ c) p μ :=
      eLpNorm_mono_enorm (enorm_indicator_le_of_subset (subset_toMeasurable _ _) _)
    _ = ‖c‖ₑ * μ t ^ (1 / p.toReal) :=
      eLpNorm_indicator_const (measurableSet_toMeasurable ..) hp h'p
    _ = ‖c‖ₑ * μ s ^ (1 / p.toReal) := by rw [measure_toMeasurable]

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

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

Goal state before:
pp: case neg.inr.right
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ x ∈ sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
setLIntegral_congr_fun hs.compl h

Goal state after:
case neg.inr.right
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ x ∈ sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖g x‖ₑ ^ p.toReal ∂μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
⊢ eLpNorm 0 p μ = 0

Tactic:
by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simp only [h_top, eLpNorm_exponent_top, eLpNormEssSup_zero]
  rw [← Ne] at h0
  simp [eLpNorm_eq_eLpNorm' h0 h_top, ENNReal.toReal_pos h0 h_top]

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 ≠ ∞

Tactic:
finiteness [show ‖c‖ₑ ≠ 0 by simp [hc_ne_zero]]

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

Goal state before:
pp: case pos
α : 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 : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

pp: case neg
α : 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 : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : ¬p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
· simpa [hp'] using eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h

Goal state after:
case neg
α : 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 : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : ¬p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (Measure.map (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = (μ 0) s * (μ 1) t

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod,
    Measure.pi_pi, Fin.prod_univ_two]

Goal state after:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * (μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) = (μ 0) s * (μ 1) t
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
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y = log (z / y)

Tactic:
rw [← log_div hz.ne' hy.ne']

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
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < y⁻¹

Tactic:
have h : 0 < z - y := by linarith
    rw [div_lt_iff₀ h]
    have hyz' : 0 < z / y := by positivity
    have hyz'' : z / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
    calc
      log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
      _ < z / y - 1 := log_lt_sub_one_of_pos hyz' hyz''
      _ = y⁻¹ * (z - y) := by field

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ eLpNorm' f q ν ≤ eLpNorm' f q μ

Tactic:
eLpNorm'

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν) ^ (1 / q) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ q = p / (p - 1)

Tactic:
convert! inv_inv q ▸ congr($(h.symm.inv_sub_inv_eq_inv.symm)⁻¹) using 1
  field [h.ne_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rw [monovaryOn_iff_smul_rearrangement]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
h_inv_rpow : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [h_inv_rpow]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Tactic:
exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case x
ι : 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
⊢ ℝ

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case hx
ι : 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
⊢ ∀ i ∈ s, w i ≠ 0 → z i = x

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case hw
ι : 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
⊢ ∀ i ∈ s, 0 ≤ w i

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case hz
ι : 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
⊢ ∀ i ∈ s, 0 ≤ z i

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
NNReal.le_rpow_inv_iff hp_pos,

Goal state after:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / q)) ^ p ≤ a ^ p + b ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
rw [mul_comm, mul_comm ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p))]

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)
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
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}, z j = ∑ i ∈ s with w i ≠ 0, w i * z i
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i

Tactic:
grind [prod_filter_of_ne, sum_filter_of_ne, rpow_zero]

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
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

Tactic:
grind [prod_filter_of_ne, sum_filter_of_ne, rpow_zero]

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
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}, z j ≠ ∑ i ∈ s with w i ≠ 0, w i * z i
⊢ ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, w j ≠ 0 ∧ z j ≠ ∑ i ∈ s, w i * z i

Tactic:
grind [prod_filter_of_ne, sum_filter_of_ne, rpow_zero]

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

Tactic:
rw [← arith_mean_weighted_of_constant s w (fun _ => z j) (z j) hw' fun _ _ => congrFun rfl]

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 : ι
hjs : j ∈ s
⊢ ∑ i ∈ s, w i * z j = ∑ i ∈ s, w i * z i
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
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, ∃ k ∈ s, w j ≠ 0 ∧ w k ≠ 0 ∧ z j ≠ z k

Tactic:
grind [prod_filter_of_ne, sum_filter_of_ne, rpow_zero]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ ↑(⟨w₁, hw₁⟩ + ⟨w₂, hw₂⟩) = ↑1

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hw₃ : 0 ≤ w₃
hw₄ : 0 ≤ w₄
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hp₃ : 0 ≤ p₃
hp₄ : 0 ≤ p₄
hw : w₁ + w₂ + w₃ + w₄ = 1
⊢ ↑(⟨w₁, hw₁⟩ + ⟨w₂, hw₂⟩ + ⟨w₃, hw₃⟩ + ⟨w₄, hw₄⟩) = ↑1

Tactic:
assumption

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

Goal state before:
pp: case refine_2
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst✝ : ContinuousAdd ε'
ι : Type u_5
s✝ : Finset ι
f : ι → α → ε'
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a ↦ ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp (fun a ↦ f i a + ∑ i ∈ s, f i a) p μ

Tactic:
exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h1.hx
ι : 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
⊢ x ∈ s

Tactic:
assumption

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

Goal state before:
pp: case h₂.inr.inl
α : 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
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ essSup (fun x ↦ ‖f x‖ₑ * ‖g x‖ₑ) μ ≤ essSup (fun x ↦ ‖f x‖ₑ) μ * essSup (fun x ↦ ‖g x‖ₑ) μ

Tactic:
exact ENNReal.essSup_mul_le (‖f ·‖ₑ) (‖g ·‖ₑ)

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
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
⊢ ∀ (i i_1 i_2 : ℕ), i ≤ i_1 → i ≤ i_2 → ∀ᵐ (a : α) ∂μ, ‖(f i_1 - f i_2) a‖ₑ < B i

Tactic:
exact fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Span

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
x : E
hx : ‖x‖ = 1
⊢ ∀ (x_1 : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) x_1‖ = ‖x_1‖

Tactic:
by
    intro
    rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : dist t 0 < 1
⊢ ‖t‖ < 1

Tactic:
← dist_zero_right

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : dist t 0 < 1
⊢ dist t 0 < 1
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ ‖f x‖ ≤ c * (‖k‖ / r) * ‖x‖

Tactic:
calc
    ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
    _ ≤ c * (‖x‖ * ‖k‖ / r) := le_mul_of_one_le_right ?_ ?_
    _ = _ := by ring

Goal state after:
case h.calc_1
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c

case h.calc_2
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖

Tactic:
rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
left✝ : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x✝ : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ C * ‖‖(x, y).1‖ * ‖(x, y).2‖‖

Tactic:
by simpa [mul_assoc] using hC x y

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

Goal state before:
pp: case inl
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ∞
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

Tactic:
simp only [Measure.real, h, ENNReal.toReal_top]
    exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)

Tactic:
simp only [measureReal_def]
  rw [measure_union_congr_of_subset hs _ ht]
  · exact (ENNReal.toReal_le_toReal h₂ (measure_ne_top_of_subset ht h₂)).1 htμ
  · exact (ENNReal.toReal_le_toReal h₁ (measure_ne_top_of_subset hs h₁)).1 hsμ

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
assumption

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

Tactic:
assumption

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

Goal state before:
pp: case hμ
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0

Tactic:
assumption

Goal state after: