mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Tactic:
;

Goal state after:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
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)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) + 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Tactic:
;

Goal state after:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) + 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Tactic:
;

Goal state after:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ (↑c / ↑d).sqrtTwoAddSeries n

Tactic:
;

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ (↑c / ↑d).sqrtTwoAddSeries n
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
this : 0 ≤ x
⊢ 0 ≤ ↑b ^ n * x

Tactic:
;

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
this : 0 ≤ x
⊢ 0 ≤ ↑b ^ n * x
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n

Tactic:
;

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
n : ℕ
hn : r < ↑n
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → r < ↑b

Tactic:
exact ⟨n, fun m hm ↦ hn.trans_le (mod_cast hm)⟩

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

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)

Tactic:
;

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (√(2 + ↑c / ↑d)).sqrtTwoAddSeries n

Tactic:
;

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (√(2 + ↑c / ↑d)).sqrtTwoAddSeries n
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: z : ℤ
⊢ sqrt ↑z = ↑(Int.sqrt z)

Tactic:
simp only [sqrt, num_intCast, den_intCast, Nat.sqrt_one, mkRat_one]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: a b : ℤ
hx : Irrational (↑a / ↑b)
⊢ False

Tactic:
;

Goal state after:
a b : ℤ
hx : Irrational (↑a / ↑b)
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x ↦ -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝

Tactic:
;

Goal state after:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x ↦ -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
;

Goal state after:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -↑(-r) < ofSeq f
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Tactic:
;

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Tactic:
;

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ 1 ≠ 0

Tactic:
;

Goal state after:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ 1 ≠ 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ 0 ≤ ArchimedeanClass.mk x

Tactic:
have h := h 1 zero_lt_one
      exact mk_nonneg_of_le_of_le_of_archimedean coeRingHom h.1.le h.2.le

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

Goal state before:
pp: case neg
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
hp : ¬p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
have hv_ne : v p.leadingCoeff ≠ 0 :=
      fun h ↦ hp <| hv.injective <| h.trans (map_zero _).symm
    have hv_norm : ‖v p.leadingCoeff‖ = ‖p.leadingCoeff‖ := hv.norm_map_of_map_zero (map_zero _) _
    grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]

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

Goal state before:
pp: case refine_1
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ (fun x1 x2 ↦ x1 - x2) (stdPart x) y < stdPart x

Tactic:
;

Goal state after:
case refine_1
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ (fun x1 x2 ↦ x1 - x2) (stdPart x) y < stdPart x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ stdPart x < (fun x1 x2 ↦ x1 + x2) (stdPart x) y

Tactic:
;

Goal state after:
case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ stdPart x < (fun x1 x2 ↦ x1 + x2) (stdPart x) y
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s t : ℝ
⊢ r = s → s = t → r = t

Tactic:
;

Goal state after:
r s t : ℝ
⊢ r = s → s = t → r = t
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False

Tactic:
;

Goal state after:
x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
;

Goal state after:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (y * x).InfiniteNeg
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite

Tactic:
;

Goal state after:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case hf0
⊢ Tendsto (fun i ↦ 2 * ↑i + 1) atTop atTop

Tactic:
;

Goal state after:
case hf0
⊢ Tendsto (fun i ↦ 2 * ↑i + 1) atTop atTop
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case zero
⊢ 0 < ∏ i ∈ range 0, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))

Tactic:
;

Goal state after:
case zero
⊢ 0 < ∏ i ∈ range 0, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
⊢ (1 - 1 ^ 2) ^ (n + 1) = 0

Tactic:
;

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)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
⊢ (1 - 1 ^ 2) ^ (n + 1) = 0
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
⊢ (1 - (-1) ^ 2) ^ (n + 1) = 0

Tactic:
;

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)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
⊢ (1 - (-1) ^ 2) ^ (n + 1) = 0
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1

Tactic:
;

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : ¬z.re = π / 2
⊢ ¬z.re = ↑(2 * k + 1) * π / 2

Tactic:
;

Goal state after:
case inl
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : ¬z.re = π / 2
⊢ ¬z.re = ↑(2 * k + 1) * π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ cos z ≠ 0

Tactic:
by
  refine cos_ne_zero_iff.mpr (fun k ↦ ?_)
  rw [ne_eq, Complex.ext_iff, not_and_or] at h₀ ⊢
  norm_cast at h₀ ⊢
  rcases h₀ with nr | ni
  · left; contrapose nr
    rw [nr, mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_of_pos_right (by positivity)] at h₁
    rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂
    norm_cast at h₁ h₂
    change -1 < _ at h₁
    rwa [show 2 * k + 1 = 1 by lia, Int.cast_one, one_mul] at nr
  · exact Or.inr ni

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

Goal state before:
pp: case e_a
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1

Tactic:
;

Goal state after:
case e_a
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: case h₂
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ √(x ^ 2 - 1)

Tactic:
;

Goal state after:
case h₂
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ √(x ^ 2 - 1)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: case h₂
x : ℝ
hx : 1 < x
⊢ 0 ≤ √(x ^ 2 - 1)

Tactic:
;

Goal state after:
case h₂
x : ℝ
hx : 1 < x
⊢ 0 ≤ √(x ^ 2 - 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2

Tactic:
;

Goal state after:
case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)

Tactic:
by
  induction n with
  | zero => simp [dist_gm_am_le]
  | succ n ih =>
    rw [agmSequences_succ']
    apply dist_gm_am_le.trans
    rw [pow_succ, ← div_div]
    gcongr

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

Goal state before:
pp: ⊢ 1 / 2 * log 2 + 1 / 2 * log 2 = log 2

Tactic:
;

Goal state after:
⊢ 1 / 2 * log 2 + 1 / 2 * log 2 = log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2

Tactic:
;

Goal state after:
⊢ 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)

Tactic:
;

Goal state after:
p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0

Tactic:
;

Goal state after:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (max z.re |z.im|)

Tactic:
← Real.log_mul,

Goal state after:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ Real.log ‖z‖ ≤ Real.log (√2 * max z.re |z.im|)

case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ √2 ≠ 0

case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ max z.re |z.im| ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0

Tactic:
;

Goal state after:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - 2⁻¹ < p

Tactic:
;

Goal state after:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - 2⁻¹ < p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
h : ¬p = 1 / 2
this : ∀ {p : ℝ}, ¬p = 1 / 2 → p < 1 / 2 → binEntropy p < log 2
hp : 1 / 2 ≤ p
⊢ 1 / 2 < p

Tactic:
;

Goal state after:
p : ℝ
h : ¬p = 1 / 2
this : ∀ {p : ℝ}, ¬p = 1 / 2 → p < 1 / 2 → binEntropy p < log 2
hp : 1 / 2 ≤ p
⊢ 1 / 2 < p
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖

Tactic:
by
          filter_upwards [isLittleO_iff_nat_mul_le'.1 hl.isLittleO_log_re_re n,
            hl.abs_im_pow_eventuallyLE_exp_re n,
            hl.tendsto_re.eventually_gt_atTop 1] with z hre him h₁
          rcases le_total |z.im| z.re with hle | hle
          · rwa [max_eq_left hle]
          · have H : 1 < |z.im| := h₁.trans_le hle
            norm_cast at *
            rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]

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

Goal state before:
pp: ⊢ Continuous fun p ↦ p.negMulLog + (1 - p).negMulLog

Tactic:
;

Goal state after:
⊢ Continuous fun p ↦ p.negMulLog + (1 - p).negMulLog
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p) * log (1 - p)⁻¹) 0

Tactic:
fun_prop (disch := simp)

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

Goal state before:
pp: case refine_2
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log p⁻¹) 1

Tactic:
fun_prop (disch := simp)

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

Goal state before:
pp: x✝ : ℝ
⊢ qaryEntropy 2 x✝ = binEntropy x✝

Tactic:
;

Goal state after:
x✝ : ℝ
⊢ qaryEntropy 2 x✝ = binEntropy x✝
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Continuous fun p ↦ p * log ↑(↑q - 1) + binEntropy p

Tactic:
;

Goal state after:
q : ℕ
⊢ Continuous fun p ↦ p * log ↑(↑q - 1) + binEntropy p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log ↑(↑q - 1) + binEntropy p) p

Tactic:
;

Goal state after:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log ↑(↑q - 1) + binEntropy p) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
x✝ : ℝ
⊢ log (↑q - 1) + log (1 - x✝) - log x✝ = log (↑q - 1) + (log (1 - x✝) - log x✝)

Tactic:
;

Goal state after:
q : ℕ
x✝ : ℝ
⊢ log (↑q - 1) + log (1 - x✝) - log x✝ = log (↑q - 1) + (log (1 - x✝) - log x✝)
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ (2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ) * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))

Tactic:
;

Goal state after:
θ : ℝ
n : ℕ
⊢ (2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ) * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) *
        ((↑n + 1) * ↑n ! *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 *
        (↑n ! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑n !) *
      ((2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)

Tactic:
;

Goal state after:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) *
        ((↑n + 1) * ↑n ! *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 *
        (↑n ! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑n !) *
      ((2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: 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
x✝ : ℝ≥0
⊢ x✝ ∈ Icc 0 1 ↔ x✝ ∈ Ioo 0 1 ∪ {0} ∪ {1}

Tactic:
;

Goal state after:
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
x✝ : ℝ≥0
⊢ x✝ ∈ Icc 0 1 ↔ x✝ ∈ Ioo 0 1 ∪ {0} ∪ {1}
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k

Tactic:
;

Goal state after:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
x✝ : ℝ≥0
⊢ x✝ ∈ Icc 0 1 ↔ x✝ ∈ Ioo 0 1 ∪ {0} ∪ {1}

Tactic:
;

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
x✝ : ℝ≥0
⊢ x✝ ∈ Icc 0 1 ↔ x✝ ∈ Ioo 0 1 ∪ {0} ∪ {1}
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
this : ∀ᶠ (a_1 : ℕ) in atTop, ↑a ^ (2 * a_1 + 1) / ↑a_1 ! < 1 / 2
⊢ ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1

Tactic:
filter_upwards [this] with n hn

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
this : ∀ᶠ (a_1 : ℕ) in atTop, ↑a ^ (2 * a_1 + 1) / ↑a_1 ! < 1 / 2
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! < 1 / 2
⊢ ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ q

Tactic:
exact concaveOn_nnrpow hp

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

Goal state before:
pp: p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * ‖p * log x‖ ^ 2 = p * ‖log x‖ ^ 2

Tactic:
by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]

Goal state after: