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

Goal state before:
pp: case e'_5
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ i₁ = e.symm (e i₁)

pp: case e'_6
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ i₀ = e.symm (e i₀)

Tactic:
<;>

Goal state after:
case e'_5
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ i₁ = e.symm (e i₁)

case e'_6
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ i₀ = e.symm (e i₀)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg.step
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ¬(p = 2 ∧ m = 2) → m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)

Tactic:
by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case e'_5
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ k = e.symm (e k)

pp: case e'_6
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ k = e.symm (e k)

Tactic:
<;>

Goal state after:
case e'_5
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ k = e.symm (e k)

case e'_6
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ k = e.symm (e k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = Λ 0 + ∑ x ∈ Ioc 0 ⌊x⌋₊, Λ x

pp: x : ℝ
⊢ 0 ≤ ⌊x⌋₊

Tactic:
<;>

Goal state after:
x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = Λ 0 + ∑ x ∈ Ioc 0 ⌊x⌋₊, Λ x

x : ℝ
⊢ 0 ≤ ⌊x⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    (if Nat.Prime 0 then log ↑0 else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0

pp: x : ℝ
⊢ 0 ≤ ⌊x⌋₊

Tactic:
<;>

Goal state after:
x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    (if Nat.Prime 0 then log ↑0 else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0

x : ℝ
⊢ 0 ≤ ⌊x⌋₊
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
have : j = b.natDegree - (natDegree b - j.succ).succ := by
    rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this✝ : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
this : j = b.natDegree - (b.natDegree - j.succ).succ
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
⊢ 0 < ↑(cardPowDegree b) * ε

Tactic:
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hx
x : ℝ
hx : 0 ≤ x
⊢ 0 < ↑(primorial ⌊x⌋₊)

pp: case hxy
x : ℝ
hx : 0 ≤ x
⊢ ↑(primorial ⌊x⌋₊) ≤ 4 ^ ⌊x⌋₊

Tactic:
<;>

Goal state after:
case hx
x : ℝ
hx : 0 ≤ x
⊢ 0 < ↑(primorial ⌊x⌋₊)

case hxy
x : ℝ
hx : 0 ≤ x
⊢ ↑(primorial ⌊x⌋₊) ≤ 4 ^ ⌊x⌋₊
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ (Finset.image (fun x ↦ ↑x) (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ)).max' ⋯ < y

Tactic:
apply (Finset.max'_lt_iff _ (him.image _)).mpr

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ ∀ y_1 ∈ Finset.image (fun x ↦ ↑x) (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ), y_1 < y
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(A i₁ % b - A i₀ % b).natDegree = (A i₁ % b - A i₀ % b).degree

Tactic:
degree_eq_natDegree h'

Goal state after:
case e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(A i₁ % b - A i₀ % b).natDegree = ↑(A i₁ % b - A i₀ % b).natDegree
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < ↑(cardPowDegree b) * ε

Tactic:
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
k : ℕ
hk : 0 < k
⊢ ∑ v ∈ Ico 1 0, ↑v ^ (2 * k) = ∑ v ∈ range 0, ↑v ^ (2 * k)

pp: case succ
k : ℕ
hk : 0 < k
n✝ : ℕ
⊢ ∑ v ∈ Ico 1 (n✝ + 1), ↑v ^ (2 * k) = ∑ v ∈ range (n✝ + 1), ↑v ^ (2 * k)

Tactic:
<;>

Goal state after:
case zero
k : ℕ
hk : 0 < k
⊢ ∑ v ∈ Ico 1 0, ↑v ^ (2 * k) = ∑ v ∈ range 0, ↑v ^ (2 * k)

case succ
k : ℕ
hk : 0 < k
n✝ : ℕ
⊢ ∑ v ∈ Ico 1 (n✝ + 1), ↑v ^ (2 * k) = ∑ v ∈ range (n✝ + 1), ↑v ^ (2 * k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log 2 ≤ log x

pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 0 < log 2

Tactic:
<;>

Goal state after:
case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log 2 ≤ log x

x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 0 < log 2
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case mp
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := ⋯
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FunctionField F K → FiniteDimensional Ft K

pp: case mpr
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := ⋯
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FiniteDimensional Ft K → FunctionField F K

Tactic:
<;>

Goal state after:
case mp
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := ⋯
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FunctionField F K → FiniteDimensional Ft K

case mpr
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := ⋯
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FiniteDimensional Ft K → FunctionField F K
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖↑x.zmodRepr‖ = 1 → ‖x‖ = 1

pp: case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖x‖ = 1 → ‖↑x.zmodRepr‖ = 1

Tactic:
<;>

Goal state after:
case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖↑x.zmodRepr‖ = 1 → ‖x‖ = 1

case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖x‖ = 1 → ‖↑x.zmodRepr‖ = 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
h : ‖↑x.zmodRepr‖ = 1
⊢ ‖x‖ = 1

pp: case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
h : ‖x‖ = 1
⊢ ‖↑x.zmodRepr‖ = 1

Tactic:
<;>

Goal state after:
case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
h : ‖↑x.zmodRepr‖ = 1
⊢ ‖x‖ = 1

case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
h : ‖x‖ = 1
⊢ ‖↑x.zmodRepr‖ = 1
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) (b' • (r • a - q * b))) = abv ((Algebra.norm R) ((r • a' - b' • q) * b))

Tactic:
smul_sub b',

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) (b' • r • a - b' • (q * b))) = abv ((Algebra.norm R) ((r • a' - b' • q) * b))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat 0 < p
⊢ OfNat.ofNat 0 = ↑(OfNat.ofNat 0)

pp: case succ.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat (0 + 1) < p
⊢ OfNat.ofNat (0 + 1) = ↑(OfNat.ofNat (0 + 1))

pp: case succ.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat (n + 1 + 1) < p
⊢ OfNat.ofNat (n + 1 + 1) = ↑(OfNat.ofNat (n + 1 + 1))

Tactic:
<;>

Goal state after:
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat 0 < p
⊢ OfNat.ofNat 0 = ↑(OfNat.ofNat 0)

case succ.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat (0 + 1) < p
⊢ OfNat.ofNat (0 + 1) = ↑(OfNat.ofNat (0 + 1))

case succ.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat (n + 1 + 1) < p
⊢ OfNat.ofNat (n + 1 + 1) = ↑(OfNat.ofNat (n + 1 + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hx_pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ 0 < z

pp: case hx
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ z ≠ 1

Tactic:
<;>

Goal state after:
case hx_pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ 0 < z

case hx
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ z ≠ 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ 0 < z

pp: case refine_2
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ z ≠ 1

Tactic:
<;>

Goal state after:
case refine_1
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ 0 < z

case refine_2
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ z ≠ 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
n : ℕ
x✝ : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ log ↑n = log ↑n * a n

pp: case neg
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
n : ℕ
x✝ : n ∈ Icc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ 0 = log ↑n * a n

Tactic:
<;>

Goal state after:
case pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
n : ℕ
x✝ : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ log ↑n = log ↑n * a n

case neg
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
n : ℕ
x✝ : n ∈ Icc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ 0 = log ↑n * a n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hd
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 0 < log a ^ 2

pp: case ha
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 0 ≤ log a

Tactic:
<;>

Goal state after:
case hd
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 0 < log a ^ 2

case ha
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 0 ≤ log a
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case one_lt_a
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ 1 < a

pp: case one_lt_b
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ 1 < b

Tactic:
<;>

Goal state after:
case one_lt_a
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ 1 < a

case one_lt_b
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ 1 < b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ x - √x ≤ x

pp: case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ √x - 2 ≤ √x

Tactic:
<;>

Goal state after:
case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ x - √x ≤ x

case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ √x - 2 ≤ √x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hab.one_lt_a
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < 2

pp: case hab.one_lt_b
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x

Tactic:
<;>

Goal state after:
case hab.one_lt_a
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < 2

case hab.one_lt_b
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc.one_lt_a
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x

pp: case hbc.one_lt_b
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < x

Tactic:
<;>

Goal state after:
case hbc.one_lt_a
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x

case hbc.one_lt_b
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ (traceMatrix A ⇑(b.reindex f)).det = discr A ⇑b

Tactic:
traceMatrix_reindex,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ ((reindex f f) (traceMatrix A ⇑b)).det = discr A ⇑b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 1 < x
⊢ x ≠ 0

pp: x : ℝ
a✝ : 1 < x
⊢ x ≠ 1

pp: x : ℝ
a✝ : 1 < x
⊢ x ≠ -1

Tactic:
<;>

Goal state after:
x : ℝ
a✝ : 1 < x
⊢ x ≠ 0

x : ℝ
a✝ : 1 < x
⊢ x ≠ 1

x : ℝ
a✝ : 1 < x
⊢ x ≠ -1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Real.sqrt =o[atTop] fun x ↦ x / log x ^ 2

Tactic:
apply isLittleO_mul_iff_isLittleO_div _ |>.mp
  · conv => arg 2; ext; rw [mul_comm]
    apply isLittleO_mul_iff_isLittleO_div _ |>.mpr
    · simp_rw [div_sqrt, sqrt_eq_rpow, ← rpow_two]
      apply isLittleO_log_rpow_rpow_atTop _ (by norm_num)
    filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx
  filter_upwards [eventually_gt_atTop 1] with x _
  apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩ <;> linarith

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ c - (toZMod c).cast ∈ maximalIdeal ℤ_[p]

Tactic:
apply toZMod_spec

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
x : ℝ
a✝ : 4 ≤ x
⊢ 1 < 2

pp: case refine_2
x : ℝ
a✝ : 4 ≤ x
⊢ 1 < x

Tactic:
<;>

Goal state after:
case refine_1
x : ℝ
a✝ : 4 ≤ x
⊢ 1 < 2

case refine_2
x : ℝ
a✝ : 4 ≤ x
⊢ 1 < x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ¬↑p ≤ √x
⊢ log √x ≤ log ↑p + 0

Tactic:
have : log √x < log p := log_lt_log (by positivity) (not_le.mp h)

Goal state after:
case neg
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ¬↑p ≤ √x
this : log √x < log ↑p
⊢ log √x ≤ log ↑p + 0
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case neg
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous
    (⇑{ toFun := fun g ↦ 1, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits ∘ ⇑(MulSemiringAction.toRingAut Gal(L/K) L))

Tactic:
exact continuous_const (y := 1)

Goal state after: