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

Goal state before:
pp: p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
⊢ Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), log ‖eval (circleMap 0 1 x) p‖ ∈ univ

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ 0 ≤ 2 * π

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
⊢ ((fun x ↦ Inv.inv ∘ x) fun x ↦ 0) =ᶠ[↑φ] fun x ↦ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
f g : α → β
⊢ ↑f < ↑g ↔ ∀* (x : α), f x < g x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
⊢ (fun x1 x2 ↦ x1 < x2) = LiftRel fun x1 x2 ↦ x1 < x2

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ = √((⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
⊢ max ↑a ↑b = map₂ max ↑a ↑b

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), ‖eval (circleMap 0 1 x) p‖ ∈ Ici 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
⊢ min ↑a ↑b = map₂ min ↑a ↑b

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √((⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) ^ 2) ≤ √(⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(max x y) = max ↑x ↑y

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
n : ℕ
⊢ 0 ≤ ofDigitsTerm digits n

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √(⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ ^ 2) = √(circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1)

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
n : ℕ
⊢ ofDigitsTerm digits n ≤ (↑b - 1) * (↑b ^ (n + 1))⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(min x y) = min ↑x ↑y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝¹ : AddCommGroup β
inst✝ : LinearOrder β
x : β
⊢ ↑|x| = |↑x|

Tactic:
by

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 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √(circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1) = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ 0 ≤ (↑b)⁻¹

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ Summable (ofDigitsTerm digits)

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ 0 ≤ ofDigits digits

Tactic:
by

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

Goal state before:
pp: p : ℂ[X]
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
by

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

Goal state before:
pp: p : ℂ[X]
⊢ 0 ≤ ↑p.natDegree + 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 0 ≤ (↑b)⁻¹

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ (↑b)⁻¹ < 1

Tactic:
by

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

Goal state before:
pp: p : ℂ[X]
⊢ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) ≤ √(↑p.natDegree + 1) * p.supNorm

Tactic:
by

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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ ofDigits digits ≤ 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
a : ℕ → Fin b
n : ℕ
⊢ ofDigits a = ∑ i ∈ Finset.range n, ofDigitsTerm a i + (↑b ^ n)⁻¹ * ofDigits fun i ↦ a (i + n)

Tactic:
by

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

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
i : ℕ
hi : i ∈ Finset.range n
⊢ ofDigitsTerm x i = ofDigitsTerm y i

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ 0 < ‖p.leadingCoeff‖

Tactic:
by

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

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i
⊢ 0 ≤ (↑b ^ n)⁻¹

Tactic:
by

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

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |ofDigits x - ofDigits y| ≤ (↑b ^ n)⁻¹

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π := by
    rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
    focus
      apply sin_lt
      apply div_pos pi_pos
    all_goals apply pow_pos; norm_num
  refine lt_of_le_of_lt (le_of_eq ?_) this
  rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]; simp

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

Goal state before:
pp: n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ x.toFinset, ‖z‖ ^ count z x ≤ ∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 6 ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z p.roots

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

Tactic:
by

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

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

Tactic:
by

Goal state after:
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⌋₊
⊢ 0 ≤ ↑b ^ n * x

Tactic:
by

Goal state after:
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⌋₊
h_le : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ ↑b ^ n * x
hb : b ≠ 0
⊢ 0 < ↑b ^ n

Tactic:
by

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

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

Tactic:
by

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

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Summable fun i ↦ ‖ofDigitsTerm (x.digits b) i‖

Tactic:
by

Goal state after:
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) ≤ z

Tactic:
by

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

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ HasSum (ofDigitsTerm (x.digits b)) x

Tactic:
by

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
x : ℝ
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ ofDigits (x.digits b) = x

Tactic:
by

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
⊢ 1 < |↑b + 1|

Tactic:
by

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ‖(↑(b + 1))⁻¹‖ < 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ 0 ≤ (↑(b + 1))⁻¹

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ ↑r < ω

Tactic:
by

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ (↑(b + 1))⁻¹ < 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)| < |ArchimedeanOrder.val (ArchimedeanOrder.of ω)|

Tactic:
by

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

Goal state before:
pp: ⊢ stdPart ω = 0

Tactic:
by

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

Goal state before:
pp: ⊢ 0 < ArchimedeanClass.mk ε

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
hxr : Germ.Tendsto x (𝓝 r)
⊢ (Germ.map f x).Tendsto (𝓝 (f r))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ℝ*
r s : ℝ
f : ℝ → ℝ → ℝ
hxr : Germ.Tendsto x (𝓝 r)
hys : Germ.Tendsto y (𝓝 s)
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ (Germ.map₂ f x y).Tendsto (𝓝 (f r s))

Tactic:
by

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
⊢ (ofDigits fun x ↦ Fin.last b) = 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ (ofDigits fun x ↦ ⟨b - 1, ⋯⟩) = 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ b ≠ 0

Tactic:
by

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
⊢ z ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)

Tactic:
by

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

Goal state before:
pp: ⊢ 3 < π

Tactic:
by

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

Goal state before:
pp: ⊢ π < 4

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
⊢ ∑ x ∈ S.toFinset, ↑(count x S) * ‖x.prod‖ ≤
    ∑ x ∈ S.toFinset, ↑(count x S) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
by

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

Goal state before:
pp: ⊢ 3.14 < π

Tactic:
by

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

Goal state before:
pp: ⊢ π < 3.15

Tactic:
by

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

Goal state before:
pp: ⊢ 3.1415 < π

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ Set.SurjOn ofDigits Set.univ (Set.Icc 0 1)

Tactic:
by

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

Goal state before:
pp: ⊢ π < 3.1416

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ 0 < n + 2 ∧ 1 < n + 2

Tactic:
by

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

Goal state before:
pp: ⊢ 3.141592 < π

Tactic:
by

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

Goal state before:
pp: b✝ n : ℕ
hb0 : 0 < n + 2
b : ℕ
hb : 1 < b
⊢ Continuous ofDigits

Tactic:
rify at hb0 hb

Goal state after:
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ Continuous ofDigits
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ π < 3.141593

Tactic:
by

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

Goal state before:
pp: ⊢ 3.14159265358979323846 < π

Tactic:
by

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

Goal state before:
pp: ⊢ π < 3.14159265358979323847

Tactic:
by

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

Goal state before:
pp: b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ 0 ≤ (↑b)⁻¹

Tactic:
by

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

Goal state before:
pp: ⊢ π < ↑3 + 1

Tactic:
by

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

Goal state before:
pp: ⊢ ↑4 - 1 < π

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ round π = 3

Tactic:
by

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

Goal state before:
pp: b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ (↑b - 1) * (↑b ^ (n + 1))⁻¹ ≤ ↑b * (↑b ^ (n + 1))⁻¹

Tactic:
by

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

Goal state before:
pp: b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ ↑b * (↑b ^ (n + 1))⁻¹ = (↑b ^ n)⁻¹

Tactic:
by

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

Goal state before:
pp: b : ℕ
⊢ Continuous ofDigits

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: q : ℚ
⊢ sqrt (q * q) = |q|

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: x : ℚ
x✝ : ∃ q, q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: m : ℚ
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: n : ℕ
⊢ sqrt ↑n = ↑n.sqrt

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ Irrational x ↔ ∀ (a b : ℤ), b ≠ 0 → x ≠ ↑a / ↑b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : Irrational x
a b : ℤ
⊢ x ≠ ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : ¬Irrational x
⊢ ∃ q, x = ↑q

Tactic:
by

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

Goal state before:
pp: r : ℝ
tr : Transcendental ℚ r
⊢ Irrational r

Tactic:
by

Goal state after:
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 : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
⊢ ↑↑D ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
⊢ ∑ x ∈ S.toFinset, ↑(count x S) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod =
    ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
⊢ Germ.Tendsto x (𝓝 r) ↔ (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ 0 ≤ ArchimedeanClass.mk x

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ stdPart x = r

Tactic:
by

Goal state after: