mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
ha : IsUnit a
⊢ orderOf a = p ^ n

Tactic:
exact orderOf_one_add_prime hp hp2 n

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : m✝ < n
⊢ (coeff (m✝ + single i 1)) f * (↑(m✝ i) + 1) =
    (if m✝ + single i 1 < n + single i 1 then (coeff (m✝ + single i 1)) f else 0) * (↑(m✝ i) + 1)

Tactic:
if_pos (add_lt_add_left h _)

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : m✝ < n
⊢ (coeff (m✝ + single i 1)) f * (↑(m✝ i) + 1) = (coeff (m✝ + single i 1)) f * (↑(m✝ i) + 1)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) → n = p ^ n.factorization p

Tactic:
rintro ⟨q, m, hq, -, rfl⟩

Goal state after:
case neg.refine_2
p : ℕ
hp : Nat.Prime p
odd : Odd p
q m : ℕ
hq : Nat.Prime q
hn : Odd (q ^ m)
hn0 : q ^ m ≠ 0
h1 : q ^ m ≠ 1
dvd : p ∣ q ^ m
hnp : ¬q ^ m = p ^ (q ^ m).factorization p
⊢ q ^ m = p ^ (q ^ m).factorization p
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ bernoulli n = ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))

Tactic:
bernoulli

Goal state after:
n : ℕ
⊢ ∑ i ∈ range (n + 1), (monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i)) =
    ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 (k + n) | Prime x}) ≤ #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
←
        Ico_union_Ico_eq_Ico (zero_le k) le_self_add,

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 k ∪ Ico k (k + n) | Prime x}) ≤ #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : b < 1
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
Nat.floor_eq_zero.mpr hb,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : b < 1
⊢ ∑ x ∈ Icc 0 0, f ↑x * c x = f b * ∑ x ∈ Icc 0 0, c x - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Goal state before:
pp: case refine_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / ((algebraMap ℤ ℝ) |b| * ε) < ↑↑⌈1 / ε⌉₊

Tactic:
eq_intCast,

Goal state after:
case refine_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / (↑|b| * ε) < ↑↑⌈1 / ε⌉₊
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.degree
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
rw [coeff_sub, sub_eq_zero]

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.degree
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n p : ℕ
h : p ∈ n.primesLE
⊢ p ∈ n.lcmUpto.primeFactors

Tactic:
· refine Prime.mem_primeFactors (prime_of_mem_primesLE h) (dvd_lcm ?_) <| lcmUpto_ne_zero n
    exact mem_Icc.mpr ⟨(prime_of_mem_primesLE h).one_le, le_of_mem_primesLE h⟩

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

Goal state before:
pp: case neg
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₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
obtain ⟨i₀, i₁, i_ne, deg_lt⟩ := exists_approx_polynomial_aux le_rfl b (fun i => A i % b) fun i =>
    EuclideanDomain.mod_lt (A i) hb

Goal state after:
case neg
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)⌉₊)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
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]
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
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ log ↑(↑(Fintype.card Fq) ^ (A i₁ % b - A i₀ % b).natDegree) <
    log ((algebraMap ℤ ℝ) (↑(Fintype.card Fq) ^ b.natDegree) * ε)

Tactic:
eq_intCast,

Goal state after:
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
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ log ↑(↑(Fintype.card Fq) ^ (A i₁ % b - A i₀ % b).natDegree) < log (↑(↑(Fintype.card Fq) ^ b.natDegree) * ε)
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ ↑(normBound abv bS) *
      ((algebraMap ℤ ℝ) (abv b) * ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))) ^ ↑(Fintype.card ι) ≤
    ↑(abv b) ^ ↑(Fintype.card ι)

Tactic:
eq_intCast,

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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ ↑(normBound abv bS) * (↑(abv b) * ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))) ^ ↑(Fintype.card ι) ≤
    ↑(abv b) ^ ↑(Fintype.card ι)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ↑(f 0) = 0

Tactic:
rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]

Goal state after:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 0 - ↑(f 0) ∈ Ideal.span {↑v}

case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 0 - ↑0 ∈ Ideal.span {↑v}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0

Tactic:
rw [← sub_zero x] at h

Goal state after:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x✝ : ℤ_[p]
⊢ x✝ - ↑(x✝.appr n) ∈ Ideal.span {↑(p ^ n)}

Tactic:
rw [Nat.cast_pow]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x✝ : ℤ_[p]
⊢ x✝ - ↑(x✝.appr n) ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0

Tactic:
rw [← sub_zero x] at h

Goal state after:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
let E := AlgebraicClosure L

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε

Tactic:
dsimp [nthHomSeq]

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom f (r + s) j) - (↑(nthHom f r j) + ↑(nthHom f s j))) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε

Tactic:
dsimp [nthHomSeq]

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom f (r * s) j) - ↑(nthHom f r j) * ↑(nthHom f s j)) < ε
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this✝ : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
this : (algebraMap ℤ ℚ) (r * r') = 1
⊢ r * r' = 1

Tactic:
rw [← map_one (algebraMap ℤ ℚ)] at this

Goal state after:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this✝ : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
this : (algebraMap ℤ ℚ) (r * r') = (algebraMap ℤ ℚ) 1
⊢ r * r' = 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (toZModPow n) ((lift f_compat) r) - (toZModPow n) ↑((f n) r).val = 0

Tactic:
← map_sub,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (toZModPow n) ((lift f_compat) r - ↑((f n) r).val) = 0
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inr
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = (-1) ^ (p ^ k * (p - 1) / 2)

Tactic:
have hpo : Odd p := hp.out.odd_of_ne_two hp2

Goal state after:
case e_a.inr
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = (-1) ^ (p ^ k * (p - 1) / 2)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ 1 ≤ p ^ k * (2 * a)

Tactic:
← ha

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ 1 ≤ p ^ k * (p - 1)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Tactic:
exact nonnegg_neg_pos.2 (sqLe_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
by
    refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_add _ _ _).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_assoc]
    apply xn_modEq_x2n_add

Goal state after:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ -1 + (↑n + 1) ≤ (ξ * ↑m - ↑⌊ξ * ↑m⌋) * (↑n + 1)

Tactic:
simpa only [neg_add_cancel_comm_assoc] using! hf'

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
ψ : Mˣ →* Rˣ
hψ : ψ.domRestrict N.units = χ.toUnitHom.comp ↑N.unitsEquivUnitsType
x✝ : (↥N)ˣ
⊢ (domRestrict N (ofUnitHom ψ)) ↑x✝ = χ ↑x✝

Tactic:
domRestrict_ofUnitHom

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
ψ : Mˣ →* Rˣ
hψ : ψ.domRestrict N.units = χ.toUnitHom.comp ↑N.unitsEquivUnitsType
x✝ : (↥N)ˣ
⊢ (ofUnitHom ((ψ.domRestrict N.units).comp ↑N.unitsEquivUnitsType.symm)) ↑x✝ = χ ↑x✝
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inl
k : ℕ
hk0 : 0 < k
⊢ 0 ^ k = 0

Tactic:
exact zero_pow hk0.ne'

Goal state after:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = ξ.convergent 0

Tactic:
rw [convergent_zero, Rat.intCast_inj, eq_comm, floor_eq_iff]

Goal state after:
case h
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u ≤ ξ ∧ ξ < ↑u + 1
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = (∏' (p : Primes), f ↑p) * ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 2))

Tactic:
tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf

Goal state after:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 1)) = (∏' (p : Primes), f ↑p) * ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 2))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ fract ξ ≤ 1 ∧ (fract ξ)⁻¹ < 1 + 1

Tactic:
one_add_one_eq_two,

Goal state after:
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ fract ξ ≤ 1 ∧ (fract ξ)⁻¹ < 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ↑n ^ k * |rexp (-π * ((↑n + a) ^ 2 * t))| ≤
    ↑n ^ k * rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t))

Tactic:
abs_exp

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ↑n ^ k * rexp (-π * ((↑n + a) ^ 2 * t)) ≤ ↑n ^ k * rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_1
z τ : ℂ
hτ : 0 < τ.im
⊢ Summable fun x ↦ jacobiTheta₂_term x z τ

Tactic:
refine (summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded ?_
    simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hτ le_rfl le_rfl

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-(π * q i) * t))) (?m.122 t)

Tactic:
by simpa using hF

Goal state after: