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

Goal state before:
pp: case a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := ⋯
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
a✝ : a ∈ p.roots.toFinset
⊢ x ≤ p.roots

Tactic:
·

Goal state after:
case a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := ⋯
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
a✝ : a ∈ p.roots.toFinset
⊢ x ≤ p.roots
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) = 2 ^ (n + 2 + 2 * n)

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

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:
·

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

Goal state before:
pp: case e'_5
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ x = x - 0

pp: case convert_3
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ |(↑b)⁻¹| < 1

Tactic:
·

Goal state after:
case e'_5
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ x = x - 0
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case convert_3
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ |(↑b)⁻¹| < 1

Tactic:
·

Goal state after:
case convert_3
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ |(↑b)⁻¹| < 1
Module: Mathlib.Analysis.Real.OfDigits

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

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

Tactic:
·

Goal state after:
b : ℕ
inst✝ : NeZero b
x : ℝ
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ HasSum (ofDigitsTerm (x.digits b)) x
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
·

Goal state after:
b : ℕ
inst✝ : NeZero b
x : ℝ
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Summable (ofDigitsTerm (x.digits b))
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
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n

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

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

Tactic:
·

Goal state after:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ↑↑(Fin.last b) * ∑' (i : ℕ), (↑(b + 1))⁻¹ ^ (i + 1) = 1

pp: case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)

Tactic:
·

Goal state after:
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ↑↑(Fin.last b) * ∑' (i : ℕ), (↑(b + 1))⁻¹ ^ (i + 1) = 1
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
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)

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

Tactic:
·

Goal state after:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)
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
⊢ 0 < 2 ^ (n + 1)

Tactic:
·

Goal state after:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)

Tactic:
·

Goal state after:
case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_1
b : ℕ
hb : 1 < b
⊢ b = b - 1 + 1

pp: b : ℕ
hb : 1 < b
⊢ NeZero (b - 1)

Tactic:
·

Goal state after:
case e'_1
b : ℕ
hb : 1 < b
⊢ b = b - 1 + 1
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ NeZero (b - 1)

Tactic:
·

Goal state after:
b : ℕ
hb : 1 < b
⊢ NeZero (b - 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
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ ↑a ^ 2 / ↑b ^ 2 ≤ (2 * ↑d + ↑c) / ↑d

Tactic:
div_le_div_iff₀ (pow_pos hb' _) hd'

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
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ ↑a ^ 2 * ↑d ≤ (2 * ↑d + ↑c) * ↑b ^ 2
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∈ Set.Ico 0 1
⊢ y ∈ ofDigits '' Set.univ

pp: case neg
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∉ Set.Ico 0 1
⊢ y ∈ ofDigits '' Set.univ

Tactic:
·

Goal state after:
case pos
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∈ Set.Ico 0 1
⊢ y ∈ ofDigits '' Set.univ
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∉ Set.Ico 0 1
⊢ y ∈ ofDigits '' Set.univ

Tactic:
·

Goal state after:
case neg
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∉ Set.Ico 0 1
⊢ y ∈ ofDigits '' Set.univ
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ 3.141592 < π

Tactic:
by
  -- bound[3141592*^-6, Iters -> 10, Rounding -> .8, Precision -> 16]
  pi_lower_bound [
    11482/8119, 7792/4217, 54055/27557, 2-623/64690, 2-337/139887, 2-208/345307, 2-167/1108925,
    2-64/1699893, 2-31/3293535, 2-48/20398657]

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

Goal state before:
pp: case refine_1
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s < r
⊢ ↑s ≤ ofSeq f

pp: case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

pp: case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
·

Goal state after:
case refine_1
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s < r
⊢ ↑s ≤ ofSeq f
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case refine_1
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ ∀ (i : ℕ), Continuous fun x ↦ ofDigitsTerm x i

pp: case refine_2
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ Summable fun i ↦ (↑b)⁻¹ ^ i

pp: case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ ‖ofDigitsTerm x n‖ ≤ (↑b)⁻¹ ^ n

Tactic:
·

Goal state after:
case refine_1
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ ∀ (i : ℕ), Continuous fun x ↦ ofDigitsTerm x i
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case refine_2
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ Summable fun i ↦ (↑b)⁻¹ ^ i

pp: case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ ‖ofDigitsTerm x n‖ ≤ (↑b)⁻¹ ^ n

Tactic:
·

Goal state after:
case refine_2
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ Summable fun i ↦ (↑b)⁻¹ ^ i
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
·

Goal state after:
case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ ‖ofDigitsTerm x n‖ ≤ (↑b)⁻¹ ^ n
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

pp: case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
·

Goal state after:
case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
·

Goal state after:
case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
match b with
  | 0 => fun_prop
  | 1 => fun_prop
  | n + 2 =>
    obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
    generalize n + 2 = b at hb
    rify at hb0 hb
    refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_
    · simp only [ofDigitsTerm]
      fun_prop
    · exact summable_geometric_of_lt_one (by positivity) (inv_lt_one_of_one_lt₀ hb)
    · simp only [norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg, inv_pow]
      apply ofDigitsTerm_le.trans
      calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind

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

Goal state before:
pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
·

Goal state after:
case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x

pp: case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ Irrational x

Tactic:
·

Goal state after:
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

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

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:
·

Goal state after:
case pos
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
hp : p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
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:
·

Goal state after:
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
Module: Mathlib.Analysis.Real.Hyperreal

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

pp: case refine_2
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ coeRingHom s ≤ x

pp: case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ coeRingHom s

Tactic:
·

Goal state after:
case refine_1
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ 0 ≤ ArchimedeanClass.mk x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case mp
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) → ∃ r, q = r * r

pp: case mpr
q : ℚ
hq : 0 ≤ q
⊢ (∃ r, q = r * r) → ∃ y, ↑y = √↑q

Tactic:
·

Goal state after:
case mp
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) → ∃ r, q = r * r
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_2
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ coeRingHom s ≤ x

pp: case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ coeRingHom s

Tactic:
·

Goal state after:
case refine_2
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ coeRingHom s ≤ x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ coeRingHom s

Tactic:
·

Goal state after:
case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ coeRingHom s
Module: Mathlib.Analysis.Real.Hyperreal

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

pp: case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ x < ↑(stdPart x) + ↑y

Tactic:
·

Goal state after:
case refine_1
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ ↑(stdPart x) - ↑y < x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case mpr
q : ℚ
hq : 0 ≤ q
⊢ (∃ r, q = r * r) → ∃ y, ↑y = √↑q

Tactic:
·

Goal state after:
case mpr
q : ℚ
hq : 0 ≤ q
⊢ (∃ r, q = r * r) → ∃ y, ↑y = √↑q
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
·

Goal state after:
case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ x < ↑(stdPart x) + ↑y
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inl
q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

pp: case inr
q : ℚ
hq : q < 0
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
·

Goal state after:
case inl
q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case pos
x : ℝ*
h : ∃ r, x.IsSt r
⊢ Classical.choose h = stdPart x

pp: case neg
x : ℝ*
h : ¬∃ r, x.IsSt r
⊢ 0 = stdPart x

Tactic:
·

Goal state after:
case pos
x : ℝ*
h : ∃ r, x.IsSt r
⊢ Classical.choose h = stdPart x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ¬∃ r, x.IsSt r
⊢ 0 = stdPart x

Tactic:
·

Goal state after:
case neg
x : ℝ*
h : ¬∃ r, x.IsSt r
⊢ 0 = stdPart x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
q : ℚ
hq : q < 0
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
·

Goal state after:
case inr
q : ℚ
hq : q < 0
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfinitePos
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0

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

Tactic:
·

Goal state after:
case refine_1
x : ℝ*
h : x.InfinitePos
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0
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:
·

Goal state after:
case refine_2
x : ℝ*
x✝ : 0 < x ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : 0 < x
hx' : ArchimedeanClass.mk x < 0
⊢ ↑r < x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfiniteNeg
⊢ x < 0 ∧ ArchimedeanClass.mk x < 0

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

Tactic:
·

Goal state after:
case refine_1
x : ℝ*
h : x.InfiniteNeg
⊢ x < 0 ∧ ArchimedeanClass.mk x < 0
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
·

Goal state after:
case refine_2
x : ℝ*
x✝ : x < 0 ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : x < 0
hx' : ArchimedeanClass.mk x < 0
⊢ x < ↑r
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inl
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : C 0 * X + C b ≠ 0
x_is_root : (aeval x) (C 0 * X + C b) = 0
this : ↑0 * x = -↑b
⊢ False

pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False

Tactic:
·

Goal state after:
case inl
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : C 0 * X + C b ≠ 0
x_is_root : (aeval x) (C 0 * X + C b) = 0
this : ↑0 * x = -↑b
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False

Tactic:
·

Goal state after:
case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False

pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0

Tactic:
·

Goal state after:
case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0

Tactic:
·

Goal state after:
case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case pos
x : ℝ*
h : x.Infinite
⊢ (-x).st = -x.st

pp: case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
·

Goal state after:
case pos
x : ℝ*
h : x.Infinite
⊢ (-x).st = -x.st
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
·

Goal state after:
case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case inl
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite

pp: case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite

Tactic:
·

Goal state after:
case inl
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite

Tactic:
·

Goal state after:
case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case hfa
⊢ Antitone fun i ↦ (2 * ↑i + 1)⁻¹

pp: case hf0
⊢ Tendsto (fun i ↦ (2 * ↑i + 1)⁻¹) atTop (𝓝 0)

Tactic:
·

Goal state after:
case hfa
⊢ Antitone fun i ↦ (2 * ↑i + 1)⁻¹
Module: Mathlib.Analysis.Real.Pi.Leibniz

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

Tactic:
·

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

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

pp: case h2
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, x ^ 2 ∈ Set.Iio 1

Tactic:
·

Goal state after:
case h1
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝 1)
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case h2
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, x ^ 2 ∈ Set.Iio 1

Tactic:
·

Goal state after:
case h2
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, x ^ 2 ∈ Set.Iio 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ 1 - z * I ≠ 0

Tactic:
contrapose h₂

Goal state after:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 - z * I = 0
⊢ z = -I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0

Tactic:
·

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0
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 ∨ ¬z.im = 0

pp: case inr
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
ni : ¬z.im = 0
⊢ ¬z.re = ↑(2 * k + 1) * π / 2 ∨ ¬z.im = 0

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 ∨ ¬z.im = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

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

Tactic:
·

Goal state after:
case inr
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
ni : ¬z.im = 0
⊢ ¬z.re = ↑(2 * k + 1) * π / 2 ∨ ¬z.im = 0