mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ dist (eval α fR) (eval y fR) ≤ |eval xm (derivative fR)| * dist α y

Tactic:
]

Goal state after:
case refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ dist (eval α fR) (eval y fR) ≤ |eval xm (derivative fR)| * dist α y
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖eval y (derivative fR)‖ ≤ |eval xm (derivative fR)|

Tactic:
]

Goal state after:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖eval y (derivative fR)‖ ≤ |eval xm (derivative fR)|
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ (e - j) • Module.rank (R ⧸ p) (S ⧸ P) = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)

pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥⊥ = 0

Tactic:
]

Goal state after:
case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥⊥ = 0
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_1
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
⊢ p * f.natDegree - 1 ≤ p * f.natDegree - 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval (↑z / (↑a + 1)) fR|

Tactic:
]

Goal state after:
case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval (↑z / (↑a + 1)) fR|
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ 1 ≤ ↑↑(a + 1) ^ f.natDegree * |eval (↑z / ↑↑(a + 1)) fR|

Tactic:
]

Goal state after:
case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ 1 ≤ ↑↑(a + 1) ^ f.natDegree * |eval (↑z / ↑↑(a + 1)) fR|
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥⊤ = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥⊤ = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0

Tactic:
]

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !

pp: case hb
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

pp: case hd
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Tactic:
]

Goal state after:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !

case hb
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

case hd
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ ↑1 < ↑b

Tactic:
]

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ ↑1 < ↑b
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑e * Module.rank (R ⧸ p) (S ⧸ P) = ↑e * Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ 1 / ↑m = 1 / ↑m

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)

Tactic:
]

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
]

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P * finrank (R ⧸ p) (S ⧸ ↑P) = p.ramificationIdx' ↑P * finrank (R ⧸ p) (S ⧸ ↑P)

pp: case hP0
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ ↑P ≠ ⊥

pp: case he
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P ≠ 0

Tactic:
]

Goal state after:
case hP0
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ ↑P ≠ ⊥

case he
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P ≠ 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (k + 1)!) + ↑(m ^ k !) * 1 * ↑(m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Tactic:
]

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (k + 1)!) + ↑(m ^ k !) * 1 * ↑(m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P✝ : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P * p.inertiaDeg' ↑P ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P✝ : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P * p.inertiaDeg' ↑P ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
P✝ : Ideal S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
P : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)

Tactic:
]

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case hbc
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 2 ^ r ≤ ↑b ^ r

Tactic:
]

Goal state after:
case hbc
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 2 ^ r ≤ ↑b ^ r
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1)) * map (algebraMap ℤ ℂ) f ^ p

Tactic:
]

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1)) * map (algebraMap ℤ ℂ) f ^ p
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case calc_1
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ ∑ x ∈ (factors (map f p)).toFinset.attach, e ↑x * p.inertiaDeg' ↑x =
    ∑ P ∈ (factors (map f p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

Tactic:
]

Goal state after:
case calc_1
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ ∑ x ∈ (factors (map f p)).toFinset.attach, e ↑x * p.inertiaDeg' ↑x =
    ∑ P ∈ (factors (map f p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case calc_1
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
P : ↥(factors (map f p)).toFinset
x✝ : P ∈ (factors (map f p)).toFinset.attach
⊢ e ↑P * p.inertiaDeg' ↑P = p.ramificationIdx' ↑P * p.inertiaDeg' ↑P

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n

Tactic:
]

Goal state after:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n

Tactic:
]

Goal state after:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 1)!

Tactic:
]

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 1)!