mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
I4 :
  ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ + ↑δ
Q : Finset (Set X) := Finset.image (fun p ↦ p.snd ∩ s) (g.range.sigma P)
p : Set X
i : X
hi : p ∈ P (g i)
q : Set X
j : X
hj : q ∈ P (g j)
htu : p ∩ s ≠ q ∩ s
⊢ p ≠ q

Tactic:
grind only

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Monotone primesLE

Tactic:
by
  intros n m _ p
  simp [mem_primesLE]; grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !

Tactic:
← div_eq_iff (hne p),

Goal state after:
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)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ (∑ k ∈ range n, ↑k ^ p) / ↑p ! = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case e_a
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
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
⊢ ↑p ^ N = ↑p ^ (N - e + e)

Tactic:
Nat.sub_add_cancel hv

Goal state after:
case e_a
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
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
⊢ ↑p ^ N = ↑p ^ N
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case right
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)⌉₊)
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
by_cases h : A i₁ % b = A i₀ % b

Goal state after:
case pos
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
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

case neg
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
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case refine_2.refine_1.e_6
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 ι
ε : ℝ := ⋯
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := ⋯
s : ι →₀ R := ⋯
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := ⋯
rs : Fin (cardM bS adm).succ → ι → R := ⋯
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ⋯
r : R := ⋯
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ (bS.repr (∑ x, (rs k x • bS x - rs j x • bS x))) i = rs k i - rs j i

Tactic:
map_sum,

Goal state after:
case refine_2.refine_1.e_6
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 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ (∑ x, bS.repr (rs k x • bS x - rs j x • bS x)) i = rs k i - rs j i
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
zmodRepr_eq_zero_iff_dvd,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ = 1 ↔ ¬↑p ∣ x
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ ↑((autToPow R hμ) g) = ↑((modularCyclotomicCharacter L ⋯) g.toRingEquiv)

Tactic:
apply ZMod.val_injective

Goal state after:
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ (↑((autToPow R hμ) g)).val = (↑((modularCyclotomicCharacter L ⋯) g.toRingEquiv)).val
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inl
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✝ : Subsingleton R
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

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
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

Tactic:
· have : Subsingleton Rₘ := Module.subsingleton R Rₘ
    simp [eq_iff_true_of_subsingleton]

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
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inl
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✝ : Subsingleton R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

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
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
· have : Subsingleton Rₘ := Module.subsingleton R Rₘ
    simp [eq_iff_true_of_subsingleton]

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
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) = 2
⊢ p = 2

Tactic:
by
        rw [← pow_one 2] at hk
        exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk

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

Goal state before:
pp: case h
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = ↑⌊ξ⌋

Tactic:
Rat.intCast_inj,

Goal state after:
case h
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ u = ⌊ξ⌋
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.g (1 / x) = (P.ε⁻¹ * ↑(x ^ P.k)) • P.f x

Tactic:
(div_div_cancel₀ (one_ne_zero' ℝ) ▸ P.h_feq (1 / x) (one_div_pos.mpr hx) :),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.g (1 / x) = (P.ε⁻¹ * ↑(x ^ P.k)) • (P.ε * ↑((1 / x) ^ P.k)) • P.g (1 / x)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
hz : 0 < z.im
⊢ False

Tactic:
· have : ((-↑·) : ℕ → ℤ).Injective := fun _ _ ↦ by simp only [neg_inj, Nat.cast_inj, imp_self]
        replace h := (h.comp_injective this).tendsto_atTop_zero
        simp_rw [Function.comp_def, Int.cast_neg, Int.cast_natCast, mul_neg, neg_mul, neg_neg] at h
        refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
        exact tendsto_exp_atTop.comp ((tendsto_natCast_atTop_atTop.const_mul_atTop
          (mul_pos two_pos pi_pos)).atTop_mul_const hz)

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = Real.Gamma s.re / p i ^ s.re

Tactic:
norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)),

Goal state after:
case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ∫ (x : ℝ) in Ioi 0, ‖↑x ^ (s - 1) * ↑(rexp (-p i * x))‖ ∂volume = Real.Gamma s.re / p i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|))

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg (abs_nonneg _)) _)

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
rw [evenKernel_undef _ hx, cosKernel_undef, mul_zero]

Goal state after:
case inl.hx
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
hc2 : MellinConvergent P.f_modif s
hc3 : mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
this : mellin (fun t ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun x ↦ P.f x - P.f₀) s
⊢ mellin (fun x ↦ P.f x - P.f₀) s = P.Λ s

Tactic:
simp only [Λ, Λ₀] at *

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
hc2 : MellinConvergent P.f_modif s
hc3 : mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
this : mellin (fun t ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun x ↦ P.f x - P.f₀) s
⊢ mellin (fun x ↦ P.f x - P.f₀) s = mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / (↑P.k - s)) • P.g₀
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
⊢ P.Λ = mellin P.f

Tactic:
by
  ext s
  simp only [mellin, Λ, Λ₀, f_modif, hP.hf₀, sub_zero, hP.hg₀, smul_zero]
  refine integral_congr_ae <| (ae_restrict_iff' measurableSet_Ioi).mpr ?_
  filter_upwards [compl_mem_ae_iff.mpr (Subsingleton.measure_zero (s := {1}) (by simp) _)]
    with t (ht₁ : t ≠ 1) (ht₀ : 0 < t)
  by_cases ht : t < 1 <;> [rw [add_comm] ; skip] <;>
  rw [Pi.add_apply, indicator_of_mem (by grind), indicator_of_notMem (by grind), add_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
| (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)

Tactic:
enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
x : ℝ
| ‖↑(evenKernel a x) - if a = 0 then 1 else 0‖
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
⊢ False

Tactic:
refine ((one_half_le_sum_primes_ge_one_div k).trans_lt <| LE.le.trans_lt ?_ hk).false

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
⊢ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p ≤
    ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)

Tactic:
aux,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑0) / 0 / 2)
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
suffices DifferentiableAt ℂ
      (fun s ↦ completedHurwitzZetaEven a s / Gammaℝ s - 1 / (s - 1) / Gammaℝ s) 1 by
    apply this.congr_of_eventuallyEq
    filter_upwards [eventually_ne_nhds one_ne_zero] with x hx
    rw [hurwitzZetaEven, Function.update_of_ne hx]
  simp_rw [← sub_div, div_eq_mul_inv _ (Gammaℝ _)]
  refine DifferentiableAt.mul ?_ differentiable_Gammaℝ_inv.differentiableAt
  simp_rw [completedHurwitzZetaEven_eq, sub_sub, add_assoc]
  conv => enter [2, s, 2]; rw [← neg_sub, div_neg, neg_add_cancel, add_zero]
  exact (differentiable_completedHurwitzZetaEven₀ a _).sub
    <| (differentiableAt_const _).div differentiableAt_id one_ne_zero

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n

Tactic:
intro _ _ _ ha hb hc

Goal state after:
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ a✝ ^ n + b✝ ^ n ≠ c✝ ^ n
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case mp
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 → k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
grind [mul_eq_zero]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
right
    exact ⟨hx, hy⟩

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4

Tactic:
exact fermatLastTheoremFour

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℕ
⊢ (algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
rw [← map_pow, ← val_pow_eq_pow_val]

Goal state after: