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

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑S.u₄ - ↑(-1) = -(↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 - (S.Y ^ 3 + 1) - ↑S.u₄ * (λ ^ 2 * Z))

Tactic:
← hZ,

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑S.u₄ - ↑(-1) = -(↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 - (S.Y ^ 3 + 1) - ↑S.u₄ * (S.Z ^ 3 + 1))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
⊢ logHeight (x * y) ≤ logHeight x + logHeight y

Tactic:
by
  simp only [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact log_le_log (by positivity) <| mulHeight_mul_le ..

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

Goal state before:
pp: case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 < x
⊢ ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Tactic:
norm_of_nonneg (div_nonneg (sub_nonneg.mpr hx.1.le) (by positivity)),

Goal state after:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 < x
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ (Complex.ofReal ∘ fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) s = riemannZeta ↑s - 1 / (↑s - 1)

Tactic:
simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
      Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]

Goal state after:
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = riemannZeta ↑s
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
⊢ (χ * φ).ringHomComp (algebraMap F' FF') ≠ 1

Tactic:
exact (MulChar.ringHomComp_ne_one_iff hinj).mpr hχφ

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

Goal state before:
pp: ⊢ riemannZeta₀ 1 = ↑γ

Tactic:
simp [riemannZeta₀]

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
← ringHomComp_inv,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ.ringHomComp (algebraMap F' FF'))⁻¹ (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ.ringHomComp (algebraMap F' FF'))⁻¹ (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
← ringHomComp_inv,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ.ringHomComp (algebraMap F' FF'))⁻¹ (φ.ringHomComp (algebraMap F' FF'))⁻¹) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ deriv riemannZeta s / riemannZeta s + (s - 1)⁻¹ - ↑γ) =O[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
suffices (fun s ↦ (deriv riemannZeta₁ s) / (riemannZeta₁ s) - γ) =O[𝓝 1] (· - 1) by
    refine (this.mono nhdsWithin_le_nhds).congr' ?_ .rfl
    filter_upwards [log_deriv_riemannZeta_eq_neg_inv_sub_add]
    simp +contextual
  suffices DifferentiableAt ℂ (fun s ↦ (deriv riemannZeta₁ s) / (riemannZeta₁ s)) 1 by
    simpa using this.isBigO_sub
  fun_prop (disch := simp)

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 : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : R[X]
⊢ (h.lift i x hx) (h.map z) = eval₂ i x z

Tactic:
by
  simp [lift, h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ rfl]

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
a✝ : Nontrivial R
⊢ ↑n < f.degree

Tactic:
contrapose! hdeg

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 : ℕ
a✝ : Nontrivial R
hdeg : f.degree ≤ ↑n
⊢ f.natDegree ≤ n
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ ↑R[α] = Set.univ

Tactic:
hα₂,

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ ↑⊤ = Set.univ
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case a
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
a✝ : p ∈ N.primeFactors
⊢ ↑p ^ (-s) = 1 ↑p * ↑p ^ (-s)

Tactic:
MulChar.one_apply <| isUnit_of_subsingleton _,

Goal state after:
case a
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
a✝ : p ∈ N.primeFactors
⊢ ↑p ^ (-s) = 1 * ↑p ^ (-s)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = ↑(bernoulli k)

Tactic:
Polynomial.eval_zero_map,

Goal state after:
k : ℕ
⊢ (algebraMap ℚ ℝ) (Polynomial.eval 0 (Polynomial.bernoulli k)) = ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k).re

Tactic:
· norm_cast
    lia

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k + 1).re

Tactic:
· norm_cast
    lia

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

Goal state before:
pp: case inr
k : ℕ
hk : k ≠ 0
⊢ -1 / (↑k + 1) * Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
Polynomial.eval_zero_map,

Goal state after:
case inr
k : ℕ
hk : k ≠ 0
⊢ -1 / (↑k + 1) * (algebraMap ℚ ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) =
    -↑(bernoulli' (k + 1)) / (↑k + 1)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))

Tactic:
Polynomial.eval_zero_map,

Goal state after:
case e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      (algebraMap ℚ ℝ) (Polynomial.eval 0 (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(p / 2)! ≠ 0

Tactic:
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ p / 2 < p
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
⊢ IsDiscrete R

Tactic:
by_cases H : DenselyOrdered (ValueGroupWithZero R)
    · classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range
    · rw [isNontrivial_iff_nontrivial_units] at h
      rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] at H
      rw [nonempty_orderIso_withZeroMul_int_iff] at H
      exact H.left

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : b ≠ 0
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Tactic:
by
    rw [← neZero_iff] at hb; exact eq_zero_iff_not_coprime.2 h

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Compact

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
hN : N.FG
⊢ IsCompact ↑N

Tactic:
obtain ⟨s, hs⟩ := hN
  have : LinearMap.range (Fintype.linearCombination R (α := s) Subtype.val) = N := by
    simp [hs]
  rw [← this]
  refine isCompact_range ?_
  simp only [Fintype.linearCombination, Finset.univ_eq_attach, LinearMap.coe_mk,
    AddHom.coe_mk]
  fun_prop

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

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ε * t ^ (-s) ≤ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s))

Tactic:
by
      rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
      · exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one
      · exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

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

Tactic:
replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv

Goal state after:
case succ
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

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

Tactic:
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.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e * a') | b) = J(↑(2 ^ e * a') | b % (4 * a))

Tactic:
rw [Nat.cast_mul, mul_left, mul_left, quadratic_reciprocity' ha₁ hb,
    quadratic_reciprocity' ha₁ hb', Nat.cast_pow, pow_left, pow_left, Nat.cast_two, at_two hb,
    at_two hb']

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ χ₈ ↑b ^ e * (qrSign b a' * J(↑b | a')) = χ₈ ↑(b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: 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 : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
⊢ {x | (valuation K).restrict x ≤ (valuation K).restrict γ} =
    ⇑(Homeomorph.mulLeft₀ (γ / r) ⋯) '' {x | Valued.v.restrict x ≤ (valuation K).restrict r}

Tactic:
refine .trans ?_ (Equiv.image_eq_preimage_symm _ _).symm

Goal state after:
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 : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
⊢ {x | (valuation K).restrict x ≤ (valuation K).restrict γ} =
    ⇑(Homeomorph.mulLeft₀ (γ / r) ⋯).symm ⁻¹' {x | Valued.v.restrict x ≤ (valuation K).restrict r}
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case c0
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure

pp: case h
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n

Tactic:
· exact mahlerMeasure_nonneg _

Goal state after:
case h
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
x✝ : ℂ
hz : x✝ ∈ primitiveRoots n ℂ
⊢ ‖x✝‖ ≤ 1

Tactic:
exact (IsPrimitiveRoot.norm'_eq_one (isPrimitiveRoot_of_mem_primitiveRoots hz) hn).le

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
by
  dsimp [lucasLehmerResidue] at h
  rw [sZMod_eq_s p'] at h
  replace h : 2 ^ (p' + 2) - 1 ∣ s p' := by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h
  obtain ⟨k, h⟩ := h
  use k
  replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h
  rw [closed_form] at h
  replace h := congr_arg (fun x => ω ^ 2 ^ p' * x) h
  have t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1) := by ring
  rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h
  rw [mul_comm, coe_mul] at h
  rw [mul_comm _ (k : X (q (p' + 2)))] at h
  replace h := eq_sub_of_add_eq h
  have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide)
  exact mod_cast h

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
⊢ IsCyclic ↥H ↔ DiscreteTopology ↥H

Tactic:
nontriviality G using isCyclic_of_subsingleton, Subsingleton.discreteTopology

Goal state after:
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ IsCyclic ↥H ↔ DiscreteTopology ↥H
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mp
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx : x ∈ Gamma1' N
hxx : ⟨x, hx⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
Gamma1_to_Gamma0_mem

Goal state after:
case mp
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ⟨x, hx✝⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
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
h : w 0 = 0
⊢ ∀ (x : Fin 2), w x = 0 x

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case coe
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
⊢ g • ↑c = ↑c ↔ ↑c = g.parabolicFixedPoint

Tactic:
suffices g 1 0 * c ^ 2 + (g 1 1 - g 0 0) * c - g 0 1 = 0 ↔ c = g.parabolicFixedPoint by
      simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]
    by_cases hc : g 1 0 = 0
    · have hd : g 1 1 = g 0 0 := by grind
      suffices g 0 1 ≠ 0 by simpa [parabolicFixedPoint, hc, hd]
      -- can't have `g 0 1 ≠ 0` since that would force `g` to be scalar
      refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_
      simp [fixpointPolynomial, hb, hc, hd]
    · have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind
      simpa [parabolicFixedPoint, if_neg hc, sq, sub_eq_add_neg]
        using quadratic_eq_zero_iff_of_discrim_eq_zero hc this c

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN✝ : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) Γ(M)
x : SL(2, ℤ)
hx : x ∈ Γ(N)
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)

Tactic:
obtain ⟨y, hy, hy'⟩ := Subgroup.mem_inv_pointwise_smul_iff.mp <| hN' ⟨x, hx, rfl⟩

Goal state after:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN✝ : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) Γ(M)
x : SL(2, ℤ)
hx : x ∈ Γ(N)
y : SL(2, ℤ)
hy : y ∈ ↑Γ(M)
hy' : (mapGL ℝ) y = toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ) x
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: case refine_3.inl
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) 0‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖

Tactic:
refine ⟨0, by simpa only [norm_zero] using exp_nonneg _, le_rfl⟩

Goal state after: