mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
by

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

Goal state before:
pp: p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ ↑(p.natDegree.choose i) ≤ ↑(p.natDegree.choose (p.natDegree / 2))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℂ[X]
⊢ p.supNorm ≤ ↑(p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: x : ℝ
n : ℕ
m : ℤ
hxr : x ^ n = ↑m
hv : ¬∃ y, x = ↑y
hnpos : 0 < n
⊢ Irrational x

Tactic:
by

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

Goal state before:
pp: n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ ↑(g.natDegree.choose n) * g.mahlerMeasure ≤ ↑(g.natDegree.choose n) * (g * h).mahlerMeasure

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
f g : A[X]
⊢ (f * g).mapMahlerMeasure v = f.mapMahlerMeasure v * g.mapMahlerMeasure v

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 0 v = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 1 v = 1

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
z : A
⊢ (C z).mapMahlerMeasure v = ‖z‖

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x atTop
⊢ ↑r < x

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x atBot
⊢ x < ↑r

Tactic:
by

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

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x atTop
⊢ ArchimedeanClass.mk x < 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x atBot
⊢ ArchimedeanClass.mk x < 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
h : 0 < x ∧ ArchimedeanClass.mk x < 0
⊢ Germ.Tendsto x atTop

Tactic:
by

Goal state after:
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
⊢ multiplicity (↑p) m % 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: x : ℝ*
h : x < 0 ∧ ArchimedeanClass.mk x < 0
⊢ Germ.Tendsto x atBot

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
h : x.IsSt r
⊢ 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r

Tactic:
by

Goal state after:
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.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝¹ : NormedRing A
p : A[X]
v : A →+* ℂ
inst✝ : NormOneClass A
hv : Isometry ⇑v
hp : p.Monic
⊢ 1 ≤ p.mapMahlerMeasure v

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
h : 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
⊢ x.IsSt r

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
x : ℕ
x✝ : x ∈ p.support
⊢ ‖(map v p).coeff x‖ = ‖p.coeff x‖

Tactic:
simp [hv.norm_map_of_map_zero (map_zero _)]

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
x : ℕ
x✝ : x ∈ p.support
⊢ ‖(map v p).coeff x‖ = ‖p.coeff x‖

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.st = stdPart x

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖
⊢ ‖v (p.coeff n)‖ = ‖(map v p).coeff n‖

Tactic:
by

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

Goal state before:
pp: z : ℤ
hz : 0 ≤ z
⊢ Irrational √↑z ↔ ¬IsSquare z

Tactic:
by

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

Goal state before:
pp: z : ℤ
⊢ Irrational √↑z ↔ ¬IsSquare z ∧ 0 ≤ z

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.Infinitesimal ↔ 0 < ArchimedeanClass.mk x

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Irrational √↑n ↔ ¬IsSquare n

Tactic:
by

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

Goal state before:
pp: ⊢ Irrational √2

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖
hcoeff : ‖v (p.coeff n)‖ = ‖(map v p).coeff n‖
⊢ ‖v (p.coeff n)‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v

Tactic:
hcoeff,

Goal state after:
A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖
hcoeff : ‖v (p.coeff n)‖ = ‖(map v p).coeff n‖
⊢ ‖(map v p).coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑m

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ x ≠ 1

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ Irrational (x + y) → Irrational x ∨ Irrational y

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑(-q) + (↑q + x))

Tactic:
by

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m + x)
⊢ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational (-x)
x✝ : x ∈ Set.range Rat.cast
q : ℚ
hx : ↑q = x
⊢ ↑(-q) = -x

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ Irrational (- -x)

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x - ↑q)

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑q - x)

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational (x - ↑q)
⊢ Irrational (x + ↑(-q))

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational (↑q - x)
⊢ Irrational (↑q + -x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (x - ↑m)
⊢ Irrational (x - ↑↑m)

Tactic:
by

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m - x)
⊢ Irrational (↑↑m - x)

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ Irrational (x * y) → Irrational x ∨ Irrational y

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q * ↑q⁻¹)

Tactic:
by

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑↑m)

Tactic:
by

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑↑m * x)

Tactic:
by

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

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfiniteNeg
hx : x < 0
n : ℕ
⊢ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)| < |ArchimedeanOrder.val (ArchimedeanOrder.of x)|

Tactic:
simpa [abs_of_neg hx, lt_neg] using! h (-n)

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ Irrational x⁻¹⁻¹

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x / ↑q)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑m)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ ↑m ≠ 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational (1 / x)
⊢ Irrational (↑1 / x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x

Tactic:
by

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

Goal state before:
pp: 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
⊢ ↑a * x = -↑b

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.Infinite ↔ ArchimedeanClass.mk x < 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ b = 0

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
⊢ x.IsSt r ↔ Germ.Tendsto x (𝓝 r)

Tactic:
by

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

Goal state before:
pp: x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
hrs : r < s
⊢ x < y

Tactic:
by

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

Goal state before:
pp: x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
⊢ 1 < p.natDegree

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
⊢ Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: m : ℤ
x : ℝ
⊢ Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r s : ℝ
hr : x.IsSt r
hs : x.IsSt s
⊢ r = s

Tactic:
by

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

Goal state before:
pp: m : ℤ
x : ℝ
⊢ Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: q : ℚ
x : ℝ
⊢ Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ x.st = r

Tactic:
rw [st, dif_pos h]

Goal state after:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ Classical.choose h = r
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
⊢ Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: m : ℤ
x : ℝ
⊢ Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ x.st = r

Tactic:
by

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

Goal state before:
pp: m : ℤ
x : ℝ
⊢ Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
by

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

Goal state before:
pp: x : ℝ*
hni : ¬x.Infinite
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.st = sSup {y | ↑y < x}

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ x.IsSt x.st

Tactic:
by

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

Goal state before:
pp: r s : ℝ
⊢ (↑r).IsSt s ↔ (↑s).IsSt r

Tactic:
by

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

Goal state before:
pp: r s t : ℝ
⊢ (↑r).IsSt s → (↑s).IsSt t → (↑r).IsSt t

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
⊢ x.IsSt r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop atTop
⊢ (ofSeq f).InfinitePos

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop atBot
⊢ (ofSeq f).InfiniteNeg

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ ¬(↑r).Infinite

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ (-x).st = -x.st

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
hx : x.Infinitesimal
⊢ (-x).Infinitesimal

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ (x - ↑r).Infinitesimal

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹

Tactic:
rw [infinitePos_iff, infinitesimal_iff]

Goal state after:
x : ℝ*
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0 ↔ 0 < ArchimedeanClass.mk x⁻¹ ∧ 0 < x⁻¹
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x⁻¹⁻¹.Infinitesimal ∧ 0 < x⁻¹⁻¹ ↔ x.Infinitesimal ∧ 0 < x

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x⁻¹⁻¹.Infinitesimal ∧ x⁻¹⁻¹ < 0 ↔ x.Infinitesimal ∧ x < 0

Tactic:
by

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

Goal state before:
pp: x : ℝ*
h : x ≠ 0
⊢ x.Infinitesimal ↔ x⁻¹⁻¹.Infinitesimal

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ*
⊢ x⁻¹.st = x.st⁻¹

Tactic:
by

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

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y

Tactic:
by

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

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
⊢ ↑r < x * y

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: θ : ℝ
⊢ I 0 θ * θ = 2 * sin θ

Tactic:
by

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)
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 * θ) * θ
⊢ Continuous f

Tactic:
by

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

Goal state before:
pp: x✝² x✝¹ : ℕ
x✝ : x✝² < x✝¹
⊢ (2 * ↑x✝¹ + 1)⁻¹ ≤ (2 * ↑x✝² + 1)⁻¹

Tactic:
by

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)
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
⊢ Continuous u₁'

Tactic:
by

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

Goal state before:
pp: ⊢ ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)

Tactic:
by

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)
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₁'
⊢ Continuous v₁'

Tactic:
by

Goal state after: