mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
⊢ stdPart x = r

Tactic:
]

Goal state after:
x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
⊢ stdPart x = r
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
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

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

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.Polynomial.MahlerMeasure

Goal state before:
pp: case hbc
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure

Tactic:
]

Goal state after:
case hbc
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

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

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: case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x

Tactic:
]

Goal state after:
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x
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

Tactic:
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
    simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
      (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv

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

Goal state before:
pp: r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ ↑r < ofSeq f

Tactic:
]

Goal state after:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ ↑r < ofSeq f
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ)) atBot
⊢ ofSeq f < ↑r

Tactic:
]

Goal state after:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ)) atBot
⊢ ofSeq f < ↑r
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
case inr
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ 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: case inr
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : 0 ≠ 0
this : y ≠ 0
⊢ False

Tactic:
]

Goal state after:
case inr
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : 0 ≠ 0
this : y ≠ 0
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
h : 0 < ofSeq f ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in ↑(hyperfilter ℕ), b ≤ f a

Tactic:
]

Goal state after:
f : ℕ → ℝ
h : 0 < ofSeq f ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in ↑(hyperfilter ℕ), b ≤ f a
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: f : ℕ → ℝ
h : ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in ↑(hyperfilter ℕ), f a ≤ b

Tactic:
]

Goal state after:
f : ℕ → ℝ
h : ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in ↑(hyperfilter ℕ), f a ≤ b
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
hv_ne : v p.leadingCoeff ≠ 0
hv_norm : ‖v p.leadingCoeff‖ = ‖p.leadingCoeff‖
⊢ (map v p).mahlerMeasure ≤ (map v p).mahlerMeasure

Tactic:
]

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

Goal state before:
pp: case mp
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ↑q = ↑q

Tactic:
]

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 ≤ 1

Tactic:
]

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

Goal state before:
pp: x : ℝ*
⊢ (if h : ∃ r, x.IsSt r then Classical.choose h else 0) = stdPart x

Tactic:
]

Goal state after:
x : ℝ*
⊢ (if h : ∃ r, x.IsSt r then Classical.choose h else 0) = stdPart x
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

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

Tactic:
]

Goal state after:
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ p.support, ‖(map v p).coeff n‖ = ∑ n ∈ p.support, ‖p.coeff n‖
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℝ*
⊢ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.mk x ≠ 0 ↔ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.mk x ≠ 0

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑↑m
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational x

Tactic:
]

Goal state after:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
m : ℤ
h : Irrational (↑↑m + x)
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
by
  rw [← cast_intCast] at h
  exact h.of_ratCast_add m

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

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

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‖
⊢ ↑(p.natDegree.choose n) * (map v p).mahlerMeasure ≤ ↑(p.natDegree.choose n) * (map v p).mahlerMeasure

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
m : ℤ
h : Irrational (x - ↑m)
⊢ Irrational (x - ↑m)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
m : ℤ
h : Irrational (↑m - x)
⊢ Irrational (↑m - x)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational x

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑m)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑m * x)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ m ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q⁻¹)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ m ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational (1 / x)
⊢ Irrational (1 / x)
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
h : Irrational 1
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
]

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

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

Goal state before:
pp: r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g

Tactic:
]

Goal state after:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
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

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: r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s

Tactic:
]

Goal state after:
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
⊢ q ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x

Tactic:
]

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

Goal state before:
pp: m : ℤ
x : ℝ
⊢ m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x

Tactic:
]

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x

Tactic:
]

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

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

Tactic:
]

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 : ℝ
⊢ ¬q = 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x

Tactic:
]

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

Goal state before:
pp: x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
]

Goal state after:
x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ x.IsSt (sSup {y | ↑y < x})
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = sSup {y | ↑y < x}

Tactic:
]

Goal state after:
x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = sSup {y | ↑y < x}
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

Goal state after:
x : ℝ*
⊢ stdPart x = sSup {y | ↑y < x}
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

Goal state after:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ x.IsSt r
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
⊢ s = r ↔ s = r

Tactic:
]

Goal state after:
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: r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
]

Goal state after:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ 0 < ofSeq f ∧ ArchimedeanClass.mk (ofSeq f) < 0

Tactic:
]

Goal state after:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ 0 < ofSeq f ∧ ArchimedeanClass.mk (ofSeq f) < 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ)) atBot
⊢ ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0

Tactic:
]

Goal state after:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ)) atBot
⊢ ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s

Tactic:
]

Goal state after:
r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case pos
x : ℝ*
h : x.Infinite
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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⁻¹.Infinitesimal ∧ x⁻¹ < 0 ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
by
  simp [st_eq]

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
⊢ 0 < r₁ ∧ ↑r₁ ≤ y

Tactic:
]

Goal state after:
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
⊢ 0 < r₁ ∧ ↑r₁ ≤ y
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₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y

Tactic:
]

Goal state after:
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₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

Goal state after:
x y : ℝ*
⊢ x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos
Module: Mathlib.Analysis.Real.Hyperreal

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

Tactic:
]

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos
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.Irrational

Goal state before:
pp: θ : ℝ
⊢ θ * ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ 0 * cos (x * θ) = 2 * sin θ

Tactic:
]

Goal state after:
θ : ℝ
⊢ θ * ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ 0 * cos (x * θ) = 2 * sin θ
Module: Mathlib.Analysis.Real.Pi.Irrational

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

Tactic:
]

Goal state after:
θ : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.Real.Pi.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 ^ 2))

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 ^ 2))
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
⊢ ∃ v ∈ 𝓝[<] 1, ∀ y ∈ v, y ^ 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
⊢ ∃ v ∈ 𝓝[<] 1, ∀ y ∈ v, y ^ 2 ∈ Set.Iio 1
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))

Tactic:
]

Goal state after:
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Tactic:
]

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₂ : z ≠ -I
h₁ : I = z
⊢ z = I

Tactic:
]

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

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

Tactic:
]

Goal state after:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I
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)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo (-1) 1
⊢ x✝¹ ∈ Set.Ioo (-1) 1

Tactic:
]

Goal state after:
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✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo (-1) 1
⊢ x✝¹ ∈ Set.Ioo (-1) 1