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
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∀ (i : ι'), ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      ∀ (i : ι'),
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
rw [q.withSeminorms_iff_uniformSpace_eq_iInf.mp hq, uniformEquicontinuous_iInf_rng,
      equicontinuous_iInf_rng, equicontinuousAt_iInf_rng]
  refine forall_tfae [_, _, _, _, _] fun i ↦ ?_
  let _ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
  clear u hu hq
  -- Now we can prove the equivalence in this setting
  simp only [List.map]
  tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
  tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
  tfae_have 2 → 1 := fun H ↦ H 0
  tfae_have 3 → 5
  | H => 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
  tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩
  tfae_have 4 → 1 -- This would work over any `NormedField`
  | ⟨p, hp, hfp⟩ =>
    Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <|
      Eventually.of_forall fun x k ↦ by simpa using! hfp k x
  tfae_finish

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_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
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∀ (i : ι'), ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      ∀ (i : ι'),
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
by
  -- We start by reducing to the case where the target is a seminormed space
  rw [q.withSeminorms_iff_uniformSpace_eq_iInf.mp hq, uniformEquicontinuous_iInf_rng,
      equicontinuous_iInf_rng, equicontinuousAt_iInf_rng]
  refine forall_tfae [_, _, _, _, _] fun i ↦ ?_
  let _ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
  clear u hu hq
  -- Now we can prove the equivalence in this setting
  simp only [List.map]
  tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
  tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
  tfae_have 2 → 1 := fun H ↦ H 0
  tfae_have 3 → 5
  | H => 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
  tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩
  tfae_have 4 → 1 -- This would work over any `NormedField`
  | ⟨p, hp, hfp⟩ =>
    Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <|
      Eventually.of_forall fun x k ↦ by simpa using! hfp k x
  tfae_finish

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
hA : IsOpen[inst✝] A
⊢ IsOpen[instTopologicalSpace] (⇑(CompactCoherentification.mk X) '' A)

Tactic:
isOpen_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
hA : IsOpen[inst✝] A
⊢ ∀ (K : Set X),
    IsCompact K →
      IsOpen[instTopologicalSpaceSubtype]
        (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' ⇑(CompactCoherentification.mk X) '' A)
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'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ Inseparable g f'

Tactic:
← inseparable_coe,

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
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ Inseparable ⇑g ⇑f'
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ 0 < μ[t | s]

Tactic:
by
  rw [cond_apply hms]
  refine ENNReal.mul_pos ?_ hci
  exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

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

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

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

Tactic:
· rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, fun x _ ↦ by simpa [*] using hb _⟩

Goal state after:
case mpr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
⊢ (∃ x,
      ∃ (hx : 0 ≤ x),
        ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
          (∀ᶠ (a : ι) in f, ↑(u a) ≤ ↑(NNReal.mk x_1 hx_1)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk x_1 hx_1)) →
    ∃ b, ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
by_cases hu : u =ᶠ[f] 0

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f
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
k : R
a : α
⊢ ((algebraMap R C(α, A)) k) a = k • 1

Tactic:
rw [Algebra.algebraMap_eq_smul_one]
  rfl

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

Goal state before:
pp: case inr.inl
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : r < 0
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun a ↦ (u a).toReal) f ≤ r

pp: case inr.inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun a ↦ (u a).toReal) f ≤ r

Tactic:
· exact iff_of_false (hr.trans_le toReal_nonneg).not_ge
      (hr.trans_le <| le_limsup_of_frequently_le (by simpa)).not_ge

Goal state after:
case inr.inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun a ↦ (u a).toReal) f ≤ r
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑|f| =ᵐ[μ] fun x ↦ |↑f x|

Tactic:
simp_rw [abs]

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑(f ⊔ -f) =ᵐ[μ] fun x ↦ ↑f x ⊔ -↑f x
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 : ℝ
hc : c < 0
p : ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ = 0 ∧ ‖g x‖ = 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
norm_eq_zero,

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 : ℝ
hc : c < 0
p : ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, f x = 0 ∧ g x = 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ ↔ c = 0 ∨ μ Set.univ < ∞

Tactic:
by
  rw [memLp_const_iff_enorm enorm_ne_top hp_ne_zero hp_ne_top]; simp

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ eLpNorm' f q μ ≤ eLpNorm' g q μ

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm]
  gcongr ?_ ^ (1 / q)
  refine lintegral_mono_ae (h.mono fun x hx => ?_)
  gcongr

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

Goal state before:
pp: case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

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

Goal state before:
pp: case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

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

Goal state before:
pp: case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

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

Goal state before:
pp: case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ 1 + s < 1 + p * s

Tactic:
gcongr
      exact lt_mul_of_lt_one_left hs' hp2

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

Goal state before:
pp: case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

Tactic:
rw [add_sub_cancel_left, div_div, log_one, sub_zero]

Goal state after:
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:
by rw [log_neg_eq_log]

Goal state after:
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 * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x) =
    (a * a) • f x • g x + (b * a) • f y • g x + ((a * b) • f x • g y + (b * b) • f y • g y)

Tactic:
mul_comm b a,

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 + (a * b) • f y • g x) =
    (a * a) • f x • g x + (a * b) • f y • g x + ((a * b) • f x • g y + (b * b) • f y • g y)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.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
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, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ log (z j) = ∑ x ∈ s, log (z x) * w x

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

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

Tactic:
simp [h2i₀]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
by_cases h : 1 < p

Goal state after:
case pos
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
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 : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x ↦ 1
a : α
⊢ ‖f a‖ₑ ^ p = (‖f a‖ₑ * g a) ^ p

Tactic:
by simp [g]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
i : ι
hi : i ∈ s
⊢ (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)

Tactic:
← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹,

Goal state after:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
i : ι
hi : i ∈ s
⊢ z i ^ (w i * n⁻¹) = z i ^ (w i / n)
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 : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
⊢ eLpNorm f p μ < ∞

Tactic:
have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq
    rw [hp_top]
    rwa [hq_top] at hfq_lt_top

Goal state after:
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:
simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]
    exact mul_inv_cancel₀ hw'.ne'

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a = ∞ ∨ b = ∞
⊢ a * b = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q ↔ a = ∞ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ∞ ∨ a ^ p = b ^ q

pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a * b = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q ↔ a = ∞ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ∞ ∨ a ^ p = b ^ q

Tactic:
· rcases h with rfl | rfl <;> simp [hpq.pos, hpq.symm.pos, h0, div_eq_mul_inv]

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a * b = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q ↔ a = ∞ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ∞ ∨ a ^ p = b ^ q
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:
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

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) =
    ((∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)) ^ (1 / r)
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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
⊢ CompleteSpace ↥(Lp E p μ)

Tactic:
have hB_pos : ∀ n, 0 < B n := fun n => pow_pos (div_pos zero_lt_one zero_lt_two) n

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
⊢ CompleteSpace ↥(Lp E p μ)
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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := ⋯
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨M, hB⟩ : Summable B := summable_geometric_two

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)