mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : ¬w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : ¬w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case infty
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
⊢ (fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p)
      ((fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯) ∞) =
    ∞

pp: case coe
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
x✝ : K
⊢ (fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p)
      ((fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯) ↑x✝) =
    ↑x✝

Tactic:
<;>

Goal state after:
case infty
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
⊢ (fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p)
      ((fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯) ∞) =
    ∞

case coe
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
x✝ : K
⊢ (fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p)
      ((fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯) ↑x✝) =
    ↑x✝
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
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) (mk K w hw)) =
    mk K w hw

pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) (mk K w hw)) =
    mk K w hw

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) (mk K w hw)) =
    mk K w hw

case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) (mk K w hw)) =
    mk K w hw
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case h.«0»
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) ((fun i ↦ i) ⟨0, ⋯⟩) = ![1, 0] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«1»
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) ((fun i ↦ i) ⟨1, ⋯⟩) = ![1, 0] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case h.«0»
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) ((fun i ↦ i) ⟨0, ⋯⟩) = ![1, 0] ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«1»
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) ((fun i ↦ i) ⟨1, ⋯⟩) = ![1, 0] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

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

Tactic:
by simp [inv_mul_cancel₀ h₀]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ↑g 1 0 = 0
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ¬↑g 1 0 = 0
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ↑g 1 0 = 0
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ¬↑g 1 0 = 0
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
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
h : ↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

pp: case neg
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
h : ¬↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

Tactic:
<;>

Goal state after:
case pos
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
h : ↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

case neg
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
h : ¬↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
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₂
⊢ g * (mapGL ℚ) ⟨y, hy⟩ * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
have hz_det : z.det = 1 := by
    have := congr_arg Matrix.det hz_coe
    simp_rw [Matrix.det_mul, ← Int.cast_det] at this
    rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this

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
⊢ g * (mapGL ℚ) ⟨y, hy⟩ * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
x✝ : ℍ
⊢ (0 ∣[k] A) x✝ = 0 x✝

Tactic:
by simp [privateSlash]

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

Goal state before:
pp: case mpr.refine_1
a : SL(2, ℤ)
⊢ ((mapGL ℝ) (a * ModularGroup.T * a⁻¹)).IsParabolic

Tactic:
suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa

Goal state after:
case mpr.refine_1
a : SL(2, ℤ)
⊢ ((mapGL ℝ) ModularGroup.T).IsParabolic
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 : ℤ
⊢ (∀ γ ∈ Γ, f ∣[k] γ = f) → ∀ γ ∈ s, f ∣[k] γ = f

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

Tactic:
<;>

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

case mpr
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
⊢ (∀ γ ∈ s, f ∣[k] γ = f) → ∀ γ ∈ Γ, f ∣[k] γ = f
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case left.inl
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods.relIndex 𝒢.periods = 1
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

pp: case left.inr
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods.relIndex 𝒢.periods = 2
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

Tactic:
<;>

Goal state after:
case left.inl
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods.relIndex 𝒢.periods = 1
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

case left.inr
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods.relIndex 𝒢.periods = 2
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case «0»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case «0».«0»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom ((fun x ↦ x • 1) m)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

pp: case inr
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : -upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
<;>

Goal state after:
case inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

case inr
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : -upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ 0 < 𝒢.widthInfty

Tactic:
by
  apply strictWidthInfty_pos

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (fun x ↦ f (↑ofComplex x)) {z | 0 < z.im}
this :
  Set.EqOn (fun x ↦ (starRingEnd ℂ) (f (↑ofComplex (-(starRingEnd ℂ) ↑(↑ofComplex x)))))
    (fun x ↦ (starRingEnd ℂ) (f (↑ofComplex (-(starRingEnd ℂ) x)))) {z | 0 < z.im}
z : ℂ
hz : z ∈ {z | 0 < z.im}
⊢ 0 < (-(starRingEnd ℂ) z).im

Tactic:
simpa using! hz

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

Goal state before:
pp: case mpr.«0»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case mpr.«1»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case mpr.«0»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨0, ⋯⟩) j

case mpr.«1»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
j : Fin 2
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr.«0».«0»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case mpr.«0».«1»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case mpr.«1».«0»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case mpr.«1».«1»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case mpr.«0».«0»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case mpr.«0».«1»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case mpr.«1».«0»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case mpr.«1».«1»
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ (algebraMap ℤ ℝ).mapMatrix (↑(ModularGroup.T ^ (a * ↑N))) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(upperRightHom x) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ (⇑(c • f.toSlashInvariantForm) ∣[k] g) =O[atImInfty] 1

Tactic:
FunLike.coe_smul,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ ((c • ⇑f.toSlashInvariantForm) ∣[k] g) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto (⇑(c • f.toSlashInvariantForm) ∣[k] g) atImInfty (𝓝 0)

Tactic:
FunLike.coe_smul,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((c • ⇑f.toSlashInvariantForm) ∣[k] g) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto (⇑(c • f.toSlashInvariantForm) ∣[k] g) atImInfty (𝓝 0)

Tactic:
FunLike.coe_smul,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((c • ⇑f.toSlashInvariantForm) ∣[k] g) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: case inl
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) = f

pp: case inr
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T) = f

Tactic:
<;>

Goal state after:
case inl
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) = f

case inr
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T) = f
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] γ = f

Tactic:
exact (slash_action_generators h𝒮ℒ).mpr (fun g hg ↦ by rcases hg with rfl | rfl <;> assumption)
    _ (MonoidHom.mem_range.mpr ⟨γ, rfl⟩)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
exact normSq_denom_pos g z.im_ne_zero

Goal state after: