mathlib-initiative/mathlib-tactics huggingface dataset:
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
n i : ℕ
⊢ i < n →
    dist ((next hf hx)^[i] α) ((next hf hx)^[i + 1] α) ≤
      (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)

Tactic:
hi

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
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i + 1] α) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)
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 : ℕ
⊢ i < n →
    dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i + 1] α) ≤
      (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)

Tactic:
hi

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]^[i] α) ((next hf hx)^[m]^[i + 1] α) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

Tactic:
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : eval x Q ∣ eval x R + eval x (Q * (P /ₘ Q)) ∧ |eval x R| < |eval x Q|
⊢ x ∈ {x | R.IsRoot x}

Tactic:
eval_mul,

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : eval x Q ∣ eval x R + eval x Q * eval x (P /ₘ Q) ∧ |eval x R| < |eval x Q|
⊢ x ∈ {x | R.IsRoot x}
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi : (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) = v (p.coeff i) * c ^ i
⊢ (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) ≤ ⨆ i, v (p.coeff i) * c ^ i

Tactic:
hi

Goal state after:
case a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi : (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) = v (p.coeff i) * c ^ i
⊢ v (p.coeff i) * c ^ i ≤ ⨆ i, v (p.coeff i) * c ^ i
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ 0 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
i : ℕ
⊢ 0 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := ↑K * a + ‖f x₀‖ + 1
hL : L = ↑K * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ x ∈ closedBall x₀ (a / 2), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
t₀ : ℝ
⊢ 1 ≤ 2 - 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
⊢ 0 < -eval x P

Tactic:
have := eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos hroots' (nonpos_of_neg_nonneg hlc')

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
this : eval (-x) (P.comp (-X)) < 0
⊢ 0 < -eval x P
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
H : ∀ {a b : α}, f a ≠ f b → f a > f b → f (a + b) = max (f a) (f b)
hab : ¬f a > f b
⊢ f (a + b) = max (f a) (f b)

Tactic:
simpa [add_comm, max_comm] using (H hne.symm ((not_lt.mp hab).lt_of_ne hne))

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
by_cases! hp : p = 0

Goal state after:
case pos
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p = 0
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

case neg
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
⊢ 0 < 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
⊢ 4 ≤ 6

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
⊢ (4 / 2 ^ 2 / 2 ^ n) ^ 3 = ((2 ^ n) ^ 3)⁻¹

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 4 = 2 ^ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 * n) ≠ 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) ≠ 0

Tactic:
norm_num

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

Goal state before:
pp: ⊢ stdPart ω = 0

Tactic:
stdPart_eq_zero

Goal state after:
⊢ ArchimedeanClass.mk ω ≠ 0
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ 3.15 + 1 / 2 ≤ ↑3 + 1

Tactic:
norm_num

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

Goal state before:
pp: case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
⊢ stdPart x = 0

Tactic:
stdPart_eq_zero

Goal state after:
case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
⊢ ArchimedeanClass.mk x ≠ 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ p.mapMahlerMeasure v ≤ p.sum fun x a ↦ ‖a‖

Tactic:
by
  apply mahlerMeasure_le_sum_norm_coeff _ |>.trans_eq
  rw [sum_def, sum_def, support_map_of_injective _ hv.injective]
  exact Finset.sum_congr rfl fun x _ ↦ by
    simp [hv.norm_map_of_map_zero (map_zero _)]

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

Goal state before:
pp: case refine_2
x : ℝ*
x✝ : 0 < x ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : 0 < x
hx' : ArchimedeanClass.mk x < 0
⊢ ↑r < x

Tactic:
exact lt_of_mk_lt_mk_of_nonneg (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
let u₁' (x : ℝ) : ℝ := - (2 * (n + 1) * x * f x ^ n)

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case zero
⊢ 1 = 1 * ↑1 ^ 4 / (↑1 ^ 2 * (2 * ↑0 + 1))

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1

Tactic:
W_eq_integral_sin_pow_div_integral_sin_pow,

Goal state after:
k : ℕ
⊢ (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤ 1
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k

Tactic:
W_eq_integral_sin_pow_div_integral_sin_pow,

Goal state after:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

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

Tactic:
norm_num

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

Goal state before:
pp: x y : ℝ≥0
⊢ 0 ≤ 2⁻¹

Tactic:
norm_num

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

Goal state before:
pp: x y : ℝ≥0
⊢ 2⁻¹ < 1

Tactic:
norm_num

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

Goal state before:
pp: x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ √((1 + tanh x) / (1 - tanh x)) ^ 2 = rexp x ^ 2

Tactic:
sq_sqrt (le_of_lt h),

Goal state after:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ (1 + tanh x) / (1 - tanh x) = rexp x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ ↑(n - k) * ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n * ↑n ^ k

Tactic:
refine IsEquivalent.mul ?_ h

Goal state after:
case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ ↑(n - k)) ~[atTop] Nat.cast
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ 2⁻¹ < 1

Tactic:
norm_num

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

Goal state before:
pp: case hg
⊢ Tendsto (fun x ↦ -log x) (𝓝[>] 0) atTop

Tactic:
apply tendsto_neg_atTop_iff.mpr tendsto_log_nhdsGT_zero

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

Goal state before:
pp: ⊢ 1 - 2⁻¹ < 1

Tactic:
norm_num

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

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ 1 - 2⁻¹ < 1

Tactic:
norm_num

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

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a✝¹ : ℝ
a✝ : 1 - 2⁻¹ < a✝¹ ∧ a✝¹ < 1
⊢ 1 = 2⁻¹ + 2⁻¹

Tactic:
norm_num

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

Goal state before:
pp: q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ 0 < 2⁻¹

Tactic:
norm_num

Goal state after:
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) a)⁻¹ʳ = (conjSqrt c⁻¹ʳ) a⁻¹ʳ

Tactic:
by_cases ha : IsUnit a

Goal state after:
case pos
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
ha : IsUnit a
⊢ ((conjSqrt c) a)⁻¹ʳ = (conjSqrt c⁻¹ʳ) a⁻¹ʳ

case neg
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
ha : ¬IsUnit a
⊢ ((conjSqrt c) a)⁻¹ʳ = (conjSqrt c⁻¹ʳ) a⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ Icc 0 2⁻¹ = Icc 0 (1 - 1 / 2)

Tactic:
norm_num

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

Goal state before:
pp: ⊢ Icc 2⁻¹ 1 = Icc (1 / 2) 1

Tactic:
norm_num

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

Goal state before:
pp: ⊢ Icc (1 / 2) 1 = Icc (1 - 1 / ↑2) 1

Tactic:
norm_num

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

Goal state before:
pp: case left
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: case right
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
⊢ 1 * |1 - -1| ≤ 2

Tactic:
norm_num

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: case inl
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_zero : t = 0
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
| inl ht_zero =>

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

Goal state before:
pp: case refine_1.refine_1
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (fun q ↦ q.1 ^ (p - 1)) (Ioi 0 ×ˢ s)

Tactic:
exact ContinuousOn.rpow_const (by fun_prop) (by grind)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ ↑(harmonic 6) - log (↑6 + 1) = 49 / 20 - log 7

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 0 ≤ 49 / 20 - 1 / 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 <
    ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / ↑i.factorial + (49 / 20 - 1 / 2) ^ 0 / ↑(Nat.factorial 0) +
                (49 / 20 - 1 / 2) ^ 1 / ↑((0 + 1) * Nat.factorial 0) +
              (49 / 20 - 1 / 2) ^ 2 / ↑((1 + 1) * ((0 + 1) * Nat.factorial 0)) +
            (49 / 20 - 1 / 2) ^ 3 / ↑((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))) +
          (49 / 20 - 1 / 2) ^ 4 / ↑((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0)))) +
        (49 / 20 - 1 / 2) ^ 5 / ↑((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))) +
      (49 / 20 - 1 / 2) ^ 6 / ↑((5 + 1) * ((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))))

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ (if 6 = 0 then 2 else ↑(harmonic 6) - log ↑6) = 49 / 20 - log 6

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

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

Tactic:
norm_num

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (107 / 60) < 6
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ 107 < 6 ^ OfNat.ofNat 60

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Tactic:
have h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1) := by
    intro n h
    specialize hs (2 * n + 1)
    simp_all

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_1
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
x : ℝ
hx : 0 < x
⊢ ∀ (m : ℕ), x ≠ -↑m

Tactic:
exact fun m ↦ ne_of_gt (by linarith)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_2
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
x : ℝ
hx : 0 < x
⊢ ∀ (m : ℕ), x ≠ -↑m

Tactic:
exact fun m ↦ ne_of_gt (by linarith)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * (s - 1) / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
(by ring : s + 1 = (s - 1) + 2),

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * (s - 1) / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * (s - 1 + 2).Gammaℝ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos ((↑π * s - ↑π * 1) / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹

Tactic:
sub_div,

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * s / 2 - ↑π * 1 / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
norm_num

Goal state after:
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 : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ ↑(Nat.log b ⌊r⌋₊) = 0

Tactic:
Nat.log_of_left_le_one hb,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + log ↑(2 ^ 2 * π)) / 2 = -(↑γ + log (4 * ↑π)) / 2

Tactic:
norm_num

Goal state after:
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 : ℕ
r : R
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r

pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r

Tactic:
· obtain hr | hr := le_total 1 r
    · rw [clog_of_right_le_one _ (inv_le_one_of_one_le₀ hr), log_of_one_le_right _ hr, inv_inv]
    · rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r
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 : ℕ
hb : b ≤ 1
r : R
⊢ clog b r = 0

Tactic:
by
  rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]

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

Goal state before:
pp: ⊢ rexp (-1) < 1

Tactic:
norm_num

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

Goal state before:
pp: ⊢ 2 = (1 / 2)⁻¹

Tactic:
norm_num

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

Goal state before:
pp: case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌈0⌉ = 0

Tactic:
Int.ceil_zero

Goal state after:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ rexp (-(ε * g x * g x)) ≤ 1

Tactic:
rw [exp_le_one_iff, Left.neg_nonpos_iff, mul_assoc]

Goal state after:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * (g x * g x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ (fun x ↦ c) =o[atTop] logb b

Tactic:
rw [Asymptotics.isLittleO_const_left, or_iff_not_imp_left]
  intro hc
  exact tendsto_abs_logb_atTop hb

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

Goal state before:
pp: k n : ℕ
⊢ ↑k < ↑n - 1 → ↑(k.descFactorial n) = 0 ↑k

Tactic:
Pi.zero_apply,

Goal state after:
k n : ℕ
⊢ ↑k < ↑n - 1 → ↑(k.descFactorial n) = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_1
L : PeriodPair
α β : ℚ
H : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
⊢ α.den = 1 ∧ β.den = 1

Tactic:
obtain ⟨m, n, e⟩ := mem_lattice.mp H

Goal state after:
case refine_1
L : PeriodPair
α β : ℚ
H : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
m n : ℤ
e : ↑m * L.ω₁ + ↑n * L.ω₂ = ↑α * L.ω₁ + ↑β * L.ω₂
⊢ α.den = 1 ∧ β.den = 1