awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
neg :
  ∀ (u : R) (hu_mem : u ∈ 𝒢.periods) (hu_notMem : u ∉ 𝒢.strictPeriods),
    𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
obtain ⟨u, hu_mem, hu_notMem⟩ := (SetLike.lt_iff_le_and_exists.mp h).2

Premises used: SetLike.lt_iff_le_and_exists, And.right, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
neg :
  𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
rw [AddSubgroup.relIndex_eq_two_iff_exists_notMem_and]

Premises used: AddSubgroup.relIndex_eq_two_iff_exists_notMem_and
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods

Tactic:
.inr ⟨u, hu_mem, hu_notMem, fun b hb ↦ ?_⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
neg : ∀ (b : R) (hb : b ∈ 𝒢.periods), b + u ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods

Tactic:
refine .inr ⟨u, hu_mem, hu_notMem, fun b hb ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
b : R
hb : b ∈ 𝒢.periods
neg :
  ∀
    (hu_mem :
      Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∨
        Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R))
    (hu_notMem : ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∉ 𝒢)
    (hb :
      Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R) ∨
        Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)),
    HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
          ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
        𝒢 ∨
      Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
⊢ b + u ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods

Tactic:
simp only [Subgroup.periods, mem_strictPeriods_iff, mem_adjoinNegOne_iff,
      AddChar.map_add_eq_mul] at hu_mem hu_notMem hb ⊢

Premises used: Subgroup.mem_adjoinNegOne_iff, AddChar.map_add_eq_mul, Subgroup.mem_strictPeriods_iff, Subgroup.periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem :
  Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R)
hu_notMem : ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∉ 𝒢
hb :
  Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R) ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
neg :
  ∀ (h : Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)),
    HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
          ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
        𝒢 ∨
      Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
neg₁ :
  ∀ (h : Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)),
    HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
          ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
        𝒢 ∨
      Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
⊢ HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
        ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
      𝒢 ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)

Tactic:
rcases hb with h | h
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h_1 : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem :
  Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R)
hu_notMem : ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∉ 𝒢
h : Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
⊢ HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
        ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
      𝒢 ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)

Tactic:
Or.inr h

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h_1 : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem :
  Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R)
hu_notMem : ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∉ 𝒢
h : Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
⊢ HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
        ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
      𝒢 ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)

Tactic:
exact Or.inr h

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h_1 : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem :
  Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R)
hu_notMem : ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∉ 𝒢
h : Membership.mem (α := GL (Fin 2) R) 𝒢 (-(upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
⊢ HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R) ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)
        ((upperRightHom : (a : R) → GL (Fin 2) R) u : GL (Fin 2) R) ∈
      𝒢 ∨
    Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) b : GL (Fin 2) R)

Tactic:
simpa only [neg_mul_neg] using Or.inl (mul_mem h <| hu_mem.resolve_left hu_notMem)

Premises used: Or.resolve_left, neg_mul_neg, Or.inl, MulMemClass.mul_mem
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
left : 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
right : 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0
⊢ 𝒢.strictPeriods.Commensurable 𝒢.periods

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
left : ∀ (h : 𝒢.strictPeriods.relIndex 𝒢.periods = 1), 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
left₁ : ∀ (h : 𝒢.strictPeriods.relIndex 𝒢.periods = 2), 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

Tactic:
rcases 𝒢.relIndex_strictPeriods with h | h

Premises used: Subgroup.relIndex_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods.relIndex 𝒢.periods = 1
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods.relIndex 𝒢.periods = 2
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0

Tactic:
simp [AddSubgroup.relIndex_eq_one.mpr 𝒢.strictPeriods_le_periods]

Premises used: Iff.mpr, AddSubgroup.relIndex_eq_one, Subgroup.strictPeriods_le_periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h𝒢 : -1 ∈ 𝒢
⊢ 𝒢.strictPeriods = 𝒢.periods

Tactic:
simp [Subgroup.periods, adjoinNegOne_eq_self_iff.mpr h𝒢]

Premises used: Iff.mpr, Subgroup.adjoinNegOne_eq_self_iff, Subgroup.periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h𝒢 : -1 ∈ 𝒢
⊢ 𝒢.IsRegularAtInfty

Tactic:
𝒢.strictPeriods_eq_periods_of_neg_one_mem h𝒢

Premises used: Subgroup.IsRegularAtInfty, Subgroup.strictPeriods_eq_periods_of_neg_one_mem
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
hG : DiscreteTopology.{u_1} ↥𝒢
H : Set (GL (Fin 2) R) := (↑𝒢 : Set (GL (Fin 2) R)) ∩ Set.range (ι := R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)
⊢ DiscreteTopology.{u_1} (↑H : Type u_1)

Tactic:
have hH : DiscreteTopology H := hG.of_subset Set.inter_subset_left
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
hG : DiscreteTopology.{u_1} ↥𝒢
H : Set (GL (Fin 2) R) := (↑𝒢 : Set (GL (Fin 2) R)) ∩ Set.range (ι := R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)
hH : DiscreteTopology.{u_1} (↑H : Type u_1)
x : R
hx : x ∈ (↑𝒢.strictPeriods : Set R)
⊢ Membership.mem (α := GL (Fin 2) R) H ((upperRightHom : (a : R) → GL (Fin 2) R) x : GL (Fin 2) R)

Tactic:
grind [SetLike.mem_coe, Subgroup.mem_strictPeriods_iff]

Premises used: SetLike.mem_coe, Subgroup.mem_strictPeriods_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
hG : DiscreteTopology.{u_1} ↥𝒢
H : Set (GL (Fin 2) R) := (↑𝒢 : Set (GL (Fin 2) R)) ∩ Set.range (ι := R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)
hH : DiscreteTopology.{u_1} (↑H : Type u_1)
⊢ Set.MapsTo (⇑upperRightHom : (a : R) → GL (Fin 2) R) (↑𝒢.strictPeriods : Set R) H

Tactic:
have : Set.MapsTo upperRightHom 𝒢.strictPeriods H := fun x hx ↦ by
    grind [SetLike.mem_coe, Subgroup.mem_strictPeriods_iff]
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
hG : DiscreteTopology.{u_1} ↥𝒢
H : Set (GL (Fin 2) R) := (↑𝒢 : Set (GL (Fin 2) R)) ∩ Set.range (ι := R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)
hH : DiscreteTopology.{u_1} (↑H : Type u_1)
this : Set.MapsTo (⇑upperRightHom : (a : R) → GL (Fin 2) R) (↑𝒢.strictPeriods : Set R) H
⊢ DiscreteTopology.{u_1} ↥𝒢.strictPeriods

Tactic:
.of_continuous_injective (continuous_upperRightHom.restrict this)
    (this.restrict_inj.mpr injective_upperRightHom.injOn)

Premises used: Iff.mpr, Function.Injective.injOn, Continuous.restrict, DiscreteTopology.of_continuous_injective, Matrix.GeneralLinearGroup.continuous_upperRightHom, Matrix.GeneralLinearGroup.injective_upperRightHom, Set.MapsTo.restrict_inj
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
hG : DiscreteTopology.{u_1} ↥𝒢
H : Set (GL (Fin 2) R) := (↑𝒢 : Set (GL (Fin 2) R)) ∩ Set.range (ι := R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)
hH : DiscreteTopology.{u_1} (↑H : Type u_1)
this : Set.MapsTo (⇑upperRightHom : (a : R) → GL (Fin 2) R) (↑𝒢.strictPeriods : Set R) H
⊢ DiscreteTopology.{u_1} ↥𝒢.strictPeriods

Tactic:
exact .of_continuous_injective (continuous_upperRightHom.restrict this)
    (this.restrict_inj.mpr injective_upperRightHom.injOn)
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : T2Space R
hG : DiscreteTopology.{u_1} ↥𝒢
⊢ DiscreteTopology.{u_1} ↥𝒢.periods

Tactic:
inferInstanceAs (DiscreteTopology 𝒢.adjoinNegOne.strictPeriods)

Premises used: _private.0.Subgroup.instDiscreteTopPeriods._proof_1
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
h : ∀ (x : ℝ), x ∈ strictPeriods (map (mapGL ℝ) Γ) ↔ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x
⊢ strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
h :
  (∃ x_1 ∈ Γ,
      Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
        ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
            (↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x
⊢ x ∈ strictPeriods (map (mapGL ℝ) Γ) ↔ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x

Tactic:
simp only [mem_strictPeriods_iff, Subgroup.mem_map, Units.ext_iff, mapGL_coe_matrix,
    map_apply_coe]

Premises used: Units.ext_iff, Matrix.SpecialLinearGroup.map_apply_coe, Subgroup.mem_strictPeriods_iff, Subgroup.mem_map, Matrix.SpecialLinearGroup.mapGL_coe_matrix
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
h :
  ∃ x_1 ∈ Γ,
    Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
      ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) :
        Matrix (Fin 2) (Fin 2) ℝ)
      ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)
g : SL(2, ℤ)
left : g ∈ Γ
hg :
  Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑g : Matrix (Fin 2) (Fin 2) ℤ) :
      Matrix (Fin 2) (Fin 2) ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)
⊢ (fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) = x

Tactic:
simpa using congr_fun₂ hg 0 1

Premises used: congr_fun₂, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
h :
  Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x →
    ∃ x_1 ∈ Γ,
      Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
        ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
            (↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)
⊢ (∃ x_1 ∈ Γ,
      Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
        ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
            (↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x

Tactic:
refine ⟨fun ⟨g, _, hg⟩ ↦ ⟨g 0 1, by simpa using congr_fun₂ hg 0 1⟩, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ ∃ x ∈ Γ,
    Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
      ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑x : Matrix (Fin 2) (Fin 2) ℤ) :
        Matrix (Fin 2) (Fin 2) ℝ)
      ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ) :
        Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
⟨ModularGroup.T ^ m, zpow_mem hΓ m, ?_⟩

Premises used: zpow_mem, ModularGroup.T, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
h :
  Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) :
      Matrix (Fin 2) (Fin 2) ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
        Matrix (Fin 2) (Fin 2) ℝ) :
      Matrix (Fin 2) (Fin 2) ℝ)
⊢ ∃ x ∈ Γ,
    Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
      ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑x : Matrix (Fin 2) (Fin 2) ℤ) :
        Matrix (Fin 2) (Fin 2) ℝ)
      ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ) :
        Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
refine ⟨ModularGroup.T ^ m, zpow_mem hΓ m, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
h :
  ∀ (i j : Fin 2),
    Eq (α := ℝ)
      ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) i j :
        ℝ)
      ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
            Matrix (Fin 2) (Fin 2) ℝ)
          i j :
        ℝ)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) :
      Matrix (Fin 2) (Fin 2) ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
        Matrix (Fin 2) (Fin 2) ℝ) :
      Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
i j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
h₁ :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) i j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        i j :
      ℝ)

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
h₁ :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
h₁ :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow]

Premises used: ModularGroup.coe_T_zpow