mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case h
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
this : ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤ C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
i : ι
hi : i ∈ s
⊢ ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ (K * (‖e i‖ * ‖f i‖)) ^ r.toReal

Tactic:
← mul_assoc

Goal state after:
case h
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
this : ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤ C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
i : ι
hi : i ∈ s
⊢ ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ (K * ‖e i‖ * ‖f i‖) ^ r.toReal
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
u_fred : u.IsFredholm
dom₁ : Submodule 𝕜 E
codom₀ : Submodule 𝕜 F
h_dom : IsTopCompl (↑u).ker dom₁
h_codom : IsTopCompl (↑u).range codom₀
x : E
hx : x ∈ dom₁
⊢ u x =
    ({ X₀ := codom₀, X₁ := (↑u).range, isTopCompl := h_codom, finite_X₀ := ⋯ }.X₁.subtypeL ∘SL
        ↑(((↑u).ker.quotientEquivOfIsTopCompl dom₁ h_dom).symm.trans (ContinuousLinearEquiv.quotKerEquivRange ⋯)) ∘SL
          { X₀ := (↑u).ker, X₁ := dom₁, isTopCompl := ⋯, finite_X₀ := ⋯ }.proj)
      x

Tactic:
simp [hx, projection_apply_of_mem_left, ContinuousLinearEquiv.quotKerEquivRange]

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ y ∈ interior s

Tactic:
have hyz : ∀ i, z i < y i := by
    refine fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans ?_)
    rw [← Real.norm_eq_abs, ← dist_eq_norm']
    exact (hxz _).le

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz : ∀ (i : ι), z i < y i
⊢ y ∈ interior s
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ gronwallBound δ K ε' 0

Tactic:
gronwallBound_x0

Goal state after:
case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ δ
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
t₁ t₂ : ↑(Icc tmin tmax)
⊢ ‖∫ (x : ℝ) in ↑t₂..↑t₁, f x (α.compProj x)‖ ≤ ↑L * |↑t₁ - ↑t₂|

Tactic:
apply intervalIntegral.norm_integral_le_of_norm_le_const

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
t₁ t₂ : ↑(Icc tmin tmax)
⊢ ∀ x ∈ uIoc ↑t₂ ↑t₁, ‖f x (α.compProj x)‖ ≤ ↑L
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * ↑C ^ i ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * (dist α (next hf hx α) * ↑C ^ i)

Tactic:
← mul_assoc

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * ↑C ^ i ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α) * ↑C ^ i
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
hc : 0 ≤ c
h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty
⊢ ∀ j < Nat.find h_nonempty, v (p.coeff j) * c ^ j < gaussNorm v c p

Tactic:
intro j hj_lt

Goal state after:
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
hc : 0 ≤ c
h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty
j : ℕ
hj_lt : j < Nat.find h_nonempty
⊢ v (p.coeff j) * c ^ j < gaussNorm v c p
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f g : C(X, ℝ)
hfg : realToRCLike 𝕜 f = realToRCLike 𝕜 g
x : X
⊢ f x = g x

Tactic:
simpa using congr($hfg x)

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * ((↑b)⁻¹ * (↑b)⁻¹ ^ x)

Tactic:
← mul_assoc

Goal state after:
case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * (↑b)⁻¹ * (↑b)⁻¹ ^ x
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * ((↑b)⁻¹ * (↑b)⁻¹ ^ n)

Tactic:
← mul_assoc

Goal state after:
case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b)⁻¹ * (↑b)⁻¹ ^ n
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * ((↑b)⁻¹ * (↑b)⁻¹ ^ x)

Tactic:
← mul_assoc

Goal state after:
case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * (↑b)⁻¹ * (↑b)⁻¹ ^ x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ N ^ n
⊢ False

Tactic:
← Int.dvd_natAbs,

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ ↑(N ^ n).natAbs
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ ↑r < ofSeq f

Tactic:
by
  rw [← neg_neg r, coe_neg]; exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

Tactic:
by
  rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ 2 ^ 2 * (x * y) ≤ (x + y) ^ 2

Tactic:
← mul_assoc

Goal state after:
x y : ℝ≥0
⊢ 2 ^ 2 * x * y ≤ (x + y) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: n : WithTop ℕ∞
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬↑coshOpenPartialHomeomorph.symm x = 0

Tactic:
exact (arcosh_pos hx).ne'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (if (1 - z * I).arg = π then π else -(1 - z * I).arg) ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
z₂.1,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (if False then π else -(1 - z * I).arg) ∈ Set.Ioo (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π

Tactic:
rw [show -(π / 2) + -(π / 2) = -π by ring] at c₁

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -π < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p ≤ log 2

Tactic:
obtain rfl | hp := eq_or_ne p 2⁻¹

Goal state after:
case inl
⊢ binEntropy 2⁻¹ ≤ log 2

case inr
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ (conjSqrt c) ((conjSqrt c⁻¹ʳ) a) = a

Tactic:
grind [conjSqrt_ringInverse_conjSqrt _ _ hc.ringInverse]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
hab : a ≤ b
ha : 0 ≤ a
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
have hb : 0 ≤ b := ha.trans hab

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos.inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

pp: case pos.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
· simp_all [mem_singleton_iff]

Goal state after:
case pos.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
ha : 0 ≤ a
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b

Tactic:
have hb : 0 ≤ b := ha.trans hab

Goal state after:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume a b

Tactic:
have hf_cint : IntervalIntegrable f volume (c * a) (c * b) :=
    intervalIntegrable_iff.mpr
      ((hf.integrableOn_compact_subset (by simp [uIcc, Icc_subset_Ioi_iff, mul_pos hc ha,
        mul_pos hc hb]) isCompact_uIcc).mono_set uIoc_subset_uIcc)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume a b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
⊢ min a b * t = min (a * t) (b * t)

Tactic:
min_mul_of_nonneg _ _ ht_pos.le

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
⊢ min (a * t) (b * t) = min (a * t) (b * t)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case hb
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0

Tactic:
apply Gamma_ne_zero_of_re_pos

Goal state after:
case hb
s : ℂ
hs : 0 < s.re
⊢ 0 < (s / 2).re
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 49 / 20 - 2 / 3 < log 6

Tactic:
lt_log_iff_exp_lt (by positivity)

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (49 / 20 - 2 / 3) < 6
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ ↑(Nat.log b ⌊1⌋₊) = -↑(Nat.clog b 1)

Tactic:
Nat.floor_one,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ ↑(Nat.log b 1) = -↑(Nat.clog b 1)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ ↑(Nat.log b ⌊1⌋₊) = 0

Tactic:
Nat.floor_one,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ ↑(Nat.log b 1) = 0
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

pp: case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
· have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
    rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]
    exact Nat.clog_mono_right b <| Nat.ceil_mono <| (inv_le_inv₀ h₀' h₀).2 h

Goal state after:
case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ ↑(Nat.clog b 1) = -↑(Nat.log b ⌊1⌋₊)

Tactic:
Nat.floor_one,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ ↑(Nat.clog b 1) = -↑(Nat.log b 1)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ (clog b r - 1) < r

Tactic:
by
  rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ hr]
  · exact lt_zpow_succ_log_self hb _
  · exact zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ Convex ℝ (Unitization.inr '' Ici 0)

Tactic:
exact Convex.linear_image (convex_Ici _) (Unitization.inrHom ℝ ℂ A)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ b ^ y ≤ b ^ logb b x ↔ b ^ y ≤ x

Tactic:
rpow_logb b_pos (b_ne_one b_lt_one) hx

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ b ^ y ≤ x ↔ b ^ y ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ b ^ y < b ^ logb b x ↔ b ^ y < x

Tactic:
rpow_logb b_pos (b_ne_one b_lt_one) hx

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ b ^ y < x ↔ b ^ y < x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ log x = 0 ∨ log b = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
log_eq_zero

Goal state after:
b x : ℝ
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ Integrable (⇑f) μ

Tactic:
refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩
  calc  ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ‖f‖₊ * (μ Set.univ) := f.lintegral_nnnorm_le μ
    _ < ∞                   := ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top μ Set.univ)

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
inst✝¹ : OpensMeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (const X c - f) x ∂μ = μ.real Set.univ • c - ∫ (x : X), f x ∂μ

Tactic:
simp [integral_sub (integrable_const c) (f.integrable _)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℤ × ℤ
⊢ ↑(L.latticeEquivProd.symm x) = ↑x.1 * L.ω₁ + ↑x.2 * L.ω₂

Tactic:
by
  simp [latticeEquivProd, Finsupp.linearCombination]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ guess ^ (n + 2) ≤ a

Tactic:
have : guess ≤ a / guess ^ (n + 1) := by
        linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]

Goal state after:
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
this : guess ≤ a / guess ^ (n + 1)
⊢ guess ^ (n + 2) ≤ a
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case one
θ : ℂ
⊢ eval (cos θ) (U ℂ 1) * sin θ = sin ((↑1 + 1) * θ)

Tactic:
simp [one_add_one_eq_two, sin_two_mul]; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1

Tactic:
refine ⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩

Goal state after:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1