mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
x✝ : CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
left✝¹ : CompleteSpace ↥𝒪[K]
left✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ IsCompact Set.univ

Tactic:
rw [← totallyBounded_iff_finite_residueField] at h

Goal state after:
case refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
x✝ : CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
left✝¹ : CompleteSpace ↥𝒪[K]
left✝ : IsDiscreteValuationRing ↥𝒪[K]
h : TotallyBounded Set.univ
⊢ IsCompact Set.univ
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
cases i <;> simp [sMod]

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 - 1) * s * (Cs + ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1)) ≤
    (s - 1) * s * C + s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1))

Tactic:
rw [mul_add, ← mul_assoc, mul_comm s]
      gcongr

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this✝ : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this : X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p' = 0
⊢ (X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p').1 = 0

Tactic:
simp [this]

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

Goal state before:
pp: n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ) t = g ^ n
this : GeneralLinearGroup.det g ^ n = 1
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1

Tactic:
simp [this]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
⊢ ∃ a, a • w = ![1, 0]

Tactic:
use (w 0)⁻¹

Goal state after:
case h
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
⊢ (w 0)⁻¹ • w = ![1, 0]
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₂
hz_det : z.det = 1
i j : Fin 2
⊢ 1 i j + ↑((M • (A₁.num * k * A₂.num)) i j) = 1 i j

Tactic:
add_eq_left,

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₂
hz_det : z.det = 1
i j : Fin 2
⊢ ↑((M • (A₁.num * k * A₂.num)) i j) = 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : IsBoundedAtImInfty f
⊢ IsBoundedAtImInfty (f ∣[k] g)

Tactic:
rw [IsBoundedAtImInfty, BoundedAtFilter, ← Asymptotics.isBigO_norm_left] at hf ⊢

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : (fun x ↦ ‖f x‖) =O[atImInfty] 1
⊢ (fun x ↦ ‖(f ∣[k] g) x‖) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: case mpr
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ (∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ)) → c.IsBoundedAt f k

Tactic:
rintro ⟨γ, rfl, b⟩
    simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using! b

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

Goal state before:
pp: N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (↑N * ↑n +ᵥ z) = f z

Tactic:
by
  apply vAdd_apply_of_mem_strictPeriods
  simp [strictPeriods_Gamma, AddSubgroup.mem_zmultiples_iff, mul_comm]

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

Goal state before:
pp: N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (ModularGroup.T ^ (↑N * n) • z) = f z

Tactic:
by
  rw [modular_T_zpow_smul z (N * n)]
  simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.periods ≤ 𝒢.strictPeriods

Tactic:
periods_eq_zmultiples_widthInfty,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ AddSubgroup.zmultiples 𝒢.widthInfty ≤ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
i : ℤ
a : ModularForm Γ i
h : ⟨i, a⟩.fst = b.fst
h2 : mcast h ⟨i, a⟩.snd ⋯ = b.snd
⊢ ⟨i, a⟩ = b

Tactic:
cases h

Goal state after:
case refl
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
a : ModularForm Γ b.1
h2 : mcast ⋯ ⟨b.1, a⟩.snd ⋯ = b.snd
⊢ ⟨b.1, a⟩ = b
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n
⊢ 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left.inl.inl
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left.inl.inr
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left.inr.inl
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left.inr.inr
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right.inl.inl
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right.inl.inr
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right.inr.inl
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right.inr.inr
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith

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✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ ‖(starRingEnd ℂ) (f τ) * f τ * ↑τ.im ^ k‖ / (τ.im ^ (↑k / 2)) ^ 2

Tactic:
← Real.rpow_mul_natCast τ.im_pos.le

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ ‖(starRingEnd ℂ) (f τ) * f τ * ↑τ.im ^ k‖ / τ.im ^ (↑k / 2 * ↑2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ 9 * c ^ 4 ≤ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 * 16 ≤ 16

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«0»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«1»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«0»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«1»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : b = 0 ∨ b = 1 ∨ b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
rcases this with hb | hb | hb

Goal state after:
case inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
hb : b = 0
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
hb : b = 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
by
  have hb : g 0 1 = -1 := by
    simpa [-SpecialLinearGroup.det_coe, det_fin_two, hd, hc, neg_eq_iff_eq_neg] using g.property
  have hz' : ‖(z : ℂ)‖ = 1 :=
    le_antisymm (by simpa [denom, hc, hd] using hg') (one_le_normSq_iff.mp hz.1)
  have hg' : g = T ^ g 0 0 * S := by
    ext i j
    simp only [coe_mul, coe_S, coe_T_zpow, Matrix.mul_fin_two, mul_zero, mul_one, zero_add,
      one_mul, add_zero, zero_mul]
    fin_cases i <;> fin_cases j <;> tauto
  rw [hg', mul_smul] at hg
  have hSre : re (S • z) = -z.re := by
    rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
  have := hg.2
  rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, add_comm, coe_re, hSre] at this
  have := (abs_sub_abs_le_abs_add _ _).trans this
  rw [abs_neg, sub_le_iff_le_add] at this
  rcases lt_or_eq_of_le hz.2 with hzre | hzre
  · have := this.trans_lt ((add_lt_add_iff_left _).mpr hzre)
    rw [add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_lt] at this
    grind [Int.abs_lt_one_iff, zpow_zero]
  · rw [hzre, add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_le,
      Int.abs_le_one_iff] at this
    rcases this with h | h | h <;> simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this
    · grind [zpow_zero]
    · rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre <;> [skip; norm_num [hzre] at this]
      rw [h, zpow_one] at hg'
      refine .inr <| .inr ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) ?_⟩
      simp [hz', show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_ρ]
    · rw [abs_eq (by norm_num)] at hzre
      rcases hzre with hzre | hzre <;> [norm_num [hzre] at this; skip]
      rw [h, zpow_neg_one] at hg'
      exact .inr <| .inl ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) (by rw [hz', norm_ρ])⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
this : ↑g 0 0 = 0 ∨ ↑g 0 0 = 1
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T

Tactic:
by rcases this with h | h <;> simp [h]

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

Goal state before:
pp: z : ℍ
⊢ logDeriv η ↑z = ↑π * I / 12 * E2 z

Tactic:
unfold eta

Goal state after:
z : ℍ
⊢ logDeriv (fun z ↦ 𝕢 24 z * ∏' (n : ℕ), (1 - eta_q n z)) ↑z = ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ 2 < 3

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1».«1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [this]

Goal state after:
case «0».«1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ -↑g 0 0 - 1 = -1 - ↑g 0 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝² : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝¹ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
this✝ : 1 ≤ normSq ↑z
this : 0 ≤ -2 * z.re + 1
⊢ normSq ↑z = 1

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝² : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝¹ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
this✝ : 1 ≤ normSq ↑z
this : 0 ≤ -2 * z.re + 1
⊢ z.re = 1 / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n] = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]

Tactic:
← tsum_G2Term_eq_tsum',

Goal state after:
z : ℍ
⊢ ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n] = ∑' (m : Fin 2 → ℤ), G2Term z m
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F + G) = D F + D G

Tactic:
ext z
  have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
  have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
  simp only [normalizedDerivOfComplex, Pi.add_apply]
  rw [show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,
    deriv_add hFz hGz, mul_add]

Goal state after: