mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
H : f.toGerm = g.toGerm
⊢ ↑↑f = ↑↑g

Tactic:
by rwa [← toGerm_eq, ← toGerm_eq]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
⊢ (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

Tactic:
rcases g; rfl

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ piPremeasure m (univ.pi fun i ↦ eval i '' s) = piPremeasure m s

Tactic:
by
  simp only [eval, piPremeasure_pi']; rfl

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : univ.pi s = ∅
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i, (m i) (s i)

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x) = ∏ j ∈ Finset.univ.erase i, (μ j) univ

pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (μ i) (update (fun j ↦ univ) i s i) = (μ i) s

Tactic:
swap

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (μ i) (update (fun j ↦ univ) i s i) = (μ i) s

case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x) = ∏ j ∈ Finset.univ.erase i, (μ j) univ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) ((fun x i ↦ f i (x i)) ⁻¹' univ.pi s) = ∏ i, (map (f i) (μ i)) (s i)

pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ AEMeasurable (fun x i ↦ f i (x i)) (Measure.pi μ)

Tactic:
swap

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ AEMeasurable (fun x i ↦ f i (x i)) (Measure.pi μ)

ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) ((fun x i ↦ f i (x i)) ⁻¹' univ.pi s) = ∏ i, (map (f i) (μ i)) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ε = ∞
⊢ μ {x | ε ≤ ↑‖f x‖₊} < ∞

Tactic:
simp [h]

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 : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
⊢ IsFiniteMeasureOnCompacts (Measure.pi μ)

Tactic:
by
  constructor
  intro K hK
  suffices Measure.pi μ (Set.univ.pi fun j => Function.eval j '' K) < ⊤ by
    exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this
  rw [Measure.pi_pi]
  refine WithTop.prod_lt_top ?_
  exact fun i _ => IsCompact.measure_lt_top (IsCompact.image hK (continuous_apply i))

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f p 0 = 0

pp: case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm f p 0 = 0

Tactic:
· simp [h_top]

Goal state after:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm f p 0 = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ↑C * μ s ^ p.toReal⁻¹ ≤ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹

Tactic:
ENNReal.le_rpow_inv_iff (ENNReal.toReal_pos hp hp'),

Goal state after:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ (↑C * μ s ^ p.toReal⁻¹) ^ p.toReal ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∈ s
⊢ s.indicator (fun x ↦ ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
simp only [Set.indicator_of_mem, hxs, true_implies] at hx ⊢
    gcongr
    rwa [coe_le_enorm]

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
hyz' : 0 < z / y
h : z = y
⊢ z - y ≤ 0

Tactic:
simp [h]

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
hxy' : 0 < x / y
h : x = y
⊢ y - x ≤ 0

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' (fun x ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ p * ENNReal.ofReal q ≠ 0

Tactic:
swap

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ p * ENNReal.ofReal q ≠ 0

case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' (fun x ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q
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)

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
⊢ 1 + p * s < 1 + s

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

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
⊢ 1 + p * s < 1 + s
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)

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' : 0 < s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

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
⊢ 1 + s < 1 + p * s

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

Goal state after:
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' : 0 < s
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

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
⊢ 1 + s < 1 + p * s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ essSup (fun x ↦ ‖f x‖ₑ) ν ≤ essSup (fun x ↦ ‖f x‖ₑ) μ

Tactic:
exact essSup_mono_measure hμν

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)

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' : s < 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

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:
· rw [add_sub_cancel_left, div_div, log_one, sub_zero]

Goal state after:
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' : s < 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

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
Module: Mathlib.Data.Real.ConjExponents

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

Tactic:
by have := h.right_pos; have := h.pos'; positivity

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

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

Tactic:
by have := h.right_pos; have := h.pos'; positivity

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

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑(p - 1))⁻¹

Tactic:
← coe_inv (tsub_pos_of_lt hp).ne'

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + ↑(p - 1)⁻¹
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)

pp: case inr.inr
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
⊢ 1 + p * s < 1 + s

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

Goal state after:
case inr.inr
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
⊢ 1 + p * s < 1 + s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toReal
⊢ p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q

Tactic:
refine ⟨of_toReal, fun h ↦ ?_⟩
  have hq : 0 < q.toReal := by
    rw [toReal_pos_iff]
    refine ⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩
    contrapose! hp
    exact toReal_mono one_ne_top hp
  simpa using HolderTriple.toReal 1 (zero_lt_one.trans hp) hq

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ f y < f z

Tactic:
refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ openSegment 𝕜 x z
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 : ι → β
⊢ (∀ ⦃i : ι⦄, i ∈ Set.univ → ∀ ⦃j : ι⦄, j ∈ Set.univ → 0 ≤ (f j - f i) • (g j - g i)) ↔
    ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)

Tactic:
simp only [Set.mem_univ, forall_true_left]

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 : ι → β
⊢ (∀ ⦃i : ι⦄, i ∈ Set.univ → ∀ ⦃j : ι⦄, j ∈ Set.univ → f i • g j + f j • g i ≤ f i • g i + f j • g j) ↔
    ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j

Tactic:
simp only [Set.mem_univ, forall_true_left]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : 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
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
have := strictConvexOn_exp.map_sum_eq_iff hw hw' fun i _ => Set.mem_univ <| log (z i)

Goal state after:
case neg
ι : 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 : rexp (∑ i ∈ s, w i • log (z i)) = ∑ i ∈ s, w i • rexp (log (z i)) ↔ ∀ j ∈ s, log (z j) = ∑ i ∈ s, w i • log (z i)
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
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 : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hfq : MemLp f q μ
hpq : p ≤ q
⊢ MemLp f p μ

Tactic:
obtain ⟨hfq_m, hfq_lt_top⟩ := hfq

Goal state after:
α : 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 μ < ∞
⊢ MemLp f p μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑a.toNNReal ^ p / ENNReal.ofReal p + ↑b.toNNReal ^ q / ENNReal.ofReal q

Tactic:
← coe_rpow_of_nonneg _ hpq.nonneg,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑b.toNNReal ^ q / ENNReal.ofReal q
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
← coe_rpow_of_nonneg _ hpq.nonneg,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑b.toNNReal ^ q / ENNReal.ofReal q ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑b.toNNReal ^ q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 1 / p.toNNReal + 1 / q.toNNReal = 1

Tactic:
simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ c • ↑f ∈ Lp E p μ

Tactic:
rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_congr_ae (AEEqFun.coeFn_smul _ _)]
  exact eLpNorm_const_smul_le.trans_lt <| (by finiteness)

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
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : IsBoundedSMul 𝕜' E
c : 𝕜
f : α →ₘ[μ] E
hf : f ∈ (Lp E p μ).carrier
⊢ c • f ∈ (Lp E p μ).carrier

Tactic:
simpa using const_smul_mem_Lp c ⟨f, hf⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (n✝ + 1) ≤ k
⊢ μ {x | 2⁻¹ ^ (n✝ + 1) ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ (n✝ + 1)

Tactic:
· exact Classical.choose_spec
      (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)

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
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
γ : Type u_8
mγ : MeasurableSpace γ
μc : Measure γ
f : β → γ
hf : MeasurePreserving f μb μc
f' : α → β
hf' : MeasurePreserving f' μ μb
⊢ compMeasurePreserving (f ∘ f') ⋯ = (compMeasurePreserving f' hf').comp (compMeasurePreserving f hf)

Tactic:
by
  ext g
  simp [AEEqFun.compMeasurePreserving_comp _ hf hf']

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : PseudoEMetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
by
  obtain ⟨ms, hms1, hms2⟩ := hfg.exists_seq_tendstoInMeasure_atTop
  obtain ⟨ns, hns1, hns2⟩ := hms2.exists_seq_tendsto_ae
  exact ⟨ms ∘ ns, hms1.comp hns1.tendsto_atTop, hns2⟩

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
inst✝¹ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
inst✝ : Fact (1 ≤ p)
f : ↥(Lp E p ν)
⊢ ‖(LpToLpOfMeasureLeSMulₗ hc h) f‖ₑ ≤ c ^ (1 / p).toReal * ‖f‖ₑ

Tactic:
simp only [Lp.enorm_def]
  rw [eLpNorm_congr_ae (coeFn_LpToLpOfMeasureLeSMulₗ hc h f)]
  exact eLpNorm_le_of_measure_le_smul h

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ∞
⊢ TendstoInMeasure μ f l g

pp: case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ∞
⊢ TendstoInMeasure μ f l g

Tactic:
· subst hp_ne_top
    exact tendstoInMeasure_of_tendsto_eLpNorm_top hfg

Goal state after:
case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ∞
⊢ TendstoInMeasure μ f l g
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
h : ‖t‖ < 1
⊢ (1 - t)⁻¹ʳ = (↑(Units.oneSub t h))⁻¹ʳ

Tactic:
Units.val_oneSub

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
h : ‖t‖ < 1
⊢ (1 - t)⁻¹ʳ = (1 - t)⁻¹ʳ