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

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a.x < 0

pp: case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ a.y

pp: case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.x < 0

pp: case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.y ≤ 0

pp: case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a.y ≤ 0

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a.x < 0

case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ a.y

case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.x < 0

case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.y ≤ 0

case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a.y ≤ 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = 1
⊢ False

pp: case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = -1
⊢ False

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = 1
⊢ False

case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = -1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = Solution₁.y 1
⊢ False

pp: case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = (-1).y
⊢ False

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = Solution₁.y 1
⊢ False

case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = (-1).y
⊢ False
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
⊢ ContinuousAt (⇑(algebraMap (WithVal (valuation K v)) (WithVal (valuation L w)))) 0

Tactic:
ContinuousAt,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
⊢ Filter.Tendsto (⇑(algebraMap (WithVal (valuation K v)) (WithVal (valuation L w)))) (nhds 0)
    (nhds ((algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) 0))
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

pp: case hnsol
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ (Polynomial.aeval a) F ≠ 0

Tactic:
<;>

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

case hnsol
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ (Polynomial.aeval a) F ≠ 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
⊢ v.IsEquiv (inftyValuation K)

Tactic:
refine isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_
  rcases eq_or_ne f 0 with rfl | hf
  · simp
  · have hlt' : 1 < inftyValuation K X := by simp [← exp_zero]
    rw [valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt hf,
      valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt' hf]
    grind [one_le_zpow_iff_right₀]

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

pp: case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
<;>

Goal state after:
case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 ∣ x + y

pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 ∣ x - y

Tactic:
<;>

Goal state after:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 ∣ x + y

m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 ∣ x - y
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
⊢ v.IsUniformizer ↑πᵥ

Tactic:
by
  have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle
  rw [IsUniformizer, ← hv.valueGroup_genLTOne_eq_generator, ← h0.isUnit.unit_spec, Units.val_inj]
  apply LinearOrderedCommGroup.Subgroup.genLTOne_unique
  · rw [← Units.val_lt_val, h0.isUnit.unit_spec, Units.val_one]
    exact valuation_uniformizingPolynomial_lt_one hle
  · ext γ
    simp only [coePolynomial_eq_algebraMap, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq,
      map_eq_zero, Subgroup.mem_zpowers_iff]
    refine ⟨fun ⟨k, hk⟩ ↦ ?_, fun ⟨a, ha, b, hab⟩ ↦ ?_⟩
    · use 1, one_ne_zero, πᵥ ^ k
      simp only [← Units.val_inj, Units.val_zpow_eq_zpow_val] at hk
      simp [← hk]
    · obtain ⟨ka, hka⟩ := exists_zpow_uniformizingPolynomial hle ha
      obtain ⟨kb, hkb⟩ := exists_zpow_uniformizingPolynomial hle (f := b) (by aesop)
      rw [MonoidWithZeroHom.coe_ofClass, hka, hkb] at hab
      use kb - ka
      have : v ↑πᵥ ^ ka ≠ 0 := zpow_ne_zero _ h0
      simp [zpow_sub, ← Units.val_inj, ← coePolynomial_eq_algebraMap, field, ← hab]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: case a
x : ℤ[i]
⊢ (toComplex x).re = { re := ↑x.re, im := ↑x.im }.re

pp: case a
x : ℤ[i]
⊢ (toComplex x).im = { re := ↑x.re, im := ↑x.im }.im

Tactic:
<;>

Goal state after:
case a
x : ℤ[i]
⊢ (toComplex x).re = { re := ↑x.re, im := ↑x.im }.re

case a
x : ℤ[i]
⊢ (toComplex x).im = { re := ↑x.re, im := ↑x.im }.im
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ toComplex x = 0 ↔ x = 0

Tactic:
← toComplex_zero,

Goal state after:
x : ℤ[i]
⊢ toComplex x = toComplex 0 ↔ x = 0
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: case a
x y : ℤ[i]
⊢ (toComplex x / toComplex y - toComplex (x / y)).re =
    (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re

pp: case a
x y : ℤ[i]
⊢ (toComplex x / toComplex y - toComplex (x / y)).im =
    (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).im

Tactic:
<;>

Goal state after:
case a
x y : ℤ[i]
⊢ (toComplex x / toComplex y - toComplex (x / y)).re =
    (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re

case a
x y : ℤ[i]
⊢ (toComplex x / toComplex y - toComplex (x / y)).im =
    (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).im
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
hy : y ≠ 0
⊢ ¬toComplex y = 0

Tactic:
← toComplex_zero,

Goal state after:
x y : ℤ[i]
hy : y ≠ 0
⊢ ¬toComplex y = toComplex 0
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: case re
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ (↑k ^ 2 + 1).re = ({ re := ↑k, im := 1 } * { re := ↑k, im := -1 }).re

pp: case im
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ (↑k ^ 2 + 1).im = ({ re := ↑k, im := 1 } * { re := ↑k, im := -1 }).im

Tactic:
<;>

Goal state after:
case re
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ (↑k ^ 2 + 1).re = ({ re := ↑k, im := 1 } * { re := ↑k, im := -1 }).re

case im
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ (↑k ^ 2 + 1).im = ({ re := ↑k, im := 1 } * { re := ↑k, im := -1 }).im
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = (↑p).norm

Tactic:
hpab

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = norm (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
P : Ideal S
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : (Submodule.quotientRel P) x y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    rw [Submodule.quotientRel_def] at h ⊢
    simp only [map_mul, LinearMap.mem_range]
    refine ⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem h)⟩, ?_⟩
    ext
    rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.coe_sub, Subtype.coe_mk,
      Subtype.coe_mk, map_mul, map_sub, mul_sub]

Goal state after:
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
hfp : NeZero e
inst✝¹ : IsDedekindDomain S
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
h :
  (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' x) =
    (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' y)
⊢ Quotient.mk'' x = Quotient.mk'' y

Tactic:
have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1) := Ideal.pow_le_pow_right hi

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.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
h :
  (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' x) =
    (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' y)
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
⊢ Quotient.mk'' x = Quotient.mk'' y
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h₁
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp s.re ≤ c₁ ^ p

pp: case hbc
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp ‖s‖ ≤ c₂ ^ p

pp: case h₂
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ ‖s‖ ≤ c₃ ^ p

Tactic:
<;>

Goal state after:
case h₁
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp s.re ≤ c₁ ^ p

case hbc
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp ‖s‖ ≤ c₂ ^ p

case h₂
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ ‖s‖ ≤ c₃ ^ p
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h
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'
⊢ ∃ n,
    ¬↑p ∣ n ∧
      ∃ gp,
        gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ},
            r ∈ f.aroots ℂ →
              ‖↑n * 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:
use f.eval 0 ^ p + p * gp'.eval 0

Goal state after:
case h
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'
⊢ ¬↑p ∣ eval 0 f ^ p + ↑p * eval 0 gp' ∧
    ∃ gp,
      gp.natDegree ≤ p * f.natDegree - 1 ∧
        ∀ {r : ℂ},
          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)!
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case mul
m n : ℕ
hm : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * n

Tactic:
rcases hm with ⟨a, b, c, d, rfl⟩

Goal state after:
case mul
n : ℕ
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
a b c d : ℕ
⊢ ∃ a_1 b_1 c_1 d_1, a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * n
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)

Tactic:
simpa only [(· ∘ ·), neg_sub, one_div] using
      ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_natCast_atTop_atTop).eventually
        (eventually_gt_atTop C)

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (Units.coeHom (ZMod p)) (-1) = -1

Tactic:
Units.coeHom_apply,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(-1) = -1
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: case refine_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a ↦ ↑a ^ (1 - r)

pp: case refine_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a ↦ ↑a ^ (-r)

Tactic:
<;>

Goal state after:
case refine_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a ↦ ↑a ^ (1 - r)

case refine_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a ↦ ↑a ^ (-r)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: case refine_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ 1 - r < -1

pp: case refine_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ -r < -1

Tactic:
<;>

Goal state after:
case refine_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ 1 - r < -1

case refine_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ -r < -1
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ B.extent

Tactic:
← lowerBounds_right

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ lowerBounds B.right
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), sSup c a a

pp: case refine_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1

pp: case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), sSup c a b → sSup c b a → a = b

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), sSup c a a

case refine_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1

case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), sSup c a b → sSup c b a → a = b