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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
by
  classical
  have := Fintype.ofFinite ι
  rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂
  rcases hs₁ with ⟨u, n, A, rfl⟩
  rcases hs₂ with ⟨v, m, B, rfl⟩
  simp_rw [← ofPred_and, exists_and_exists_comm]
  refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)
  convert!
    isSemilinearSet_setOfPred_mulVec_eq (κ := (ι ⊕ Fin n) ⊕ Fin m) (Sum.elim u v) 0
      (fromBlocks (fromCols 0 A) 0 0 B) (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0)
  simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case mk.mk
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)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩ ↔
    (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Tactic:
refine ⟨fun xy => ?_, fun xy => ⟨i, hx, hy, xy⟩⟩

Goal state after:
case mk.mk
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)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
xy : ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ f.symm ≤ g.symm

Tactic:
rw [le_iff]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
    ∀ (x : ↥f.symm.dom), (inclusion cod_le_cod) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion dom_le_dom) x)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - toRatVec hs.base ≤ toRatVec x

Tactic:
simp [toRatVec_nonneg]

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

Goal state before:
pp: case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ hs.fract (hs.base + y) = hs.base ∧
    ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor (hs.base + y) i ∧ (↑i ∉ hs.periods → hs.floor (hs.base + y) i = 0)

Tactic:
refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩

Goal state after:
case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ hs.fract (hs.base + y) = hs.base

case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
i : ↑hs.basisSet
⊢ 0 ≤ hs.floor (hs.base + y) i

case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
⊢ hs.floor (hs.base + y) i = 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case e'_2.a
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
⊢ (if ↑i ∈ hs.periods then (hs.floor x i).toNat • ↑i else 0) = (hs.floor x i).toNat • ↑i

Tactic:
split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet
    (⋃ u ∈ hs.fundamentalDomain \ {hs.base},
      {x | ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = u + y})

Tactic:
refine .biUnion hs.finite_fundamentalDomain.sdiff fun i hi => .proj' ?_
    rw [ofPred_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet) (LinearMap.funLeft ℕ ℕ Sum.inr)
    apply IsSemilinearSet.proj'
    rw [ofPred_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet) (LinearMap.funLeft ℕ ℕ Sum.inr)
    classical
    have := Fintype.ofFinite ι
    convert!
      Nat.isSemilinearSet_setOfPred_mulVec_eq (κ := (ι ⊕ ι) ⊕ ι) 0 i
        (Matrix.fromCols (Matrix.fromCols 1 0) 1) (Matrix.fromCols (Matrix.fromCols 0 1) 0) using
      4 <;> simp [fromCols_mulVec]

Goal state after:
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 β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ ⇑(OrderEmbedding.ofStrictMono (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⋯) ∘ Set.inclusion ⋯ = ⇑f

Tactic:
ext x
    simp only [OrderEmbedding.coe_ofStrictMono,
      Function.comp_apply, Finset.coe_mem, ↓reduceDIte, Subtype.coe_eta]

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

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ CompactSpace (T.CompleteType α)

Tactic:
constructor
  rw [isCompact_iff_ultrafilter_le_nhds]
  intros F _
  refine ⟨⟨{φ | T.typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩
  · intro φ x
    exact F.mem_of_superset Filter.univ_mem (fun p _ ↦ p.subset x)
  · rw [Theory.IsMaximal, Theory.isSatisfiable_iff_isFinitelySatisfiable]
    refine ⟨?_, ?_⟩
    · rw[Theory.IsFinitelySatisfiable]
      intro x hx
      have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ
      rw [← Filter.biInter_finset_mem x] at this
      obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this
      have subset : (x : Set _) ⊆ T.toTheory := by rwa [Set.mem_iInter₂] at T_inter
      exact T.isMaximal.1.mono subset
    · intro φ
      simp only [mem_ofPred_eq, typesWith_not]
      exact Ultrafilter.mem_or_compl_mem F (T.typesWith φ)
  · refine ⟨mem_univ _, ?_⟩
    · rw [nhds_generateFrom]
      apply le_iInf₂
      rintro _ ⟨hφ, φ, rfl⟩
      rw [Filter.le_principal_iff]
      exact hφ

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:

Tactic:
(2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
    _ = 1 := by norm_num

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k

Tactic:
rw [← integral_deriv_eq_sub (fun t ht ↦ hf_diff t (h_inc₂ ht)),
      ← intervalIntegral.integral_mul_const]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k

𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂
Module: Mathlib.RingTheory.PowerSeries.Exp

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

Tactic:
by
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]
  simp

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hac
𝕜 : 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
⊢ IntegrableOn (fun x ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) (Set.Icc a (↑⌊a⌋₊ + 1)) volume

Tactic:
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux4)

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
Icc_eq_cons_Ioc (Nat.zero_le _)

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ ∑ k ∈ cons 0 (Ioc 0 ⌊b⌋₊) ⋯, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ ∑ x ∈ range (p + 1), _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) +
        _root_.bernoulli (p.succ - (p + 1 - (p + 1))) * ↑(p.succ.choose (p + 1 - (p + 1))) * ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)

Tactic:
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
      add_tsub_cancel_right]

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

Goal state before:
pp: case succ
n i : ℕ
⊢ (bernoulli (n + 1)).coeff i * (-1) ^ i = ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i

Tactic:
coeff_smul,

Goal state after:
case succ
n i : ℕ
⊢ (bernoulli (n + 1)).coeff i * (-1) ^ i = (-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1)).coeff i
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n i : ℕ
⊢ (bernoulli (n + 1)).coeff i * (-1) ^ i =
    (-1) ^ (n + 1) • ((bernoulli (n + 1)).coeff i + ((n + 1) • X ^ (n + 1 - 1)).coeff i)

Tactic:
coeff_smul,

Goal state after:
case succ
n i : ℕ
⊢ (bernoulli (n + 1)).coeff i * (-1) ^ i =
    (-1) ^ (n + 1) • ((bernoulli (n + 1)).coeff i + (n + 1) • (X ^ (n + 1 - 1)).coeff i)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by
    simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ 2 * ↑k - 2 * ↑m + 1 ≠ 0

Tactic:
norm_cast; lia

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ 2 * ↑k - 2 * ↑m + 1 = ↑(2 * k + 1 - 2 * m)

Tactic:
norm_cast; lia

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log ↑(primorial ⌊x⌋₊) ≤ log (4 ^ ⌊x⌋₊)

pp: x : ℝ
hx : 0 ≤ x
⊢ log (4 ^ ⌊x⌋₊) ≤ log 4 * x

Tactic:
· gcongr <;> norm_cast
    exacts [primorial_pos _, primorial_le_four_pow _]

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log (4 ^ ⌊x⌋₊) ≤ log 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ ↑p ≤ x

Tactic:
exact (le_self_pow₀ (mod_cast hp.nat_prime.one_le) hk₀.ne').trans hbx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ ↑(normBound abv bS) ≠ 0

Tactic:
norm_cast; lia

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

Goal state before:
pp: case h
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ ↑(Fintype.card ι) ≠ 0

Tactic:
norm_cast; lia

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

Goal state before:
pp: case hx
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(normBound abv bS)

Tactic:
norm_cast; lia

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

Goal state before:
pp: case hx
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(abv b)

Tactic:
norm_cast; lia

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

Goal state before:
pp: case hy
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))

Tactic:
norm_cast; lia

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ ψ x

Tactic:
rw [psi_eq_theta_add_sum_theta h]

Goal state after:
case neg
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑n))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ vonStaudtPrimes k, 1 / ↑q).den

Tactic:
sum_one_div_prime_eq_indicator_div_add (p := p) hk,

Goal state after:
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + (vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k with q ≠ p, 1 / ↑q)).den
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) +
                  ∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
                b x (1 + 6 * N + 1) +
              b x (1 + 6 * N + 1 + 1) +
            b x (1 + 6 * N + 2 + 1) +
          b x (1 + 6 * N + 3 + 1) +
        b x (1 + 6 * N + 4 + 1) +
      b x (1 + 6 * N + 5 + 1) =
    b x 1 +
          (∑ n ∈ Icc 1 (3 * N), b x (2 * n) + b x (2 * (3 * N + 1)) + b x (2 * (3 * N + 1 + 1)) +
            b x (2 * (3 * N + 2 + 1))) +
        (∑ n ∈ Icc 1 (2 * N), b x (3 * n) + b x (3 * (2 * N + 1)) + b x (3 * (2 * N + 1 + 1))) +
      (∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
        (b x (6 * (N + 1) - 1) - b x (6 * (N + 1)) + b x (6 * (N + 1) + 1)))

Tactic:
show 6 * (N + 1) - 1 = 6 * N + 5 by lia

Goal state after:
case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) +
                  ∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
                b x (1 + 6 * N + 1) +
              b x (1 + 6 * N + 1 + 1) +
            b x (1 + 6 * N + 2 + 1) +
          b x (1 + 6 * N + 3 + 1) +
        b x (1 + 6 * N + 4 + 1) +
      b x (1 + 6 * N + 5 + 1) =
    b x 1 +
          (∑ n ∈ Icc 1 (3 * N), b x (2 * n) + b x (2 * (3 * N + 1)) + b x (2 * (3 * N + 1 + 1)) +
            b x (2 * (3 * N + 2 + 1))) +
        (∑ n ∈ Icc 1 (2 * N), b x (3 * n) + b x (3 * (2 * N + 1)) + b x (3 * (2 * N + 1 + 1))) +
      (∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
        (b x (6 * N + 5) - b x (6 * (N + 1)) + b x (6 * (N + 1) + 1)))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
⊢ (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p).den = 1

Tactic:
by_contra h

Goal state after:
case inr
k : ℕ
hk : k > 0
h : ¬(bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p).den = 1
⊢ False
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
zmodRepr_eq_zero_iff_dvd

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ ¬↑p ∣ ↑x
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
⊢ discr A b = 0

Tactic:
by_contra h

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬discr A b = 0
⊢ False
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

Tactic:
Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ ((leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)).det =
    (algebraMap R Rₘ) ((norm R) a)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case succ
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n N : ℕ
IH : ↑(f (N + n)) = ↑(f n)
⊢ ↑(f (N + n)) = ↑(f (N + n + 1))

Tactic:
ZMod.intCast_eq_intCast_iff_dvd_sub

Goal state after:
case succ
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n N : ℕ
IH : ↑(f (N + n)) = ↑(f n)
⊢ ↑(p ^ n) ∣ f (N + n + 1) - f (N + n)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ a

Tactic:
apply dvd_trans _ hdvd

Goal state after:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ b
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inr.inr.inr.inl
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := ↑z + -↑x, im := ↑y + -↑w }.Nonneg

Tactic:
add_comm (y : ℤ)

Goal state after:
case inr.inr.inr.inl
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := ↑z + -↑x, im := -↑w + ↑y }.Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑0, im := ↑(y + 1) } + { re := ofNat x, im := -[y+1] }).Nonneg

Tactic:
by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑(x + 1), im := ↑0 } + { re := -[x+1], im := ofNat y }).Nonneg

Tactic:
by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑(x + 1), im := ↑(y + 1) } + { re := -[x+1], im := -[y+1] }).Nonneg

Tactic:
by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

Goal state after: