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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) ≤ r ↔ p (a • (x✝ - a⁻¹ • y)) ≤ r

Tactic:
smul_sub,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) ≤ r ↔ p (a • x✝ - a • a⁻¹ • y) ≤ r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst✝¹, _] ⇑q
hpq : p ≤ q
⊢ Continuous[inst✝¹, _] ⇑p

Tactic:
refine Seminorm.continuous_of_forall (fun r hr ↦ Filter.mem_of_superset
    (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))
  rw [ball_zero_eq]
  exact isOpen_lt hq continuous_const

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s, (r • (w₁ x - w₂ x) - w x) = 0

Tactic:
smul_sub,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s, (r • w₁ x - r • w₂ x - w x) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ∀ x ∈ {x | x ≠ 2}, x ∈ ![p₁, p₂, p₃] ⁻¹' ↑s

Tactic:
Set.mem_preimage

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ∀ x ∈ {x | x ≠ 2}, ![p₁, p₂, p₃] x ∈ ↑s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ ∑ i ∈ s, Pi.single i₁ 1 i = 1

Tactic:
Finset.sum_pi_single',

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ (if i₁ ∈ s then 1 else 0) = 1
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_1
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
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : E
hi : i ∈ s
⊢ 0 ≤ a * wx i + b * wy i

Tactic:
apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]

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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap,

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (𝓝 ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0)) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h✝ : r > 0 ∧ ∀ x ∈ s, (p i) x < r
⊢ ∃ x, ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i) x_1 ≤ x

Tactic:
use r

Goal state after:
case h
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h✝ : r > 0 ∧ ∀ x ∈ s, (p i) x < r
⊢ ∀ ⦃x : E⦄, x ∈ s → (p i) x ≤ r
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : ¬r < 0
⊢ ∃ x, ‖x‖ < 1 ∧ r < ‖f x‖

Tactic:
lift r to ℝ≥0 using not_lt.1 hr₀

Goal state after:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : ↑r < ‖f‖
hr₀ : ¬↑r < 0
⊢ ∃ x, ‖x‖ < 1 ∧ ↑r < ‖f x‖
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ IsClosed[instTopologicalSpace] A ↔
    ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)

Tactic:
simp_rw [isClosed_coinduced, isClosed_iSup_iff, ← isClosed_coinduced]

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

Goal state before:
pp: 𝕜 : 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ₗ
⊢ 1 * ‖L‖ = ‖L‖

Tactic:
one_mul

Goal state after:
𝕜 : 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ₗ
⊢ ‖L‖ = ‖L‖
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ f.limsInf = 0

Tactic:
limsInf

Goal state after:
f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ sSup {a | ∀ᶠ (n : ℝ) in f, a ≤ n} = 0
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
hcs : μ s ≠ 0
⊢ 1 * μ (s ∩ t) = μ (s ∩ t)

Tactic:
one_mul

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
hcs : μ s ≠ 0
⊢ μ (s ∩ t) = μ (s ∩ t)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ ↑(f.pair g) =ᵐ[μ] fun x ↦ (↑f x, ↑g x)

Tactic:
rw [pair_eq_mk]
  apply coeFn_mk

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ 1 * Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0

Tactic:
one_mul

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0
Module: Mathlib.MeasureTheory.Constructions.Pi

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

Tactic:
simp [h, piPremeasure]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
x : α
⊢ x ∈ t → x ∈ Function.support f

Tactic:
(hx : d < f x)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
x : α
hx : d < f x
⊢ x ∈ Function.support f
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
⊢ map (eval i) (Measure.pi μ) = (∏ j ∈ Finset.univ.erase i, (μ j) univ) • μ i

Tactic:
ext s hs
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]

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

Goal state before:
pp: case neg
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ ε ^ p.toReal * μ {x | ε ≤ ‖f x‖ₑ} ≤ 1 * eLpNorm f p μ ^ p.toReal

Tactic:
one_mul

Goal state after:
case neg
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ ε ^ p.toReal * μ {x | ε ≤ ‖f x‖ₑ} ≤ eLpNorm f p μ ^ p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
⊢ eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)

Tactic:
simp_rw [← eLpNorm_exponent_top, eLpNorm_indicator_eq_eLpNorm_restrict hs]

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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this✝ : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
simpa only [hg', mul_zero, nonpos_iff_eq_zero] using eLpNorm'_eq_zero_of_ae_eq_zero hp this

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

Goal state before:
pp: case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
suffices hq_cancel : q * (1 / q) = 1 by rw [hq_cancel, ENNReal.rpow_one]

Goal state after:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * (1 / q) = 1
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
i.prod_univ_succAbove _,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) =
    (μ i) (s i) * ∏ i_1, (μ (i.succAbove i_1)) (s (i.succAbove i_1))
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst✝² : NormedAddCommGroup R
inst✝¹ : StarAddMonoid R
inst✝ : NormedStarGroup R
p : ℝ≥0∞
f : α → R
hf : MemLp f p μ
⊢ eLpNorm (star f) p μ < ∞

Tactic:
by simpa using hf.2

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖

Tactic:
one_mul

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.re (f x)‖ ≤ ‖f x‖
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖

Tactic:
one_mul

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.im (f x)‖ ≤ ‖f x‖
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
this : p = 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
simpa [this]

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝¹ : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst✝ : p.HolderTriple q' r
⊢ q = q'

Tactic:
rw [← inv_inj, ← inv_sub_inv_eq_inv q p hr, ← inv_sub_inv_eq_inv q' p hr]

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

pp: x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ y⁻¹ < (log y - log x) / (y - x)

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

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:
· rw [← div_lt_iff₀ hp', ← div_lt_div_right_of_neg hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · gcongr
      exact mul_lt_of_one_lt_left hs' 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) < log (1 + s) * p
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 0 < p.toReal

pp: p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 0 < q.toReal

Tactic:
all_goals simpa [← coe_toNNReal_eq_toReal]

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

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

Tactic:
all_goals simpa [← coe_toNNReal_eq_toReal]

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)

Tactic:
have q : 0 < z - y := by rwa [sub_pos]

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT 0 f
hg : StrongLT 0 g
⊢ Antivary f g⁻¹ ↔ Monovary f g

Tactic:
antivary_inv_right₀ hg

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT 0 f
hg : StrongLT 0 g
⊢ Monovary f g ↔ Monovary f g
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : 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
⊢ ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

Tactic:
rcases A with ⟨i, his, hzi, hwi⟩
    rw [prod_eq_zero his]
    · exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)
    · rw [hzi]
      exact zero_rpow hwi

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
one_mul

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

Goal state before:
pp: case neg
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
h_mul : a ^ p + 1 * b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
one_mul

Goal state after:
case neg
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
h_mul : a ^ p + b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = a ^ (1 * q)

Tactic:
one_mul

Goal state after:
p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = a ^ q
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 : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
⊢ ∏ i ∈ s, z k ^ w i = ∑ i ∈ s, w i * z k

Tactic:
← rpow_sum_of_nonneg (hz k hk) (hw · · |>.le),

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 : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
⊢ z k ^ ∑ x ∈ s, w x = ∑ i ∈ s, w i * z k
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 : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
⊢ z k = 1 * z k

Tactic:
one_mul

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 : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
⊢ z k = z k
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
hp1 : p ≤ 1
⊢ (z₁ + z₂) ^ p ≤ 1 * (z₁ ^ p + z₂ ^ p)

Tactic:
one_mul

Goal state after:
case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
hp1 : p ≤ 1
⊢ (z₁ + z₂) ^ p ≤ z₁ ^ p + z₂ ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case hp
α : 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
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : ι → ℝ := ⋯
hq : ∑ i ∈ s, q i = 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ 0 ≤ p i₀

Tactic:
exact h2p i₀ <| mem_insert_self ..

Goal state after: