mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f1 f2 : L.BoundedFormula α n✝
h1 : ∀ {xs : Fin n✝ → M}, f1.toPrenex.Realize v xs ↔ f1.Realize v xs
h2 : ∀ {xs : Fin n✝ → M}, f2.toPrenex.Realize v xs ↔ f2.Realize v xs
xs✝ : Fin n✝ → M
⊢ f1.toPrenex.Realize v xs✝ → f2.toPrenex.Realize v xs✝ ↔ (f1 ⟹ f2).Realize v xs✝

Tactic:
realize_imp,

Goal state after:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f1 f2 : L.BoundedFormula α n✝
h1 : ∀ {xs : Fin n✝ → M}, f1.toPrenex.Realize v xs ↔ f1.Realize v xs
h2 : ∀ {xs : Fin n✝ → M}, f2.toPrenex.Realize v xs ↔ f2.Realize v xs
xs✝ : Fin n✝ → M
⊢ f1.toPrenex.Realize v xs✝ → f2.toPrenex.Realize v xs✝ ↔ f1.Realize v xs✝ → f2.Realize v xs✝
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case rel
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (RelMap R fun i ↦ Term.realize (Sum.elim v xs) (ts i)) → RelMap R fun i ↦ f (Term.realize (Sum.elim v xs) (ts i))

Tactic:
exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm ((inclusion ⋯) x))

Tactic:
g.toEquiv.apply_symm_apply,

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = (inclusion ⋯) x
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun b ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
⊢ cmp a ↑(G b) = cmp (↑(F a)) b

Tactic:
rcases (F a).prop with ⟨f, hf, ha⟩
      rcases (G b).prop with ⟨g, hg, hb⟩
      rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
      exact m.prop (a, _) (fm ha) (_, b) (gm hb)

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «0»
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}

pp: case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}

Tactic:
· exact admissible_A' q r

Goal state after:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ d ∈ n.divisors, ↑(μ d) * Real.log ↑d = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)

Tactic:
rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self,
    moebius_mul_coe_zeta]

Goal state after:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ↑(1 n) * Real.log ↑n = 0
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ constantCoeff ((⇑(d⁄dX R))^[n] f) = ↑n ! * (coeff n) f

Tactic:
by
  simpa using coeff_iterate_derivative f n 0

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff (n + 1)) (g ^ d) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))

Tactic:
coeff_subst' hg

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff (n + 1)) (g ^ d) =
    ∑ᶠ (d : ℕ), (coeff d) ↑((trunc (m + 1)) f) • (coeff (n + 1)) (g ^ d)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ n ! = 0

Tactic:
cast_eq_zero.1 h

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ioo 0 n)

Tactic:
by
  ext p
  simp +contextual [primesBelow_eq_filter_range, Nat.Prime.pos]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ x ∈ range n, (↑n + 1) * (↑(n.choose x) / (↑n - ↑x + 1)) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x

Tactic:
refine sum_congr rfl fun k hk => ?_

Goal state after:
case succ
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) * bernoulli' k = ↑(n.succ.choose k) * bernoulli' k
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case pos
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h✝ : n = 1
h : (coeff n) (B - (rescale (-1)) B) = 1
⊢ -bernoulli' n = bernoulli' n

Tactic:
simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h✝ : ¬n = 1
h : (coeff n) (B - (rescale (-1)) B) = 0
⊢ -bernoulli' n = bernoulli' n

Tactic:
simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 2 ^ ↑(9 + 10 * 32) ≤ 2 ^ (2 * (512 / 3))

pp: case refine_2.hx
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 0 ≤ 2

Tactic:
on_goal 1 => apply rpow_le_rpow_of_exponent_le

Goal state after:
case refine_2.hx
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 1 ≤ 2

case refine_2.hyz
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ ↑(9 + 10 * 32) ≤ 2 * (512 / 3)

case refine_2.hx
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 0 ≤ 2
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf.inl
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : ¬Nat.Prime x
⊢ x ^ n.centralBinom.factorization x = 1

pp: case hf.inr
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
· rw [factorization_eq_zero_of_not_prime n.centralBinom h, Nat.pow_zero]

Goal state after:
case hf.inr
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: 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
⊢ j = b.natDegree - (b.natDegree.succ - j.succ)

Tactic:
Nat.succ_sub_succ,

Goal state after:
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
⊢ j = b.natDegree - (b.natDegree - j)
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
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
set y' : ℤ := Finset.max' _ him with y'_def

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' : ℤ := (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
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hx
x : ℝ
h : 1 ≤ x
⊢ 0 < ↑⌊x⌋₊

Tactic:
exact_mod_cast lt_of_add_one_le <| (one_le_floor_iff x).mpr h

Goal state after:
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'
⊢ ↑y' < y

Tactic:
y'_def,

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' : ℤ := (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 k ↦ abv ((bS.repr a) k)) Finset.univ).max' him) < y
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case mpr
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
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ (distinctElems bS adm) i - (distinctElems bS adm) j ≠ 0

Tactic:
rw [Ne, sub_eq_zero]

Goal state after:
case mpr
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
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬(distinctElems bS adm) i = (distinctElems bS adm) j
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
x✝² : ℕ
hk : x✝² ∈ Icc 1 N
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑x✝²)⌋₊ | Nat.Prime p}
⊢ x✝² ≠ 0

Tactic:
linarith [mem_Icc.mp hk]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ 1 ≤ ‖↑↑r.den‖

Tactic:
apply ge_of_eq

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ‖↑↑r.den‖ = 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‖ < ‖↑x.zmodRepr‖
h : ‖↑x.zmodRepr‖ = 1
⊢ ‖x‖ = ‖↑x.zmodRepr‖

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

Tactic:
· exact norm_eq_of_norm_sub_lt_right this

Goal state after:
case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < ‖x‖
h : ‖x‖ = 1
⊢ ‖↑x.zmodRepr‖ = ‖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
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ?m.295 ≠ 0

Tactic:
exact mt Ideal.span_singleton_eq_bot.mp b_ne_zero

Goal state after:
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✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
⊢ ∃ J, mk0 I = mk0 J ∧ (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ ↑J

Tactic:
by
  set M := ∏ m ∈ finsetApprox bS adm, m
  have hM : algebraMap R S M ≠ 0 := prod_finsetApprox_ne_zero bS adm
  obtain ⟨b, b_mem, b_ne_zero, b_min⟩ := exists_min abv I
  suffices Ideal.span {b} ∣ Ideal.span {algebraMap _ _ M} * I.1 by
    obtain ⟨J, hJ⟩ := this
    refine ⟨⟨J, ?_⟩, ?_, ?_⟩
    · rw [mem_nonZeroDivisors_iff_ne_zero]
      rintro rfl
      rw [Ideal.zero_eq_bot, Ideal.mul_bot] at hJ
      exact hM (Ideal.span_singleton_eq_bot.mp (I.2.2 _ hJ))
    · rw [ClassGroup.mk0_eq_mk0_iff]
      exact ⟨algebraMap _ _ M, b, hM, b_ne_zero, hJ⟩
    rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ← Ideal.dvd_iff_le]
    apply (mul_dvd_mul_iff_left _).mp _
    swap; · exact mt Ideal.span_singleton_eq_bot.mp b_ne_zero
    rw [Subtype.coe_mk, Ideal.dvd_iff_le, ← hJ, mul_comm]
    apply Ideal.mul_mono le_rfl
    rw [Ideal.span_le, Set.singleton_subset_iff]
    exact b_mem
  rw [Ideal.dvd_iff_le, Ideal.mul_le]
  intro r' hr' a ha
  rw [Ideal.mem_span_singleton] at hr' ⊢
  obtain ⟨q, r, r_mem, lt⟩ := exists_mem_finset_approx' bS adm a b_ne_zero
  apply @dvd_of_mul_left_dvd _ _ q
  simp only [Algebra.smul_def] at lt
  rw [←
    sub_eq_zero.mp (b_min _ (I.1.sub_mem (I.1.mul_mem_left _ ha) (I.1.mul_mem_left _ b_mem)) lt)]
  refine mul_dvd_mul_right (dvd_trans (map_dvd _ ?_) hr') _
  exact Multiset.dvd_prod (Multiset.mem_map.mpr ⟨_, r_mem, rfl⟩)

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ k, k ≠ 0 ∧ ↑p ^ (-↑k) < ε

Tactic:
exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
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
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ k.succ) ^ (p ^ (k.succ - 1) * (p - 1)) * (Algebra.norm K) (ζ ^ (p ^ k.succ - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
Nat.sub_one,

Goal state after:
case e_a
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
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ k.succ) ^ (p ^ k.succ.pred * (p - 1)) * (Algebra.norm K) (ζ ^ (p ^ k.succ - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d b : ℕ
⊢ Nonnegg c d (-↑0) ↑b → SqLe 0 d b c

Tactic:
by simp [SqLe]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
⊢ xn a1 n ∣ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j

Tactic:
have h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n := by
    zify at *
    apply add_eq_of_eq_sub' (Eq.symm (pell_eqz a1 n))

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (discr K fun i ↦ (algebraMap K L) (-1) ^ ↑i) = 1

Tactic:
simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
          _root_.pow_zero, traceForm_apply, mul_one]
        rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]; simp

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case refine_2
α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ t, q (v ⊗ t) = 0
v : α → ℕ
⊢ ∀ (x : γ), ((fun x ↦ none) ⊗ some) (inr x) = some x

Tactic:
exact fun _ => by simp only [elim_inr]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
this : (lift r) ↑a.norm = 0
⊢ a = 0

Tactic:
by
      simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero,
        zero_mul] at this
      rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
⊢ ↑(n ^ k) < 2 * ↑a * ↑n - ↑n * ↑n - 1

Tactic:
refine eq_pow_of_pell_lem hn.ne' hk.ne' ?_

Goal state after:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
⊢ n ^ k < a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
⊢ n ^ k = m

Tactic:
have hnka : n ^ k < xn hw1 j := calc
      n ^ k ≤ n ^ j := Nat.pow_le_pow_right hn0 (le_trans kw wj)
      _ < (w + 1) ^ j := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) hj0.ne'
      _ ≤ xn hw1 j := xn_ge_a_pow hw1 j

Goal state after:
case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
⊢ n ^ k = m