mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left✝ : k < n
hk : χ x = μ ^ k
⊢ ∃ z ∈ ℤ[μ], χ x - 1 = z * (μ - 1)

Tactic:
refine hk ▸ ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left✝ : k < n
hk : χ x = μ ^ k
⊢ ∑ x ∈ range k, μ ^ x ∈ ℤ[μ]
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✝³ : Ring T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ ((h.ofAlgEquiv e).algEquiv h'') a = (e.symm.trans (h.algEquiv h'')) a

Tactic:
simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
⊢ x ∈ (fun a ↦ ↑a / ↑n) '' {a | mulHeight ![↑a, ↑n] ≤ B}

Tactic:
simp only [Set.mem_ofPred_eq, Set.mem_image]

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
⊢ ∃ x_1, mulHeight ![↑x_1, ↑n] ≤ B ∧ ↑x_1 / ↑n = x
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 : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z - w) = 0

Tactic:
hy,

Goal state after:
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 : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (f * y) = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case h
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
i✝ i : Fin f.natDegree
hm : f.natDegree ≤ ↑i
⊢ False

Tactic:
exact i.prop.not_ge hm

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
| 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) =
    -1 + (-↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2

Tactic:
enter [1, 2, 2, x]

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
x : F
| (χ x - 1) * (ψ (1 - x) - 1)
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
        exact finrank_quotient_span_eq_natDegree' monic ▸ minpoly.natDegree_le α

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ * χ⁻¹) (-1) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s

Tactic:
mul_inv_cancel,

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * 1 (-1) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : (normalizedFactors (Ideal.map (algebraMap R S) I)).prod = Ideal.map (algebraMap R S) I
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
hy,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : {y}.prod = Ideal.map (algebraMap R S) I
⊢ Irreducible (Ideal.map (algebraMap R S) I)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case e_a.e_f.inl
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
x : ℝ
hx : x ≥ y
⊢ (if n + 1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) (n + 1)) = F x (n + 1)

Tactic:
simp [hF₀ x le_rfl]

Goal state after:
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 ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))

Tactic:
convert! (show 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 by positivity) using 1

Goal state after:
case e'_4
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
⊢ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2)) =
    2 * a ^ n * ((z ^ n).re + 1) ^ 2
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (cexp (2 * ↑π * I * -↑x✝ * ↑x) - cexp (2 * ↑π * I * ↑x✝ * ↑x)) * I / 2 =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2

Tactic:
congr 4

Goal state after:
case e'_3.e_a.e_a.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 2 * ↑π * I * -↑x✝ * ↑x = -(2 * ↑π * ↑x✝ * ↑x) * I

case e'_3.e_a.e_a.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 2 * ↑π * I * ↑x✝ * ↑x = 2 * ↑π * ↑x✝ * ↑x * I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
⊢ J(a | 1) = 1

Tactic:
by
  simp only [jacobiSym, primeFactorsList_one, List.prod_nil, List.pmap]

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

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), ↑a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs

Tactic:
intCast_zmod_eq_zero_iff_dvd,

Goal state after:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (_ : a_1 ∈ b.primeFactorsList), ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ ϖ ∣ x

Tactic:
exact ⟨y, hy⟩

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

Goal state before:
pp: a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₂ % ↑b | b) = J(a₂ | b)

Tactic:
← mod_left

Goal state after:
a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₂ | b) = J(a₂ | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr.e_a.e_a
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'
⊢ qrSign b a' = qrSign (b % (4 * a)) a'

Tactic:
simp_rw [qrSign]

Goal state after:
case inr.e_a.e_a
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(χ₄ ↑b | a') = J(χ₄ ↑(b % (4 * a)) | a')
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
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ a * y = x * y * a * y

Tactic:
hy,

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) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ a * y = 1 * a * y
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
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * (x * y)) = y * a

Tactic:
hy,

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) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * 1) = y * a
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
⊢ conjGL Γ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) = toConjAct g⁻¹ • Γ

Tactic:
by
  ext x
  simp_rw [mem_conjGL, ← map_inv, ← map_mul, toGL_injective.eq_iff, map_intCast_injective.eq_iff,
    exists_eq_right, toConjAct_inv, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]

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

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
· by_cases hn : Even (Fintype.card n)
    · convert! HasDetPlusMinusOne.det_eq hg using 1 <;>
        simp [Units.ext_iff, det_neg, hn]
    · convert! (HasDetPlusMinusOne.det_eq hg).symm using 1 <;>
        simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : ↑z.det = ↑y.det
⊢ z.det = 1

Tactic:
hy,

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : ↑z.det = ↑1
⊢ z.det = 1
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
⊢ (σ A) (f (A • x)) * (σ A) (g (A • x)) * d ^ (k1 + k2 - 1) * (denom A ↑x ^ (-k1) * denom A ↑x ^ (-k2)) =
    d *
      ((σ A) (f (A • x)) * d ^ (k1 - 1) * denom A ↑x ^ (-k1) * ((σ A) (g (A • x)) * d ^ (k2 - 1) * denom A ↑x ^ (-k2)))

Tactic:
have h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1) := by
    have : d ≠ 0 := ofReal_ne_zero.mpr <| abs_ne_zero.mpr <| NeZero.ne _
    rw [← zpow_one_add₀ this, ← zpow_add₀ this]
    ring_nf

Goal state after:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ (σ A) (f (A • x)) * (σ A) (g (A • x)) * d ^ (k1 + k2 - 1) * (denom A ↑x ^ (-k1) * denom A ↑x ^ (-k2)) =
    d *
      ((σ A) (f (A • x)) * d ^ (k1 - 1) * denom A ↑x ^ (-k1) * ((σ A) (g (A • x)) * d ^ (k2 - 1) * denom A ↑x ^ (-k2)))
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0

pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0

Tactic:
· simpa [Subgroup.inf_relIndex_right] using h𝒢.1

Goal state after:
case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
x✝ : ℍ
⊢ (Function.const ℍ x ∣[0] g) x✝ = Function.const ℍ x x✝

Tactic:
simp [slash_def, σ, Subgroup.HasDetOne.det_eq hg]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : CuspForm Γ k₁
g : ModularForm Γ k₂
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
⊢ IsZeroAtImInfty ((f.mul g.toSlashInvariantForm).toFun ∣[k₁ + k₂] γ)

Tactic:
simpa [mul_slash] using!
      ((f.zero_at_cusps' hc γ hγ).mul_boundedAtFilter (g.bdd_at_cusps' hc γ hγ)).smul _

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r a)
⊢ ⟨↑v ᵥ* ↑(γ * γ⁻¹), ⋯⟩ = v

Tactic:
mul_inv_cancel,

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r a)
⊢ ⟨↑v ᵥ* ↑1, ⋯⟩ = v
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ i : ℕ
hi : i ∈ Finset.range (n✝ + 1)
⊢ (↑n✝.factorial)⁻¹ *
      (↑(n✝.choose i) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n✝ - i) (cuspFunction h g) 0) =
    (↑i.factorial)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n✝ - i).factorial)⁻¹ * iteratedDeriv (n✝ - i) (cuspFunction h g) 0)

Tactic:
Nat.cast_choose _ (by grind)

Goal state after:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ i : ℕ
hi : i ∈ Finset.range (n✝ + 1)
⊢ (↑n✝.factorial)⁻¹ *
      (↑n✝.factorial / (↑i.factorial * ↑(n✝ - i).factorial) * iteratedDeriv i (cuspFunction h f) 0 *
        iteratedDeriv (n✝ - i) (cuspFunction h g) 0) =
    (↑i.factorial)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n✝ - i).factorial)⁻¹ * iteratedDeriv (n✝ - i) (cuspFunction h g) 0)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ qExpansion h (f - g) = qExpansion h f - qExpansion h g

Tactic:
by
  have hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0 := by
    simpa [cuspFunction_neg hg.continuousAt] using hg.neg
  simpa [sub_eq_add_neg, qExpansion_neg hg] using (qExpansion_add hf hg')

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ qExpansion h f = 0 ↔ f = 0

Tactic:
by
  constructor
  · intro H
    ext z
    simp [← (hasSum_qExpansion hh hfper hfhol hfbdd z).tsum_eq, H]
  · intro H
    simpa [H] using qExpansion_zero h

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * ↑n ^ e)

Tactic:
simp only [F, norm_mul, norm_div, norm_real, norm_one, norm_pow, mul_assoc]

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ 1 / ‖h‖ * (1 / ‖𝕢 h (↑x + 1 / ↑n * I)‖ ^ n * ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * ↑n ^ e))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: z : ℍ
⊢ Function.Even fun x ↦ e2Summand x z

Tactic:
by
  intro n
  simp only [e2Summand, ← tsum_comp_neg (fun a ↦ eisSummand 2 ![-n, a] z)]
  apply tsum_congr (fun b ↦ ?_)
  simp only [eisSummand, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, Int.cast_neg, neg_mul, inv_inj]
  rw_mod_cast [Int.cast_neg]
  ring

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖2 • f x‖ = ‖f x‖

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}

Tactic:
norm_smul,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * (‖2‖ * ‖f x‖) = ‖f x‖

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : G2 ∣[2] (g * g⁻¹) = G2 ∣[2] g⁻¹ + (-D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
mul_inv_cancel,

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : G2 ∣[2] 1 = G2 ∣[2] g⁻¹ + (-D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹