mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ f ≤ f'.comm

Tactic:
change _ ⊆ f'.val.image _

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ↑f ⊆ Finset.image ⇑(Equiv.prodComm β α) ↑f'
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
g : ↥(insert m hS.toFinset) ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
⊢ (Substructure.closure Language.order).toFun {m} ⊔ S =
    (Substructure.closure Language.order).toFun ↑(insert m hS.toFinset)

Tactic:
simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
        Substructure.closure_eq]

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith ∼φ)

Tactic:
exact isOpen_typesWith _

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr

Tactic:
rw [← H, A', sumInv_pqr, add_assoc]

Goal state after:
case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Tactic:
clear hqr

Goal state after:
case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: ⊢ ¬Monoid.exponent (ZMod 8)ˣ = Nat.card (ZMod 8)ˣ

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
⊢ ¬Monoid.exponent (ZMod 8)ˣ = Fintype.card (ZMod 8)ˣ
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ exponent (ZMod a)ˣ ∣ exponent (ZMod (n✝ + 1))ˣ

Tactic:
exact MonoidHom.exponent_dvd <| ZMod.unitsMap_surjective h

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ λ (a.lcm b) ∣ (λ a).lcm (λ b)

Tactic:
carmichael_eq_exponent h₀.left,

Goal state after:
case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ λ (a.lcm b) ∣ (exponent (ZMod a)ˣ).lcm (λ b)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case succ
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
ha' : orderOf ha.unit = p ^ n
c : (ZMod p)ˣ
hc : orderOf c = Nat.card (ZMod p)ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case succ
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
ha' : orderOf ha.unit = p ^ n
c : (ZMod p)ˣ
hc : orderOf c = Fintype.card (ZMod p)ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h
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
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ orderOf ha.unit * (p - 1) = Nat.card (ZMod (p ^ (n + 1)))ˣ

pp: case h
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
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ (orderOf ha.unit).Coprime (orderOf (b ^ k))

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case h
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
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ orderOf ha.unit * (p - 1) = Fintype.card (ZMod (p ^ (n + 1)))ˣ

case h
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
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ (orderOf ha.unit).Coprime (orderOf (b ^ k))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ)
⊢ False

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (Fintype.card (ZMod m)ˣ).Coprime (Fintype.card (ZMod n)ˣ)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
x : X
⊢ ‖‖f x‖⁻¹ • f x‖ ≤ 1

Tactic:
simp [norm_smul, inv_mul_le_one]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ constantCoeff (exp A) = 1

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (1 / ↑0!) = 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case neg
n i : ℕ
h : ¬i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) = 0

Tactic:
exact Finset.sum_eq_zero <| by grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
exact Finset.sum_eq_zero (fun x hx => by rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self])

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ (∑ k ∈ range n, exp ℚ ^ k) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
geom_sum_mul,

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ exp ℚ ^ n - 1 =
    (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
replace h : n < 521 := h.trans_lt (by norm_num1)

Goal state after:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case zero.refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (h.card ε ^ 0).succ → Fin 0 → R
⊢ ∀ (k : Fin 0), ↑(abv (A 1 k % b - A 0 k % b)) < abv b • ε

Tactic:
rintro ⟨i, ⟨⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℕ
hne : q ≠ p
left✝ : q < 2 * k + 2
hq_prime : Nat.Prime q
right✝ : q - 1 ∣ 2 * k
⊢ (1 / ↑q).den.Coprime p

Tactic:
rw [show ((1 : ℚ) / q).den = q by simp [hq_prime.ne_zero]]

Goal state after:
k p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℕ
hne : q ≠ p
left✝ : q < 2 * k + 2
hq_prime : Nat.Prime q
right✝ : q - 1 ∣ 2 * k
⊢ q.Coprime p
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
⊢ ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε

Tactic:
refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h✝.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h✝.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h✝.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i j : Fin (M ^ n).succ
h : (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i = (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) j
⊢ i = j

case refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i₀ i₁ : Fin (M ^ n).succ
⊢ t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₀) = t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₁)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ log ↑n = 0

Tactic:
convert! log_one

Goal state after:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ ↑n = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero.inl
k : ℕ
hk : k > 0
hi : 0 + 1 < 2 * k
inst✝ : Fact (Nat.Prime 2)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / ↑2)
⊢ (Rat.padicValuation 2) (-(↑2 ^ (2 * k - 1) / 2)) ≤ 1

Tactic:
push_cast
      rw [show 2 * k - 1 = (2 * k - 2) + 1 by lia, pow_succ, mul_div_cancel_right₀ _ two_ne_zero]
      exact_mod_cast Int.padicValuation_le_one ..

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑p ∣ r.num - r.num * r.den.gcdA p % ↑p * ↑r.den

Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
  simp only [Int.cast_natCast, Int.cast_mul, Int.cast_sub]
  have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)
  simp only [Int.cast_natCast, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add,
    Int.cast_mul, zero_mul, add_zero] at this
  push_cast
  rw [mul_right_comm, mul_assoc, ← this]
  suffices rdcp : r.den.Coprime p by
    rw [rdcp.gcd_eq_one]
    simp only [mul_one, cast_one, sub_self]
  apply Coprime.symm
  apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right
  rw [← Int.natCast_dvd_natCast, ← norm_int_lt_one_iff_dvd, not_lt]
  apply ge_of_eq
  rw [← isUnit_iff]
  exact isUnit_den r h

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

Goal state before:
pp: case succ.refine_2.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁✝ : Fin (n + 1)
i₀ i₁ : Fin n
⊢ Fin.cons j t' i₀.succ = Fin.cons j t' i₁.succ ↔ ↑(cardPowDegree (A i₁.succ % b - A i₀.succ % b)) < cardPowDegree b • ε

Tactic:
rw [Fin.cons_succ, Fin.cons_succ]

Goal state after:
case succ.refine_2.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁✝ : Fin (n + 1)
i₀ i₁ : Fin n
⊢ t' i₀ = t' i₁ ↔ ↑(cardPowDegree (A i₁.succ % b - A i₀.succ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: 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
⊢ 1 - ↑1 ∈ Ideal.span {↑v}

Tactic:
· simp only [sub_self, cast_one, Submodule.zero_mem]

Goal state after:
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:
by
    rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]
    · exact f_spec _
    · simp only [sub_zero, cast_zero, Submodule.zero_mem]

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

Goal state before:
pp: case neg.inl
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
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h)).cast

Tactic:
suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec

Goal state after:
case neg.inl
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
⊢ c = ↑(unitCoeff h)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ g (h ↑↑ζ) = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)

Tactic:
rw [toFun_spec, ← Subgroup.coe_pow, toFun_spec, mul_comm, Subgroup.coe_pow, ← pow_mul,
    ← Subgroup.coe_pow]

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ↑↑(ζ ^ ((χ₀ n h).val * (χ₀ n g).val)) = ↑(↑ζ ^ (χ₀ n h * χ₀ n g).val)
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
r : R
i j : ℕ
h : i ≤ j
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i

Tactic:
specialize f_compat i j h

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i
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
⊢ IsUnit r

Tactic:
refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩

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
⊢ r * r' = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Tactic:
injection pellZd_add a1 m n with _ h
  zify
  rw [h]
  simp [pellZd]

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

Goal state before:
pp: d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ IsUnit z.norm

Tactic:
by
  rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]

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

Goal state before:
pp: 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)
⊢ (minpoly K (-1)).natDegree = 1

Tactic:
show (-1 : L) = algebraMap K L (-1) by simp,

Goal state after:
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)
⊢ (minpoly K ((algebraMap K L) (-1))).natDegree = 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Tactic:
have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den / ↑ξ.den - ↑q.num| < 1 / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den

Tactic:
div_sub' hξ₀.ne',

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |(↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num) / ↑ξ.den| < 1 / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ a = b

Tactic:
rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
⊢ m * n ∈ factoredNumbers s

Tactic:
by
  have hm' := primeFactors_subset_of_mem_factoredNumbers hm
  have hn' := primeFactors_subset_of_mem_factoredNumbers hn
  exact mem_factoredNumbers_of_primeFactors_subset (mul_ne_zero hm.1 hn.1)
    <| primeFactors_mul hm.1 hn.1 ▸ Finset.union_subset hm' hn'

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n : ℕ
⊢ n.smoothNumbers = factoredNumbers n.primesBelow

Tactic:
by
  rw [smoothNumbers_eq_factoredNumbers]
  refine Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter
  simp_rw [mem_factoredNumbers'] at hm ⊢
  exact fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z

Tactic:
rw [Nat.div_eq_iff hy, Nat.succ_mul]
              grind

Goal state after: