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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
⊢ (convexHull R) ↑s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
classical
  refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    rw [Finset.mem_coe] at hx
    refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
    · intros
      split_ifs
      exacts [zero_le_one, le_refl 0]
    · rw [Finset.sum_ite_eq, if_pos hx]
  · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]
  · rintro _ ⟨w, hw₀, hw₁, rfl⟩
    exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ diam ((convexHull ℝ) s) = diam s

Tactic:
simp only [diam, convexHull_ediam]

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

Goal state before:
pp: case pos
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : 0 < (s.sup p) v
⊢ {x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0

Tactic:
simp_rw [(lt_div_iff₀ h).symm]
    rw [← _root_.ball_zero_eq]
    exact Metric.ball_mem_nhds 0 (div_pos hr h)

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h : p ∈ s.closedInterior
⊢ ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p

Tactic:
obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
      Set.mem_of_mem_of_subset h s.closedInterior_subset_affineSpan

Goal state after:
case mpr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
w : Fin (n + 1) → 𝕜
hw1 : ∑ i, w i = 1
h : (Finset.affineCombination 𝕜 Finset.univ s.points) w ∈ s.closedInterior
⊢ ∃ s_1 w_1,
    (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
      s_1.sum w_1 = 1 ∧
        (Finset.affineCombination 𝕜 s_1 s.points) w_1 = (Finset.affineCombination 𝕜 Finset.univ s.points) w
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✝⁷ : SeminormedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : SeminormedRing 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι' : Type u_11
inst✝ : Nonempty ι'
p : ι → Seminorm 𝕜 E
q : Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ IsBounded p (fun x ↦ q) f ↔ ∃ s C, q.comp f ≤ C • s.sup p

Tactic:
by
  simp only [IsBounded, forall_const]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝ : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), (p i) x = 0
⊢ x ⤳ 0

Tactic:
hp.hasBasis_zero_ball.specializes_iff

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝ : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), (p i) x = 0
⊢ ∀ (i : Finset ι × ℝ), 0 < i.2 → x ∈ (i.1.sup p).ball 0 i.2
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : 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) × (E →SL[σ₁₂] F)
⊢ ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖

Tactic:
neg_add,

Goal state after:
𝕜 : 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) × (E →SL[σ₁₂] F)
⊢ ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
have : Continuous q := by
    apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)
    rw [← ball_eq_metric]
    exact hε

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := { toModule := inst✝, norm_smul_le := ⋯ }
this : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: case hbc
𝕜 : 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ₗ‖ ≤ 1

Tactic:
apply norm_compL_le

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ ‖(smulRight c f) x‖ ≤ ‖c‖ * ‖f‖ * ‖x‖

Tactic:
calc
      ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
      _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
      _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring

Goal state after:
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:
rw [cond_apply hms]
  refine ENNReal.mul_pos ?_ hci
  exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] * μ s + μ[t | sᶜ] * μ sᶜ = μ t

Tactic:
cond_mul_eq_inter hms,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ (s ∩ t) + μ[t | sᶜ] * μ sᶜ = μ t
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ ↑C
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
⊢ ENNReal.ofReal (limsup (fun a ↦ (u a).toReal) f) = limsup u f

Tactic:
have h₂ : IsBoundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) := by
    refine isBoundedUnder_of_eventually_le (a := C) ?_
    filter_upwards [hf] with a ha
    exact ENNReal.toReal_le_coe_of_le_coe ha

Goal state after:
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ ↑C
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
⊢ ENNReal.ofReal (limsup (fun a ↦ (u a).toReal) f) = limsup u f
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
hs : MeasurableSet s
⊢ MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

Tactic:
by
  simp [MemLp, aestronglyMeasurable_indicator_iff hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulRightInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (map (fun x ↦ x * v) (Measure.pi μ)) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
map_apply (measurable_mul_const _) (MeasurableSet.univ_pi hs),

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulRightInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) ((fun x ↦ x * v) ⁻¹' univ.pi s) = ∏ i, (μ i) (s i)
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.pi μ) (⇑(MeasurableEquiv.piFinTwo α) ⁻¹' s ×ˢ t) = (μ 0) s * (μ 1) t

Tactic:
MeasurableEquiv.piFinTwo_apply,

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
⊢ (Measure.pi μ) ((fun f ↦ (f 0, f 1)) ⁻¹' s ×ˢ t) = (μ 0) s * (μ 1) t
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝¹ : ¬p = 0
h✝ : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ

Tactic:
· exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h

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

Goal state before:
pp: case inr.inr.inl
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) < log (1 + s) * p

Tactic:
← div_lt_iff₀ hp',

Goal state after:
case inr.inr.inl
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 < log (1 + s)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr.inr
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) < log (1 + s) * p

Tactic:
← div_lt_iff₀ hp',

Goal state after:
case inr.inr.inr
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 < log (1 + s)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < p / r

Tactic:
have := h.left_pos

Goal state after:
p q r : ℝ
h : p.HolderTriple q r
this : 0 < p
⊢ 0 < p / r
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < p / r

Tactic:
have := h.left_pos

Goal state after:
p q r : ℝ≥0
h : p.HolderTriple q r
this : 0 < p
⊢ 0 < p / r
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
⊢ ∑ i ∈ s, w i ≠ 0

Tactic:
rw [hw']

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
⊢ 1 ≠ 0
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)⁻¹
⊢ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i

Tactic:
have p_pos₂ : 0 < (∏ i ∈ s, (z i) ^ w i)⁻¹ :=
    inv_pos.2 (prod_pos fun i hi => rpow_pos_of_pos ((hz i hi)) _)

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)⁻¹
⊢ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr.inl
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : 0 < ∞
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * μ Set.univ ^ (1 / p.toReal - 1 / ∞.toReal)

Tactic:
simp only [_root_.div_zero, one_div, ENNReal.toReal_top, sub_zero]
    obtain rfl | hp_top := eq_or_ne p ∞
    · simp
    rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
    have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
    refine (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos).trans (le_of_eq ?_)
    congr
    exact one_div _

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

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

Tactic:
suffices
    ∫⁻ t, ∏ j ∈ insertNone s, Option.elim j (g t) (fun j ↦ f j t) ^ Option.elim j q p ∂μ
    ≤ ∏ j ∈ insertNone s, (∫⁻ t, Option.elim j (g t) (fun j ↦ f j t) ∂μ) ^ Option.elim j q p by
    simpa using this
  refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
  · rintro (_ | i) hi
    · exact hg
    · refine hf i ?_
      simpa using hi
  · simp_rw [sum_insertNone, Option.elim]
    exact hpq
  · rintro (_ | i) hi
    · exact hq
    · refine hp i ?_
      simpa using hi

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

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

Tactic:
by
  rw [eLpNorm'_lim_eq_lintegral_liminf h_lim]
  rw [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]
  refine (lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_
  have h_pow_liminf :
    atTop.liminf (fun n ↦ eLpNorm' (f n) p μ) ^ p
      = atTop.liminf fun n ↦ eLpNorm' (f n) p μ ^ p := by
    have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos
    have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
    refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
    all_goals isBoundedDefault
  rw [h_pow_liminf]
  simp_rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div,
    inv_mul_cancel₀ hp_pos.ne.symm, ENNReal.rpow_one]

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

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

Tactic:
neg_add,

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

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

Tactic:
neg_add,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (- -↑↑f + -↑↑g) p μ = eLpNorm (↑↑f - ↑↑g) p μ
Module: Mathlib.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_congr_ae (coeFn_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
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : |↑↑f x| ≤ |↑↑g x|
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖

Tactic:
exact HasSolidNorm.solid hx

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}

Tactic:
rw [mem_ball_iff_norm] at hy

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I

Tactic:
by
    simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI

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

Goal state before:
pp: case hf.refine_2
𝕜 : 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
x : E × F
⊢ Prod.snd =O[𝓝 x] fun _x ↦ 1

Tactic:
· exact (continuous_snd.tendsto _).isBigO_one ℝ

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: case refine_1
𝕜 : Type u_1
ι✝ : Type u_2
E : ι✝ → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)
inst✝⁵ : (i : ι✝) → AddCommGroup (E i)
inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ {s | IsVonNBounded 𝕜 s}.Nonempty

Tactic:
exact ⟨∅, isVonNBounded_empty _ _⟩

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hc : IsClosedMap f
h_cont : Continuous[inst✝¹, inst✝] f
⊢ IsStrictMap f

Tactic:
rw [isStrictMap_iff_isQuotientMap_rangeFactorization]
  exact (hc.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
    h_cont.rangeFactorization Set.rangeFactorization_surjective

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsTopCompl ⊥ ⊤

Tactic:
have : IsIdempotentElem (0 : M →L[R] M) := .zero
  simpa using this.isTopCompl

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.real s = 0 ↔ μ s = 0

Tactic:
rw [Measure.real, ENNReal.toReal_eq_zero_iff]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ s = 0 ∨ μ s = ∞ ↔ μ s = 0
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hst : s ⊆ t
h_nulldiff : μ (t \ s) = 0
h : μ (t \ s) ≠ ∞
⊢ μ.real s = μ.real t

Tactic:
simp [measureReal_def, measure_eq_measure_of_null_sdiff hst h_nulldiff]

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₂ ≠ ∞
⊢ μ s₂ ≤ μ s₁

Tactic:
· exact (ENNReal.toReal_le_toReal h₁ (measure_ne_top_of_subset hs h₁)).1 hsμ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i ↦ (s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (⋃ i, s i).mulIndicator f a

Tactic:
classical exact hs.piecewise_eventually_eq_iUnion f 1 a

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
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by_cases hp_top : p = ∞
  · rw [hp_top, ENNReal.toReal_top, _root_.div_zero, Real.rpow_zero, mul_one]
    exact norm_indicatorConstLp_top hμs_pos
  · exact norm_indicatorConstLp hp_pos hp_top

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
⊢ Metric.closedBall 0 ε ∈ 𝓝 0

Tactic:
refine mem_of_superset this fun ξ hξ => ?_

Goal state after:
case refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ ξ ∈ Metric.closedBall 0 ε