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

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁷ : Language.order.Structure M
inst✝⁶ : LE M
inst✝⁵ : Language.order.OrderedStructure M
N : Type u_1
inst✝⁴ : Language.order.Structure N
inst✝³ : LE N
inst✝² : Language.order.OrderedStructure N
F : Type u_2
inst✝¹ : FunLike F M N
inst✝ : OrderHomClass F M N
⊢ ∀ (φ : F) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M), RelMap r x → RelMap r (⇑φ ∘ x)

Tactic:
by
    simp only [forall_relations, relation_eq_leSymb, relMap_leSymb, Fin.isValue,
      Function.comp_apply]
    exact fun φ x => map_rel φ

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x✝ : ι → ℕ
⊢ x✝ ∈ sᶜ ↔ x✝ ∈ hs.setOfFractNe ∪ (hs.setOfFloorNeg ∪ hs.setOfFloorPos)

Tactic:
simp only [mem_compl_iff, hs.mem_iff_fract_eq_and_floor_nonneg, IsProperLinearSet.setOfFractNe,
    IsProperLinearSet.setOfFloorNeg, IsProperLinearSet.setOfFloorPos, mem_union, mem_ofPred_eq]

Goal state after:
ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x✝ : ι → ℕ
⊢ ¬(hs.fract x✝ = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x✝ i ∧ (↑i ∉ hs.periods → hs.floor x✝ i = 0)) ↔
    hs.fract x✝ ≠ hs.base ∨
      (hs.fract x✝ = hs.base ∧ ∃ i, hs.floor x✝ i < 0) ∨
        hs.fract x✝ = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x✝ i
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
⊢ Dense (⋂ n, f n)

Tactic:
dense_iff_inter_open

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
⊢ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ ⋂ n, f n).Nonempty
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ IsCompact univ

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Goal state after:
L : Language
T : L.Theory
α : Type u_1
⊢ ∀ (f : Ultrafilter (T.CompleteType α)), ↑f ≤ Filter.principal univ → ∃ x ∈ univ, ↑f ≤ nhds x
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 : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc ?m.188 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.188 n, c k
h' : t ∈ Ι t₁ t₂
⊢ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k

Tactic:
rw [h (h_inc₁ h')]

Goal state after:
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ∣ a - b ^ 1

Tactic:
pow_one

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ∣ a - b
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
pow_one

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑p * ↑a) = orderOf (1 + ↑p * ↑a)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + (pderiv i) f * g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
mul_comm _ g,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + g * (pderiv i) f) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
h : ¬i = j
⊢ (pderiv R i) (X j) = Pi.single i 1 j

Tactic:
· grind [pderiv_X_of_ne]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: case h
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
⊢ Prime p → p.Coprime a

Tactic:
exact coprime_of_lt_prime h0 <| h1.trans_le (mem_Ico.1 hp).1

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) * bernoulli' k = ↑(n + 1)

Tactic:
suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
  simp_rw [mul_sum, ← mul_assoc]
  refine sum_congr rfl fun k hk => ?_
  congr
  have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
  simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
  rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Goal state after:
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 !
⊢ (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)

Tactic:
have h : B * (exp ℚ - 1) = X * exp ℚ := by
    simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n ↦ ∫ (x : ℝ) in 1..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n ↦
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k =
    ∑ k ∈ Icc 0 x✝, f ↑k * c k

Tactic:
sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n ↦ ∫ (x : ℝ) in 1..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n ↦
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k =
    f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n ↦ ∫ (x : ℝ) in 1..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n ↦
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ IntegrableOn (deriv f) (Set.Icc 1 ↑x✝) volume
Module: Mathlib.NumberTheory.Bernoulli

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

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

Tactic:
· left
      congr

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

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
⊢ pIntegral p (↑p ^ N / ↑M)

Tactic:
have hM'_cop : M'.Coprime p := (Nat.coprime_ordCompl Fact.out hM).symm

Goal state after:
p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
⊢ pIntegral p (↑p ^ N / ↑M)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x = θ ↑⌊x⌋₊

Tactic:
by
  unfold theta
  rw [floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (n + 1), n.choose m ≤ ∑ k ∈ range (n + 1), n.lcmUpto

Tactic:
by
    gcongr with k hk
    exact le_of_dvd (lcmUpto_pos n) (choose_dvd_lcmUpto <| by grind)

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

Goal state before:
pp: case mp
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 ≠ 0 ∧ ∃ a ∈ Finset.univ, (distinctElems bS adm) a.1 - (distinctElems bS adm) a.2 = x) →
    ∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x

Tactic:
rintro ⟨hx, ⟨i, j⟩, _, rfl⟩

Goal state after:
case mp
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
i j : Fin (cardM bS adm).succ
left✝ : (i, j) ∈ Finset.univ
hx : (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2 ≠ 0
⊢ ∃ i_1 j_1,
    i_1 ≠ j_1 ∧
      (distinctElems bS adm) i_1 - (distinctElems bS adm) j_1 =
        (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤
    max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)

Tactic:
simp only [le_max_iff]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤ ↑(Fintype.card Fq) ^ (x - y).natDegree ∨
    ↑(Fintype.card Fq) ^ (x - z).natDegree ≤ ↑(Fintype.card Fq) ^ (y - z).natDegree
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:

Tactic:
_ ≤ (log x / log 2) * (log 4 * √x) := by
    gcongr
    rw [cast_sub]
    · trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)
    apply le_floor
    norm_cast
    apply one_le_div _ |>.mpr <;> bound
  _ = (log 4 / log 2) * x.sqrt * x.log := by field
  _ = _ := by
    congr
    rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]
    field

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x

Tactic:
gcongr 1

Goal state after:
case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * √x * log x ≤ 4 * x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ p ∣ p ^ 1

Tactic:
pow_one

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ p ∣ p
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case refine_3
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ↑⟨J, ⋯⟩ ∣ Ideal.span {(algebraMap R S) M}

Tactic:
apply (mul_dvd_mul_iff_left _).mp _

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 ℤ
ι : 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 := ⋯
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ Ideal S

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 := ⋯
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ?m.295 ≠ 0

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 := ⋯
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ?m.295 * ↑⟨J, ⋯⟩ ∣ ?m.295 * Ideal.span {(algebraMap R S) M}
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
have two_le_sqrt : 2 ≤ x.sqrt := le_sqrt_of_sq_le <| by norm_num [hx]
  have sqrt_le_x : x.sqrt ≤ x := sqrt_le_left (by linarith) |>.mpr (by bound)
  rw [← intervalIntegral.integral_add_adjacent_intervals (b := x.sqrt)]
  · grw [integral_1_div_log_sq_le two_le_sqrt (by linarith),
      integral_1_div_log_sq_le sqrt_le_x (by linarith)]
    rw [log_sqrt (by linarith), add_comm, div_pow, ← div_mul, mul_comm, mul_div_assoc]
    norm_num
    gcongr <;> linarith
  all_goals apply intervalIntegrable_one_div_log_sq <;> linarith

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
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : g ζ ^ p ^ i = ↑(⋯.unit ^ aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
H₁,

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))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i = ↑(⋯.unit ^ aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∀ j ≥ k, padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) < ε

Tactic:
intro j hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
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
ε : ℚ
hε : 0 < ε
⊢ ∀ j ≥ 1, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
intro j hj

Goal state after:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i) ^ 1

pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1

Tactic:
pow_one

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i)

case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∀ j ≥ n, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε

Tactic:
intro j hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∀ j ≥ n, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε

Tactic:
intro j hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε