mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ False

Tactic:
apply h3b
    rw [add_assoc, add_comm (b ^ 3), ← add_assoc] at HF
    exact dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT Int.prime_three h3a h3c HF

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)

Tactic:
by
  by_cases ha : a = 0
  · have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
    simp only [ha, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero, zero_pow this.ne']
  · rw [quadraticChar_eq_pow_of_char_ne_two hF ha]
    by_cases ha' : a ^ (Fintype.card F / 2) = 1
    · simp only [ha', if_true, Int.cast_one]
    · have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
      simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
      exact Eq.symm

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3

Tactic:
intro H
  refine fermatLastTheoremThree_of_three_dvd_only_c (fun a b c hc ha hb ⟨x, hx⟩ hcoprime h ↦ ?_)
  refine H a b c 1 (by simp [hc]) (fun hdvd ↦ ha ?_) (fun hdvd ↦ hb ?_) ?_ ?_ ?_
  · rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd
  · rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd
  · exact dvd_trans hζ.toInteger_sub_one_dvd_prime' ⟨x, by simp [hx]⟩
  · exact IsCoprime.intCast hcoprime
  · simpa using mod_cast h

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Tactic:
rw [Nat.ModEq.comm]

Goal state after:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ↑a.val ^ 2 ^ (n + 1) + 1 = 0

Tactic:
natCast_val,

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ a.cast ^ 2 ^ (n + 1) + 1 = 0
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
n : ℕ
⊢ (∀ x ∈ Nat.cast '' s, ↑n ∣ x) ↔ ∀ m ∈ s, n ∣ m

Tactic:
Set.forall_mem_image,

Goal state after:
s : Set ℕ
n : ℕ
⊢ (∀ ⦃x : ℕ⦄, x ∈ s → ↑n ∣ ↑x) ↔ ∀ m ∈ s, n ∣ m
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ (∀ x ∈ Nat.cast '' s, x = 0) ↔ s ⊆ {0}

Tactic:
Set.forall_mem_image,

Goal state after:
s : Set ℕ
⊢ (∀ ⦃x : ℕ⦄, x ∈ s → ↑x = 0) ↔ s ⊆ {0}
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑2 ^ Nat.log 2 n = 2 ^ Nat.log 2 n

Tactic:
Nat.cast_ofNat

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ 2 ^ Nat.log 2 n = 2 ^ Nat.log 2 n
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n

Tactic:
by
  rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpaηb : p ∣ 1 * S.a + ↑η * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ ↑η ^ 2 - ↑η
⊢ (↑η ^ 2 - ↑η) * ↑η * ↑η = λ

Tactic:
calc _ = (-η.1 - 1 - η) * (-η - 1) := by rw [eta_sq, mul_assoc, ← pow_two, eta_sq]
  _ = 2 * η.1 ^ 2 + 3 * η + 1 := by ring
  _ = λ := by rw [eta_sq, coe_eta]; ring

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h₁ : IsCoprime (S.x * S.y) S.z
⊢ S.w ^ 3 * ↑S.u = S.x * S.y * S.z

Tactic:
by rw [x_mul_y_mul_z_eq_u_mul_w_cube S, mul_comm]

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

Goal state before:
pp: case inr.refine_1
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
⊢ 1 = v (((x i)⁻¹ • x) i)

Tactic:
simpa using (inv_mul_cancel₀ <| v.ne_zero_iff.mpr hi).symm

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n + 1) ^ (-(s + 1) + 1) - ↑n ^ (-(s + 1) + 1)) / (-(s + 1) + 1)) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ ContinuousOn termTSum (Ici 1)

Tactic:
by
  -- We use dominated convergence, using `fun n ↦ term n 1` as our uniform bound (since `term` is
  -- monotone decreasing in `s`.)
  refine continuousOn_tsum (fun i ↦ continuousOn_term _) term_tsum_one.summable (fun n s hs ↦ ?_)
  rw [term, term, norm_of_nonneg]
  · simp_rw [intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]
    refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)
    · exact (term_welldef n.succ_pos (zero_lt_one.trans_le hs)).1
    · exact (term_welldef n.succ_pos zero_lt_one).1
    · have : 1 ≤ x := le_trans (by simp) hx.1.le
      gcongr
      · exact sub_nonneg.mpr hx.1.le
      · exact hs
  · rw [intervalIntegral.integral_of_le (by linarith)]
    refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ div_nonneg ?_ (rpow_nonneg ?_ _))
    all_goals linarith [hx.1]

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
f : 𝓞 K →ₗ[𝓞 K] 𝓞 K := LinearMap.mulLeft (𝓞 K) ↑n
hf : Function.Injective ⇑↑f
H₁ : span {↑n * ↑m} = Submodule.map f (span {↑m})
H₂ : span {↑(n * m), ↑n * a} = Submodule.map f (span {↑m, a})
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, a})) =
    (Submodule.map f (span {↑m})).toAddSubgroup.relIndex (Submodule.map f (span {↑m, a})).toAddSubgroup

Tactic:
exact AddSubgroup.relIndex_map_map_of_injective _ _ hf |>.symm

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ ∀ᶠ (s : ℂ) in 𝓝[≠] 1, (riemannZeta s)⁻¹ = (s - 1) * (riemannZeta₁ s)⁻¹

Tactic:
by
  filter_upwards [eventually_mem_nhdsWithin,
    riemannZeta₁_ne_zero_of_near_one.filter_mono nhdsWithin_le_nhds] with s hs
  simp [riemannZeta_eq_inv_sub_mul hs, field]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
⊢ h.modByMonicHom (h.root ^ n) = X ^ n

Tactic:
nontriviality R

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.root ^ n) = X ^ n
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
⊢ (fun x ↦ Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp.coeff ⋯)
      ((fun g ↦ h.map { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }) g) =
    g

Tactic:
nontriviality R

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
⊢ (fun x ↦ Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp.coeff ⋯)
      ((fun g ↦ h.map { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }) g) =
    g
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
⊢ (h.modByMonicHom z).coeff i = 0

Tactic:
nontriviality R

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
a✝ : Nontrivial R
⊢ (h.modByMonicHom z).coeff i = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : R[α] = ⊤
monic : (minpoly R α).Monic
this✝ : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
φ : AdjoinRoot (minpoly R α) →ₐ[R] S := AdjoinRoot.liftAlgHom (minpoly R α) (Algebra.ofId R S) α ⋯
⊢ Module.finrank R (AdjoinRoot (minpoly R α)) ≤ Module.finrank R S

Tactic:
nontriviality R

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : R[α] = ⊤
monic : (minpoly R α).Monic
this✝ : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
φ : AdjoinRoot (minpoly R α) →ₐ[R] S := AdjoinRoot.liftAlgHom (minpoly R α) (Algebra.ofId R S) α ⋯
a✝ : Nontrivial R
⊢ Module.finrank R (AdjoinRoot (minpoly R α)) ≤ Module.finrank R S
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
h : ∀ (x : ℝ), f k x = 0
⊢ bernoulliFun k (↑m * x) = ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)

Tactic:
rw [← sub_eq_zero]

Goal state after:
k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
h : ∀ (x : ℝ), f k x = 0
⊢ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m) = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n ↦ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) = fun n ↦
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * (fourier 0) ↑x

Tactic:
· ext1 n
    rw [Int.cast_neg, mul_add, ← mul_assoc]
    conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
    congr 2
    rw [div_mul_eq_mul_div₀, one_mul]
    congr 1
    rw [eq_div_iff, ← mul_pow, ← neg_eq_neg_one_mul, neg_neg, one_pow]
    apply pow_ne_zero; rw [neg_ne_zero]; exact one_ne_zero

Goal state after:
case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * (fourier 0) ↑x
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re) / ↑n

Tactic:
refine div_nonneg ?_ n.cast_nonneg

Goal state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ ‖χ ↑n‖ * ‖↑n ^ (-(I * ↑y))‖ = 1

Tactic:
← hn'.unit_spec,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ ‖χ ↑hn'.unit‖ * ‖↑n ^ (-(I * ↑y))‖ = 1
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
⊢ t ≠ 1 ∨ ∑ j, 𝓕 Φ j = 0

Tactic:
exact ht.2.imp_right (fun h ↦ by simp only [← dft_apply_zero, dft_dft, neg_zero, h, smul_zero])

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

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
| fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)

Tactic:
pk

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
pk : Nat.Primes × ℕ
| (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ ∃ x, ∃ (_ : x ∈ Ico 1 (p / 2).succ), (a * ↑x).valMinAbs.natAbs = b

Tactic:
refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ 1 ≤ (↑b / a).valMinAbs.natAbs

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (↑b / a).valMinAbs.natAbs < (p / 2).succ

case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * ↑(↑b / a).valMinAbs.natAbs).valMinAbs.natAbs = b
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) =
    ∑ x ∈ Ico 1 (p / 2).succ, ↑((↑a * ↑x).valMinAbs + ↑(if (↑a * ↑x).val ≤ p / 2 then 0 else p))

Tactic:
simp only [(val_eq_ite_valMinAbs _).symm]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) = ∑ x ∈ Ico 1 (p / 2).succ, ↑↑(↑a * ↑x).val
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)

Tactic:
by
  induction n with
  | zero =>
    simp only [pow_zero, Ideal.one_eq_top]
    exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)
  | succ n ih =>
    have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)
    replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
    suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
      .of_ideal_quotient (.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
    exact @Finite.of_equiv _ _ h
      ((Ideal.quotEquivPowQuotPowSuccEquiv (IsPrincipalIdealRing.principal 𝓂[K])
        (IsDiscreteValuationRing.not_a_field _) n).trans
        (Ideal.powQuotPowSuccEquivMapMkPowSuccPow _ n))

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ -(↑s).re < -1

Tactic:
ofReal_re,

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ -s < -1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
IH (a / 2) (a.div_lt_self ha0 (by decide)) hb2 hb1

Goal state after:
case ind.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑(a / 2) | b) else J(↑(a / 2) | b)) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : 1 ≤ r
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

Tactic:
· refine ⟨r', hr', hr, .trans ?_ hrs⟩
      intro x hx
      dsimp at hx ⊢
      exact hx.trans_lt (hr.trans_le hr1)

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : H.FiniteIndex
hH : DiscreteTopology ↥H
this : IsOpen[inst✝³] ↑H
⊢ Filter.map Subtype.val (pure 1) = pure ↑1

Tactic:
map_pure

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : H.FiniteIndex
hH : DiscreteTopology ↥H
this : IsOpen[inst✝³] ↑H
⊢ pure ↑1 = pure ↑1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∀ (x : Fin 2), ((w 1)⁻¹ • w) x = ![(w 1)⁻¹ * w 0, 1] x

Tactic:
simp [inv_mul_cancel₀ h₀]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f : ℍ → ℂ
c : ℂ
⊢ (c • f) ∣[k] A = (σ A) c • f ∣[k] A

Tactic:
by
  ext τ : 1
  simp only [slash_apply, Pi.smul_apply, smul_eq_mul, map_mul, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t

Tactic:
hF𝒟

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ F * (g • τ).im ^ t ≤ F * max τ.im (1 / τ.im) ^ t
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|
⊢ ∀ (g' : SL(2, ℤ)), ↑↑g 1 = ↑g' 1 → |(↑g • z).re| ≤ |(g' • z).re|

Tactic:
intro g1

Goal state after:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|
g1 : SL(2, ℤ)
⊢ ↑↑g 1 = ↑g1 1 → |(↑g • z).re| ≤ |(g1 • z).re|
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ Summable fun x ↦ ‖eisSummand k x z‖

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast

Goal state after:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ Summable fun x ↦ ‖eisSummand k x z‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
hk' : 2 < ↑k
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)