mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ λ ^ (3 * (S.multiplicity - 1)) * ↑S.u₅ * S.X ^ 3 = λ ^ 2 * λ ^ (3 * S.multiplicity - 5) * ↑S.u₅ * S.X ^ 3

Tactic:
rw [this, pow_add]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (logHeight fun I ↦ ∏ a, x a (I a)) = ∑ a, logHeight (x a)

Tactic:
simp only [logHeight_eq_log_mulHeight]
  rw [← log_prod fun a _ ↦ mulHeight_ne_zero _]
  exact congrArg log <| mulHeight_fun_prod_eq hx

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ totalWeight K = Module.finrank ℚ K

Tactic:
by
  rw [totalWeight_eq_sum_mult, InfinitePlace.sum_mult_eq]

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

Goal state before:
pp: this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ riemannZeta 1 ≠ 0

Tactic:
by
    simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
      push_cast]

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

Goal state before:
pp: case inl
⊢ riemannZeta ((starRingEnd ℂ) 1) = (starRingEnd ℂ) (riemannZeta 1)

pp: case inr
s : ℂ
hs : s ≠ 1
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)

Tactic:
· have h : riemannZeta 1 = ((γ - Real.log (4 * π)) / 2 : ℝ) := by
      rw [riemannZeta_one, ofReal_div, ofReal_sub, ofReal_log (by positivity : (0 : ℝ) ≤ 4 * π)]
      norm_cast
    rw [map_one, h, conj_ofReal]

Goal state after:
case inr
s : ℂ
hs : s ≠ 1
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (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')
Hχφ : χ' * φ' ≠ 1
⊢ χ'⁻¹ * φ'⁻¹ ≠ 1

Tactic:
← mul_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
⊢ (χ' * φ')⁻¹ ≠ 1
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
⊢ ↑(Fintype.card F) * ↑(Fintype.card F) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * ↑(Fintype.card F)

Tactic:
← mul_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
⊢ ↑(Fintype.card F) * ↑(Fintype.card F) = gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * ↑(Fintype.card F)
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this : IsDomain (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 1 ∨ ∑ j, χ j = 0

Tactic:
have := χ.sum_eq_zero_of_ne_one

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : χ ≠ 1 → ∑ a, χ a = 0
⊢ s ≠ 1 ∨ ∑ j, χ j = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case hf
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := ⋯
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ bernoulliFun (k + 1) (↑m * x)) (↑m * (↑k + 1) * bernoulliFun k (↑m * x)) x

pp: case hg
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := ⋯
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ ∑ x_1 ∈ Finset.range m, ↑m ^ k * bernoulliFun (k + 1) (x + ↑x_1 / ↑m))
    (∑ x_1 ∈ Finset.range m, ↑m ^ k * (↑k + 1) * bernoulliFun k (x + ↑x_1 / ↑m)) x

Tactic:
· rw [mul_assoc, mul_comm (m : ℝ) _, ← Nat.cast_add_one]
        exact (hasDerivAt_bernoulliFun _ _).comp _ (hasDerivAt_const_mul ..)

Goal state after:
case hg
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := ⋯
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ ∑ x_1 ∈ Finset.range m, ↑m ^ k * bernoulliFun (k + 1) (x + ↑x_1 / ↑m))
    (∑ x_1 ∈ Finset.range m, ↑m ^ k * (↑k + 1) * bernoulliFun k (x + ↑x_1 / ↑m)) x
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : Φ 0 = 0
⊢ DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
simp only [h, funext zero_div, differentiableAt_const]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
⊢ LSeries (-f) s = -LSeries f s

Tactic:
simp [LSeries, term_neg_apply, tsum_neg]

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ term (f - g) s = term f s - term g s

Tactic:
simp_rw [sub_eq_add_neg, term_add, term_neg]

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

Goal state before:
pp: case e_a
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s = LSeries (⇑↑zeta) s

pp: case e_a
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun x ↦ B.χ ↑x) s = LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

Tactic:
· simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]

Goal state after:
case e_a
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun x ↦ B.χ ↑x) s = LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_2.refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 0 ≤ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)

pp: case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2) ≤ 2 * ↑↑p ^ (-(3 / 2))

Tactic:
· positivity [sub_pos.mpr (hp₁ p)]

Goal state after:
case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2) ≤ 2 * ↑↑p ^ (-(3 / 2))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))

Tactic:
refine tendsto_tsum_of_dominated_convergence hys.norm hc <| eventually_iff.mpr ?_

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ {x | ∀ (k : ℕ), ‖F x k‖ ≤ ‖F y k‖} ∈ atTop
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] fun x ↦ LSeries g ↑x
n : ℕ
hn : n ≠ 0
⊢ f n = g n

Tactic:
have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
    LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h
  have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
    lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg
  simpa only [Pi.sub_apply, sub_eq_zero]
    using (LSeries_eventually_eq_zero_iff'.mp hsub).resolve_right ha n hn

Goal state after:
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 | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑a * ↑x).valMinAbs.natAbs) =
    ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, x)

Tactic:
rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
              Finset.sum_eq_multiset_sum]

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

Tactic:
have hx0 : x ≠ 0 := by simp [x]

Goal state after:
case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ∀ a_1 ∈ b.primeFactorsList, ∀ (h₁ h₂ : Nat.Prime a_1), legendreSym a_1 a = legendreSym a_1 (a % ↑b)

Tactic:
rintro p hp _ h₂

Goal state after:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
⊢ legendreSym p a = legendreSym p (a % ↑b)
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
⊢ LocallyIntegrableOn S (Set.Ici 1) volume

Tactic:
simpa using locallyIntegrableOn_mul_sum_Icc f zero_le_one (locallyIntegrableOn_const 1)

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

Goal state before:
pp: case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
this : ∃ t, t.Finite ∧ ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]

Tactic:
obtain ⟨t, ht, ht'⟩ := this

Goal state after:
case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Set.univ ⊆ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t

Tactic:
rintro ⟨x⟩

Goal state after:
case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t
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
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K
val✝ : LocallyFiniteOrder (↥(MonoidHom.mrange Valued.v))ˣ
e : ↥(MonoidHom.mrange (valuation K)) ≃*o ValueGroupWithZero K :=
  { toMulEquiv := MulEquiv.ofBijective (MonoidHom.mrange (valuation K)).subtype ⋯, map_le_map_iff' := ⋯ }
⊢ Nonempty (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))

Tactic:
have : Nontrivial (ValueGroupWithZero K)ˣ := isNontrivial_iff_nontrivial_units.mp inferInstance

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
this✝¹ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this✝ : IsUniformAddGroup K
val✝ : LocallyFiniteOrder (↥(MonoidHom.mrange Valued.v))ˣ
e : ↥(MonoidHom.mrange (valuation K)) ≃*o ValueGroupWithZero K :=
  { toMulEquiv := MulEquiv.ofBijective (MonoidHom.mrange (valuation K)).subtype ⋯, map_le_map_iff' := ⋯ }
this : Nontrivial (ValueGroupWithZero K)ˣ
⊢ Nonempty (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : b = 0
⊢ J(a | b) = 1

pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ J(a | b) = 0

pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
⊢ J(a | b) =
    have this := ⋯;
    fastJacobiSym a (b / 2)

pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
⊢ J(a | b) = 1

pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % ↑b = 0
⊢ J(a | b) = 0

pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯

Tactic:
· rw [hb0, zero_right]

Goal state after:
case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ J(a | b) = 0

case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
⊢ J(a | b) =
    have this := ⋯;
    fastJacobiSym a (b / 2)

case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
⊢ J(a | b) = 1

case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % ↑b = 0
⊢ J(a | b) = 0

case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 y : A},
    (x_1 ∈ Set.range fun x_2 ↦ x * x_2) → (y ∈ Set.range fun x_2 ↦ x * x_2) → x_1 + y ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x✝ : A
hx1✝ : x✝ ∈ Subring.center A
hx1 : ∀ (g : A), g * x✝ = x✝ * g
hx2 : x✝ ≠ 0
x y : A
⊢ (fun x ↦ x✝ * x) x + (fun x ↦ x✝ * x) y ∈ Set.range fun x ↦ x✝ * x
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Tactic:
let I := TwoSidedIdeal.mk' (Set.range (x * ·)) ⟨0, by simp⟩
      (by rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x + y, mul_add _ _ _⟩)
      (by rintro _ ⟨x, rfl⟩; exact ⟨-x, by simp⟩)
      (by rintro a _ ⟨c, rfl⟩; exact ⟨a * c, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩)
      (by rintro _ b ⟨a, rfl⟩; exact ⟨a * b, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩)

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p : ℕ
⊢ sMod p 0 % (2 ^ p - 1) = sMod p 0

Tactic:
simp [sMod]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p n✝ : ℕ
⊢ sMod p (n✝ + 1) % (2 ^ p - 1) = sMod p (n✝ + 1)

Tactic:
simp [sMod]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ (1 + α) ^ 2 = 2 * ω

Tactic:
ext <;> simp [α, ω, sq] <;> norm_num

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

Goal state before:
pp: case insert
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
⊢ (∏ i ∈ insert i t, f i) ∣[∑ i ∈ insert i t, k i] g =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#(insert i t)) - 1) • ∏ i ∈ insert i t, f i ∣[k i] g

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case insert.inl
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
hi : i ∉ ∅
IH : (∏ i ∈ ∅, f i) ∣[∑ i ∈ ∅, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#∅) - 1) • ∏ i ∈ ∅, f i ∣[k i] g
⊢ (∏ i ∈ insert i ∅, f i) ∣[∑ i ∈ insert i ∅, k i] g =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#(insert i ∅)) - 1) • ∏ i ∈ insert i ∅, f i ∣[k i] g

case insert.inr
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ (∏ i ∈ insert i t, f i) ∣[∑ i ∈ insert i t, k i] g =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#(insert i t)) - 1) • ∏ i ∈ insert i t, f i ∣[k i] g
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| ≠ 0 ∨ 1 + (↑(#t) - 1) ≠ 0 ∨ 1 = 0 ∧ ↑(#t) - 1 = 0

Tactic:
left

Goal state after:
case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: case mp
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ Γ, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ s
⊢ f ∣[k] γ = f

Tactic:
exact h γ (hΓ ▸ Subgroup.mem_closure_of_mem hγ)

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(map (mapGL ℝ) Γ).strictPeriods

Tactic:
rw [hsp]

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
⊢ ↑(g • z) =
    ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))

Tactic:
by
  have nonZ1 : (p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2 ≠ 0 := mod_cast hp.sq_add_sq_ne_zero
  have : ((↑) : ℤ → ℝ) ∘ p ≠ 0 := fun h => hp.ne_zero (by ext i; simpa using congr_fun h i)
  have nonZ2 : (p 0 : ℂ) * z + p 1 ≠ 0 := by simpa using linear_ne_zero z this
  subst hg
  rw [coe_specialLinearGroup_apply]
  replace nonZ2 : z * (g 1 0 : ℂ) + g 1 1 ≠ 0 := by convert! nonZ2 using 1; ring
  have H := congr(Int.cast (R := ℂ) $(det_fin_two g))
  simp at H
  simp [field]
  linear_combination -((z : ℂ) * (g 1 1 : ℂ) - g 1 0) * H

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

Goal state before:
pp: case pos
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 • τ ∈ 𝒟
hg : ↑g 1 0 = 0
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)

Tactic:
have : g 1 1 ≠ 0 := fun hg' ↦ zero_ne_one <| by
      simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe

Goal state after:
case pos
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 • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this : ↑g 1 1 ≠ 0
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)