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

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

Tactic:
BoundedFormula.realize_iff

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : φ.Realize v xs ↔ ψ.Realize v xs
h2' : ψ.Realize v xs ↔ θ.Realize v xs
⊢ φ.Realize v xs ↔ θ.Realize v xs
Module: Mathlib.ModelTheory.Equivalence

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

Tactic:
simp only [realize_iff, realize_inf, realize_not, and_not_self, realize_bot]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.FG
t : Set M
ht : t.Finite ∧ (closure L).toFun t = s
⊢ (closure L).toFun (⇑f '' t) = Substructure.map f s

Tactic:
rw [closure_image, ht.2]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.CG
t : Set M
ht : t.Countable ∧ (closure L).toFun t = s
⊢ (closure L).toFun (⇑f '' t) = Substructure.map f s

Tactic:
rw [closure_image, ht.2]

Goal state after:
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)
⊢ (R.boundedFormula ts).Realize v xs → (R.boundedFormula ts).Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
    exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ Structure.CG L ↥S

Tactic:
by
  rw [Structure.cg_def]
  refine ⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩
  · rw [← Hom.range_eq_map, range_subtype]
    exact h
  · have h := h.map S.subtype.toHom
    rw [← Hom.range_eq_map, range_subtype] at h
    exact h

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ (closure L).toFun ↑(Exists.choose ⋯) = ↑S'

Tactic:
(Exists.choose_spec S'.prop).symm

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ (closure L).toFun ↑(Exists.choose ⋯) = (closure L).toFun ↑(Exists.choose ⋯)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst ∘ y))
h : unify f x i hx = unify f y i hy
⊢ RelMap R x = RelMap R y

Tactic:
refine _root_.trans (relMap_equiv_unify G f R x i hx)
      (_root_.trans ?_ (symm (relMap_equiv_unify G f R y i hy)))

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst ∘ y))
h : unify f x i hx = unify f y i hy
⊢ RelMap R (unify f x i hx) = RelMap R (unify f y i hy)
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 : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g

Tactic:
rw  [← g.symm_symm]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| toRatVec x - ∑ x_1, ((hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1) =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
enter [1, 2, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| hs.floor x x✝ • toRatVec ↑x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case zero
hn : 0 ≠ 0
⊢ λ 0 = exponent (ZMod 0)ˣ

Tactic:
contradiction

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

Goal state before:
pp: n : ℕ
⊢ Λ (n + 1) ≤ Real.log ↑(n + 1)

Tactic:
← vonMangoldt_sum

Goal state after:
n : ℕ
⊢ Λ (n + 1) ≤ ∑ i ∈ (n + 1).divisors, Λ i
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) = p ^ n * (p - 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:
← ha'

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) = orderOf ha.unit * (p - 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.PowerSeries.Derivative

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ (coeff d) ((d⁄dX R) f) = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

Tactic:
· have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
    rw [coeff_derivative, Polynomial.coeff_derivative, coeff_trunc, if_pos this]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n i : ℕ
⊢ (bernoulli n).coeff i = if i ≤ n then _root_.bernoulli (n - i) * ↑(n.choose i) else 0

Tactic:
simp only [bernoulli, finsetSum_coeff, coeff_monomial]

Goal state after:
n i : ℕ
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) =
    if i ≤ n then _root_.bernoulli (n - i) * ↑(n.choose i) else 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]

Goal state after:
n : ℕ
⊢ ∑ x ∈ range (n + 1 - 0),
      ∑ x_1 ∈ range (n + 1 - x),
        (monomial x) (↑((n + 1).choose (x + x_1)) * ↑((x + x_1).choose x) * _root_.bernoulli x_1) =
    (monomial n) ↑n + (monomial n) 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • X ^ (d + 1)).comp (1 + X) - ∑ x ∈ range (d + 1), (d + 2).choose x • x • X ^ (x - 1) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x =
    (d + 2) • X ^ (d + 1) -
      (∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x - ((d + 2) * (d + 1)) • X ^ (d + 1 - 1))

Tactic:
sub_sub_eq_add_sub

Goal state after:
case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • X ^ (d + 1)).comp (1 + X) - ∑ x ∈ range (d + 1), (d + 2).choose x • x • X ^ (x - 1) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x =
    (d + 2) • X ^ (d + 1) + ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m / ↑m ! * ↑q.succ ! *
      (coeff (q - m + 1))
        ({ toFun := fun f ↦ PowerSeries.mk fun n_1 ↦ ↑n ^ n_1 * (coeff n_1) f, map_one' := ⋯, map_mul' := ⋯ } (exp ℚ))

Tactic:
div_mul_eq_mul_div

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / ↑m ! *
      (coeff (q - m + 1))
        ({ toFun := fun f ↦ PowerSeries.mk fun n_1 ↦ ↑n ^ n_1 * (coeff n_1) f, map_one' := ⋯, map_mul' := ⋯ } (exp ℚ))
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ ∑ i ∈ range (n + 1), ‖f ↑i * c i‖ ≤ max (C₁ + C₂) 1

Tactic:
rw [Nat.range_eq_Icc_zero_sub_one _ n.add_one_ne_zero, add_tsub_cancel_right]
      calc
        _ = ∑ k ∈ Icc 0 n, ‖f k‖ * ‖c k‖ := by simp_rw [norm_mul]
        _ = ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
              ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ - ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ + ∫ t in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ := ?_
        _ ≤ C₁ + C₂ := ?_
        _ ≤ max (C₁ + C₂) 1 := le_max_left _ _
      · exact hf _
      · refine tsub_le_tsub_right (le_of_eq_of_le (Real.norm_of_nonneg ?_).symm (hC₁ n)) _
        exact mul_nonneg (norm_nonneg _) (sum_nonneg fun _ _ ↦ norm_nonneg _)
      · grw [sub_eq_add_neg, neg_le_abs, abs_integral_le_integral_abs]
        simp
      · unfold C₂
        grw [setIntegral_mono_set ?_ (.of_forall fun _ ↦ norm_nonneg _)
          Set.Ioc_subset_Ioi_self.eventuallyLE]
        rw [← integrableOn_Ici_iff_integrableOn_Ioi, IntegrableOn,
          integrable_norm_iff (by fun_prop)]
        exact (locallyIntegrableOn_mul_sum_Icc _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop
          hg₁ hg₂

Goal state after:
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)
⊢ ↑(A i₁ % b - A i₀ % b).natDegree * log ↑(Fintype.card Fq) < ↑b.natDegree * log ↑(Fintype.card Fq) + log ε

Tactic:
← lt_div_iff₀ (log_pos one_lt_q'),

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)
⊢ ↑(A i₁ % b - A i₀ % b).natDegree < (↑b.natDegree * log ↑(Fintype.card Fq) + log ε) / log ↑(Fintype.card Fq)
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
x : R
⊢ x ∈ finsetApprox bS adm ↔ ∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x

Tactic:
by
  simp only [finsetApprox, Finset.mem_erase, Finset.mem_image]
  constructor
  · rintro ⟨hx, ⟨i, j⟩, _, rfl⟩
    refine ⟨i, j, ?_, rfl⟩
    rintro rfl
    simp at hx
  · rintro ⟨i, j, hij, rfl⟩
    refine ⟨?_, ⟨i, j⟩, Finset.mem_univ _, rfl⟩
    rw [Ne, sub_eq_zero]
    exact fun h => hij ((distinctElems bS adm).injective h)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 ≤ ⌊log x / log 2⌋₊

Tactic:
rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul]

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ log 2 ≤ log x
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
T : ℤ
hT :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
hT_int : pIntegral p ↑T
⊢ ¬p ∣ (↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)).den

Tactic:
have hR := pIntegral_faulhaber_sum hk fun m hm_pos hm_lt ↦
      Rat.padicValuation_le_one_iff.mpr (ih m hm_lt hm_pos)

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
T : ℤ
hT :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
hT_int : pIntegral p ↑T
hR : pIntegral p (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1))
⊢ ¬p ∣ (↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)).den
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∃ C, ∀ (x : ℝ), ψ x - θ x ≤ C * √x

Tactic:
use (log 4 + 4) * 3
  intro x
  rcases le_total x 1 with h | h
  · rw [theta_eq_zero_of_le_one h, psi_eq_zero_of_le_one h, sub_self]; positivity
  have (n : ℕ) (hn : 2 ≤ n) : ψ (x ^ (1 / (n : ℝ))) ≤ (log 4 + 4) * x.sqrt := by
    grw [psi_le_const_mul_self (by positivity), sqrt_eq_rpow x]; gcongr; norm_cast
  linarith [psi_sub_theta_le_psi_add_psi_add_psi x, this 2 (le_refl _), this 3 (by norm_num),
    this 5 (by norm_num)]

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

Goal state before:
pp: case refine_1.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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ j₁.succ
approx : ¬cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
this : cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
rw [eq_comm, h]

Goal state after:
case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖x‖ = ‖↑0‖ ↔ ‖x‖ = 1 ∨ x = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
f : ℝ → ℝ
u : ℝ
x✝ : u ∈ Set.uIcc 2 x
⊢ deriv (fun x ↦ (log x)⁻¹) u * f u = f u * -(u * log u ^ 2)⁻¹

Tactic:
by simp [field]

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

Goal state before:
pp: case refine_2.refine_1
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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ 0
approx : ¬cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
this : cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
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)⁻¹
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv (fun n ↦ (log n)⁻¹) x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
rw [int_deriv]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
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)⁻¹
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) * -(u * log u ^ 2)⁻¹ =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case 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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : ¬j₀ = j₁
approx : ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A (Classical.choose ⋯).succ % b)) < cardPowDegree b • ε
this : j₀ = j₁
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
int_deriv : ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ log x) u * f u = ∫ (u : ℝ) in 2..x, f u / u
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t

Tactic:
rw [int_deriv]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
int_deriv : ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ log x) u * f u = ∫ (u : ℝ) in 2..x, f u / u
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) / u =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / log a ^ 2 ≤ (b - a) / log a ^ 2

Tactic:
by simp [field]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
hc : x - ↑(x.appr n) = 0
⊢ False

Tactic:
contradiction

Goal state after: