mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
⊢ w ∈ ↑(f (a + x + u))

Tactic:
SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
⊢ w ∈ f (a + x + u)
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ψ).Realize v xs

Tactic:
exact h M v xs

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ n s, (closure L).toFun (range s) = N) → ∃ S, S.Finite ∧ (closure L).toFun S = N

Tactic:
· rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : ∅.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ φ.toPrenex).Realize v xs

Tactic:
rw [realize_iff, realize_toPrenex]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
x✝ : (ι ⊕ Fin n) ⊕ Fin m → ℕ
⊢ u + A *ᵥ (x✝ ∘ Sum.inl) ∘ Sum.inr = (x✝ ∘ Sum.inl) ∘ Sum.inl ∧ v + B *ᵥ x✝ ∘ Sum.inr = (x✝ ∘ Sum.inl) ∘ Sum.inl ↔
    Sum.elim u v + fromBlocks (fromCols 0 A) 0 0 B *ᵥ x✝ = 0 + fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0 *ᵥ x✝

Tactic:
simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j ∈ closure (hs.basisSet \ {↑i})

Tactic:
refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _

Goal state after:
case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j ∈ closure (hs.basisSet \ {↑i})

Tactic:
refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _

Goal state after:
case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j ∈ closure (hs.basisSet \ {↑i})

Tactic:
refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _

Goal state after:
case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j ∈ closure (hs.basisSet \ {↑i})

Tactic:
refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _

Goal state after:
case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: case h
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 ⋯))
g' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr ↑((Substructure.closure Language.order).toFun {m} ⊔ S) ↑(insert m hS.toFinset)
        ⋯).toOrderEmbedding
    g
x : M
xS : x ∈ S
⊢ f ⟨x, xS⟩ = ((StrongHomClass.toEmbedding g').comp (Substructure.inclusion ⋯)) ⟨x, xS⟩

Tactic:
refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩

Goal state after:
case h
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 ⋯))
g' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr ↑((Substructure.closure Language.order).toFun {m} ⊔ S) ↑(insert m hS.toFinset)
        ⋯).toOrderEmbedding
    g
x : M
xS : x ∈ S
⊢ x ∈ hS.toFinset
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
hφ : { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ T.typesWith φ
⊢ ↑F ≤ Filter.principal (T.typesWith φ)

Tactic:
rw [Filter.le_principal_iff]

Goal state after:
case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
hφ : { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ T.typesWith φ
⊢ T.typesWith φ ∈ ↑F
Module: Mathlib.Topology.Order.IsLocallyClosed

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Ico a b)

Tactic:
rw [← Set.Iio_inter_Ici]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ 1 ∈ (Finset.range (p + 1)).erase 0

Tactic:
simp [hp.pos]

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑(p ^ m) * ↑a) = p ^ 0

Tactic:
ZMod.natCast_self

Goal state after:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + 0 * ↑a) = p ^ 0
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:
simp_rw [Nat.card_eq_fintype_card, card_units_eq_totient,
    Nat.totient_coprime_totient_iff, hm1, hn1, false_or] at h

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 : m = 2 ∨ n = 2
⊢ False
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ π' n = 0 ↔ n ≤ 2

Tactic:
primeCounting',

Goal state after:
n : ℕ
⊢ count Prime n = 0 ↔ n ≤ 2
Module: Mathlib.NumberTheory.PrimeCounting

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

Tactic:
primeCounting',

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

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

Tactic:
primeCounting',

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

Goal state before:
pp: p l : ℕ
inst✝ : Fact (Nat.Prime p)
hbij : ∑ v ∈ Ico 1 p, ↑v ^ l = ∑ u, ↑u ^ l
⊢ (∑ v ∈ Ico 1 p, ↑v ^ l + if p - 1 ∣ l then 1 else 0) = 0

Tactic:
rw [hbij, FiniteField.sum_pow_units, ZMod.card]

Goal state after:
p l : ℕ
inst✝ : Fact (Nat.Prime p)
hbij : ∑ v ∈ Ico 1 p, ↑v ^ l = ∑ u, ↑u ^ l
⊢ ((if p - 1 ∣ l then -1 else 0) + if p - 1 ∣ l then 1 else 0) = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
p : ℕ
hp : Nat.Prime p
⊢ (n.choose k).factorization p ≤ Nat.log p n

Tactic:
exact factorization_choose_le_log

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
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
by
  obtain ⟨i⟩ := bS.index_nonempty
  have him : (Finset.univ.image fun k => abv (bS.repr a k)).Nonempty :=
    ⟨_, Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩⟩
  set y' : ℤ := Finset.max' _ him with y'_def
  have hy' : ∀ k, abv (bS.repr a k) ≤ y' := by
    intro k
    exact @Finset.le_max' ℤ _ _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩)
  have : (y' : T) < y := by
    rw [y'_def,
      ← Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h)
          _ (him.image _)]
    apply (Finset.max'_lt_iff _ (him.image _)).mpr
    simp only [Finset.mem_image]
    rintro _ ⟨x, ⟨k, -, rfl⟩, rfl⟩
    exact hy k
  have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i)
  apply (Int.cast_le.mpr (norm_le abv bS a hy')).trans_lt
  simp only [Int.cast_mul, Int.cast_pow]
  apply mul_lt_mul' le_rfl
  · exact pow_lt_pow_left₀ this (by positivity) (@Fintype.card_ne_zero _ _ ⟨i⟩)
  · positivity
  · exact Int.cast_pos.mpr (normBound_pos abv bS)

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 ℤ
I : ↥(Ideal S)⁰
⊢ ∃ z, ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z

Tactic:
obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)

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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
⊢ ∃ z, ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z
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}
⊢ log ↑(x✝¹ ^ x✝²).minFac = log ↑x✝¹

Tactic:
Prime.pow_minFac _ (by linarith [mem_Icc.mp hk])

Goal state after:
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}
⊢ log ↑x✝¹ = log ↑x✝¹

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}
⊢ Nat.Prime x✝¹
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ψ x = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))

Tactic:
psi_eq_sum_theta' (by linarith) hN,

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n)) = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))
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 := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : 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 := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FiniteDimensional Ft K
⊢ FunctionField F K

Tactic:
· let b := Module.finBasis F⟮X⟯ K
    exact (b.mapCoeffs e this).finiteDimensional_of_finite

Goal state after:
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 := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FiniteDimensional Ft K
⊢ FunctionField F K
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp_prime.1.ne_zero

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

Goal state before:
pp: case refine_1
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 := ∏ m ∈ finsetApprox bS adm, m
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
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * 0
⊢ False

Tactic:
rw [Ideal.zero_eq_bot, Ideal.mul_bot] at hJ

Goal state after:
case refine_1
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 := ∏ m ∈ finsetApprox bS adm, m
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
hJ : Ideal.span {(algebraMap R S) M} * ↑I = ⊥
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ↑(π ⌊x⌋₊) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
by
  -- Rewrite in a form to which Abel summation can be applied
  simp only [primeCounting, primeCounting', count_eq_card_filter_range]
  rw [card_eq_sum_ones, range_succ_eq_Icc_zero, sum_filter]
  push_cast
  let a : ℕ → ℝ := Set.indicator (Set.ofPred Nat.Prime) (fun n ↦ log n)
  trans ∑ n ∈ Icc 0 ⌊x⌋₊, (log n)⁻¹ * a n
  · refine sum_congr rfl fun n hn ↦ ?_
    split_ifs with h
    · have : log n ≠ 0 := log_ne_zero_of_pos_of_ne_one (mod_cast h.pos) (mod_cast h.ne_one)
      simp [a, h, field]
    · simp [a, h]
  rw [sum_mul_eq_sub_integral_mul₁ a (f := fun n ↦ (log n)⁻¹) (by simp [a]) (by simp [a]),
    ← intervalIntegral.integral_of_le hx]
  · -- Rewrite the derivative inside the integral
    have int_deriv (f : ℝ → ℝ) :
        ∫ u in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u =
        ∫ u in 2..x, f u * -(u * log u ^ 2)⁻¹ :=
      intervalIntegral.integral_congr fun u _ ↦ by simp [field]
    rw [int_deriv]
    simp [a, Set.indicator_apply, sum_filter, theta_eq_sum_Icc]
    grind
  · -- Differentiability
    intro z ⟨_, _⟩
    have : z ≠ 0 := by linarith
    have : log z ≠ 0 := by apply log_ne_zero_of_pos_of_ne_one <;> linarith
    fun_prop
  · -- Integrability of the derivative
    refine ContinuousOn.integrableOn_Icc fun z ⟨_, _⟩ ↦ ContinuousWithinAt.congr ?_
      (fun _ _ ↦ deriv_inv_log_apply) deriv_inv_log_apply
    have : z ≠ 0 := by linarith
    have : log z ^ 2 ≠ 0 := by
      refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_ne_one ?_ ?_ <;> linarith
    exact ContinuousAt.continuousWithinAt <| by fun_prop

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ RingHom.ker toZMod = maximalIdeal ℤ_[p]

Tactic:
by
  ext x
  rw [RingHom.mem_ker]
  constructor
  · intro h
    simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x
  · intro h
    rw [← sub_zero x] at h
    dsimp [toZMod, toZModHom]
    convert! zmod_congr_of_sub_mem_max_ideal x _ 0 _ h
    · norm_cast
    · apply sub_zmodRepr_mem

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2

Tactic:
rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply,
    traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul, det_transpose, pow_two]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ ↑(π ⌊x⌋₊) ≤ log 4 * x / log √x + √x

Tactic:
have : 0 < log √x := log_pos (lt_sqrt_of_sq_lt (by simp [hx]))
  field_simp
  grind [pi_mul_log_sqrt_le hx.le]

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

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
⊢ (fromZetaAut hμ h) (zeta n K L) = μ

Tactic:
by
  simp_rw [fromZetaAut, autEquivPow_symm_apply]
  generalize_proofs hζ h _ hμ _
  nth_rewrite 4 [← hζ.powerBasis_gen K]
  rw [PowerBasis.equivOfMinpoly_gen, hμ.powerBasis_gen K]
  convert! h.choose_spec.2
  exact ZMod.val_cast_of_lt h.choose_spec.1

Goal state after: