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.Realize v xs✝ → f2.Realize v xs✝

Tactic:
h1,

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.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 all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
h : ∀ {xs : Fin (n✝ + 1) → M}, f✝.toPrenex.Realize v xs ↔ f✝.Realize v xs
xs✝ : Fin n✝ → M
⊢ (∀' f✝.toPrenex).Realize v xs✝ ↔ ∀ (a : M), f✝.Realize v (snoc xs✝ a)

Tactic:
realize_all

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
h : ∀ {xs : Fin (n✝ + 1) → M}, f✝.toPrenex.Realize v xs ↔ f✝.Realize v xs
xs✝ : Fin n✝ → M
⊢ (∀ (a : M), f✝.toPrenex.Realize v (snoc xs✝ a)) ↔ ∀ (a : M), f✝.Realize v (snoc xs✝ a)
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case equal
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
t₁ t₂ : L.Term (α ⊕ Fin n)
⊢ (t₁ =' t₂).Realize v xs → (t₁ =' t₂).Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
    imp_self]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
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
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)

Tactic:
rw [Fin.comp_snoc]

Goal state after:
case all
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
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) (f a))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
hy : y ∈ closure hs.basisSet
⊢ hs.floor x i ≤ hs.floor (x + y) i

Tactic:
simp only [floor]
  apply Int.floor_le_floor
  simp_rw [map_add, add_sub_right_comm, map_add, Finsupp.add_apply, le_add_iff_nonneg_right]
  rw [mem_closure_iff_of_fintype] at hy
  rcases hy with ⟨f, rfl⟩
  simp_rw [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply]
  apply Finset.sum_nonneg
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply, ite_nonneg]

Goal state after:
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 - ∑ 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:
rw [← sub_add_eq_add_sub, sub_add, ← Finset.sum_sub_distrib]

Goal state after:
ι : 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
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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
⊢ DirectLimit G f ≃[L] DirectLimit G' f'

Tactic:
let U i : G i ↪[L] DirectLimit G' f' := (of L _ G' f' i).comp (g i).toEmbedding
  let F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L _ G f U <| by
    intro _ _ _ _
    simp only [U, Embedding.comp_apply, Equiv.coe_toEmbedding, H_commuting, of_f]
  have surj_f : Function.Surjective F := by
    intro x
    rcases x with ⟨i, pre_x⟩
    use of L _ G f i ((g i).symm pre_x)
    simp only [F, U, lift_of, Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.apply_symm_apply]
    rfl
  exact ⟨Equiv.ofBijective F ⟨F.injective, surj_f⟩, F.map_fun', F.map_rel'⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥((closure L).toFun ↑(Finset.image (⇑PM) s)), str := inferInstance } ≈ P

Tactic:
rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥PM.toHom.range, str := inferInstance } ≈ P
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
p : α × β
pf : p ∈ ↑f
⊢ cmp p.1 (a, b).1 = cmp p.2 (a, b).2

Tactic:
exact a_b _ pf

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_1
α : 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'
⊢ (a, b) ∈ ↑f'.comm

Tactic:
change (a, b) ∈ f'.val.image _
      rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm]

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case intro.intro
α : 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 ⋯
⊢ Nonempty (α ≃o β)

Tactic:
exact ⟨OrderIso.ofCmpEqCmp (fun a ↦ (F a).val) (fun b ↦ (G b).val) fun a b ↦ by
      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.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 β
⊢ Nonempty (α ≃o β)

Tactic:
by
  cases nonempty_encodable α
  cases nonempty_encodable β
  let to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦
    Sum.recOn p (definedAtLeft β) (definedAtRight α)
  let our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
  let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ to_cofinal (Sum.inl a))
  let G b := invOfIdeal b our_ideal (cofinal_meets_idealOfCofinals _ to_cofinal (Sum.inr b))
  exact ⟨OrderIso.ofCmpEqCmp (fun a ↦ (F a).val) (fun b ↦ (G b).val) fun a b ↦ by
      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.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ ↦ {p | φ ∈ p}) '' S)
⊢ (∀ s ∈ (fun φ ↦ {p | φ ∈ p}) '' S, s = Set.univ) ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
← setOfPred_mem_eq_univ_iff

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ ↦ {p | φ ∈ p}) '' S)
⊢ (∀ s ∈ (fun φ ↦ {p | φ ∈ p}) '' S, s = Set.univ) ↔ ∀ φ ∈ S, {p | φ ∈ p} = Set.univ
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
p : T.CompleteType α
⊢ (∀ (M : ModelType ↑p) (v : Empty → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize (φ ⊓ ψ) v xs) ↔
    ∀ (x : ModelType ↑p) (x_1 : Empty → ↑x) (x_2 : Fin 0 → ↑x),
      BoundedFormula.Realize φ x_1 x_2 ∧ BoundedFormula.Realize ψ x_1 x_2

Tactic:
exact forall₃_congr fun _ _ _ ↦ BoundedFormula.realize_inf

Goal state after:
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: p q : ℕ
hp : Prime p
hq : Prime q
⊢ IsAlmostPrime 2 (p * q)

Tactic:
simpa using hp.isAlmostPrime_one.mul hq.isAlmostPrime_one

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

Goal state before:
pp: case inl
⊢ Λ 1 ≠ 0 ↔ IsPrimePow 1

Tactic:
simp [not_isPrimePow_one]

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0

Tactic:
by simpa using mn

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hab
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a ↑⌊b⌋₊

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hab
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a ↑⌊b⌋₊

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
by
  convert! sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int
  all_goals rw [Nat.floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
| (monomial x✝¹) (↑((n + 1).choose x✝¹) * ↑((n + 1 - x✝¹).choose (x✝¹ + x✝ - x✝¹)) * _root_.bernoulli x✝)

Tactic:
add_tsub_cancel_left,

Goal state after:
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
| (monomial x✝¹) (↑((n + 1).choose x✝¹) * ↑((n + 1 - x✝¹).choose x✝) * _root_.bernoulli x✝)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case inl
n : ℕ
hn : n ≤ 2
⊢ n ≤ n#

pp: case inr
n : ℕ
hn : 2 < n
⊢ n ≤ n#

Tactic:
· decide +revert

Goal state after:
case inr
n : ℕ
hn : 2 < n
⊢ n ≤ n#
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n# ≤ 4 ^ n

Tactic:
exact (primorial_lt_four_pow n hn).le

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ∑ q ∈ vonStaudtPrimes k, 1 / ↑q = vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k with q ≠ p, 1 / ↑q

Tactic:
by
  rw [Finset.sum_congr (Finset.filter_ne' (vonStaudtPrimes k) p) fun _ _ ↦ rfl]
  by_cases hdvd : (p - 1) ∣ 2 * k
  · have hp_mem : p ∈ vonStaudtPrimes k := Finset.mem_filter.mpr
      ⟨Finset.mem_range.mpr (by have := Nat.le_of_dvd (by lia) hdvd; lia), Fact.out, hdvd⟩
    rw [← Finset.add_sum_erase _ _ hp_mem]
    simp [vonStaudtIndicator, hdvd]
  · rw [Finset.erase_eq_of_notMem fun h ↦ hdvd (Finset.mem_filter.mp h).2.2]
    simp [vonStaudtIndicator, hdvd]

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

Goal state before:
pp: case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := ⋯
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₁
⊢ A i₁ = A i₀

Tactic:
ext j

Goal state after:
case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
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 : ℕ
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : 0 < k
⊢ ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)

Tactic:
have hfilter : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) = ∑ v ∈ range p, (v : ℚ) ^ (2 * k) := by
    cases p <;> simp [Finset.sum_range_eq_add_Ico, show 2 * k ≠ 0 by lia]

Goal state after:
k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ maximalIdeal ℤ_[p]
hn : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ↑m = ↑n

Tactic:
rw [maximalIdeal_eq_span_p] at hm hn
  have := zmod_congr_of_sub_mem_span_aux 1 x m n
  simp only [pow_one] at this
  specialize this hm hn
  apply_fun ZMod.castHom (show p ∣ p ^ 1 by rw [pow_one]) (ZMod p) at this
  simp only [map_intCast] at this
  simpa only [Int.cast_natCast] using this

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ IntegrableOn (fun t ↦ θ t / (t * log t ^ 2)) (Set.Icc 2 x) volume

Tactic:
conv => arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]

Goal state after:
x : ℝ
⊢ IntegrableOn (fun x ↦ 1 / (x * log x ^ 2) * ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ ↑p ∣ x

Tactic:
rw [← norm_lt_one_iff_dvd, ← sub_zero x, ← Nat.cast_zero, ← H]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ ‖x - ↑x.zmodRepr‖ < 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) z

Tactic:
have : log z ≠ 0 := by apply log_ne_zero_of_pos_of_ne_one <;> linarith

Goal state after:
case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this✝ : z ≠ 0
this : log z ≠ 0
⊢ DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) z
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(↑x.zmodRepr).val = ↑x.zmodRepr

Tactic:
Nat.cast_inj

Goal state after:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ (↑x.zmodRepr).val = x.zmodRepr
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
apply sub_zmodRepr_mem

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
obtain ⟨ζ, hζ⟩ := HasEnoughRootsOfUnity.exists_primitiveRoot L (p ^ (k + i))

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_f.e_f
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
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
⊢ (fun j ↦ ((e j) pb.gen - (e i) pb.gen) ^ 2) = fun j ↦ -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
ext j

Goal state after:
case e_f.e_f
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
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i j : Fin pb.dim
⊢ ((e j) pb.gen - (e i) pb.gen) ^ 2 = -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist ((lift f_compat) r) (g r) ≤ ε

Tactic:
apply le_trans _ (le_of_lt hn)

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist ((lift f_compat) r) (g r) ≤ ↑p ^ (-↑n)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
this : ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
i : Fin B.dim
x✝ : i ∈ univ
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ R[B.gen]

Tactic:
replace this := this i

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
this : ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ R[B.gen]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))

Tactic:
by
    simpa [mul_comm, mul_left_comm] using Nat.mul_le_mul xy zw

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 = xn a1 n * xn a1 n * 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

Tactic:
h1,

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