awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
c : OnePoint ℝ
hc : IsCusp c 𝒢
⊢ ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
    cosetToCuspOrbit 𝒢 a =
      Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
        (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢) c hc)
have hc₁ : ∃ (g : SL(2, ℤ)),
  c = HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
Tactic: rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'] at hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
c : OnePoint ℝ
hc_1 : IsCusp c 𝒢
hc :
  ∃ (g : SL(2, ℤ)),
    c = HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
⊢ ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
    cosetToCuspOrbit 𝒢 a =
      Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
        (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢) c hc_1)
have mk : ∀ (g : SL(2, ℤ))
  (hc :
    IsCusp
      (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)
      𝒢),
  ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
    cosetToCuspOrbit 𝒢 a =
      Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
        (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
          (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)
          hc)
Tactic: obtain ⟨g, rfl⟩ := hc
Cleared hypotheses: c, hc_1, hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
g : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞) 𝒢
⊢ ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
    cosetToCuspOrbit 𝒢 a =
      Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
        (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
          (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)
          hc)
have h : cosetToCuspOrbit 𝒢 ⟦g⁻¹⟧ =
  Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
    (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
      (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)
      hc)
Tactic: use ⟦g⁻¹⟧
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
have pos : ∀ (h : 𝒢.strictPeriods = 𝒢.periods), 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
Tactic: by_cases h : 𝒢.strictPeriods = 𝒢.periods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
pos :
  ∀ (h : 𝒢.strictPeriods = 𝒢.periods), 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
have neg : ∀ (h : ¬𝒢.strictPeriods = 𝒢.periods), 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
Tactic: by_cases h : 𝒢.strictPeriods = 𝒢.periods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : ¬𝒢.strictPeriods = 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
have h₁ : 𝒢.strictPeriods < 𝒢.periods
Tactic: replace h := 𝒢.strictPeriods_le_periods.lt_of_ne h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
have neg : ∀ (u : R) (hu_mem : u ∈ 𝒢.periods) (hu_notMem : u ∉ 𝒢.strictPeriods),
  𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
Tactic: obtain ⟨u, hu_mem, hu_notMem⟩ := (SetLike.lt_iff_le_and_exists.mp h).2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
have neg : 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
  ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
Tactic: rw [AddSubgroup.relIndex_eq_two_iff_exists_notMem_and]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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
have neg : ∀ (b : R) (hb : b ∈ 𝒢.periods), b + u ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
Tactic: refine .inr ⟨u, hu_mem, hu_notMem, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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
⊢ b + u ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
have 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)
Tactic: simp only [Subgroup.periods, mem_strictPeriods_iff, mem_adjoinNegOne_iff,
      AddChar.map_add_eq_mul] at hu_mem hu_notMem hb ⊢
Cleared hypotheses: hu_mem, hu_notMem, hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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)
⊢ 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)
have 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)
Tactic: rcases hb with h | h
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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)
⊢ 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)
have 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)
Tactic: rcases hb with h | h
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.Commensurable 𝒢.periods
have left : 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
left : 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
⊢ 𝒢.strictPeriods.Commensurable 𝒢.periods
have right : 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
have left : ∀ (h : 𝒢.strictPeriods.relIndex 𝒢.periods = 1), 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
Tactic: rcases 𝒢.relIndex_strictPeriods with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
left : ∀ (h : 𝒢.strictPeriods.relIndex 𝒢.periods = 1), 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
have left₁ : ∀ (h : 𝒢.strictPeriods.relIndex 𝒢.periods = 2), 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0
Tactic: rcases 𝒢.relIndex_strictPeriods with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
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} ↥𝒢.strictPeriods
have hH : DiscreteTopology.{u_1} (↑H : Type u_1)
Tactic: have hH : DiscreteTopology H := hG.of_subset Set.inter_subset_left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
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)
⊢ DiscreteTopology.{u_1} ↥𝒢.strictPeriods
have this : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
⊢ strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
have h : ∀ (x : ℝ), x ∈ strictPeriods (map (mapGL ℝ) Γ) ↔ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
⊢ x ∈ strictPeriods (map (mapGL ℝ) Γ) ↔ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x
have 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
Tactic: simp only [mem_strictPeriods_iff, Subgroup.mem_map, Units.ext_iff, mapGL_coe_matrix,
    map_apply_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
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) ℝ)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples 1) x
have 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) ℝ)
Tactic: refine ⟨fun ⟨g, _, hg⟩ ↦ ⟨g 0 1, by simpa using congr_fun₂ hg 0 1⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ)
have 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) ℝ)
Tactic: refine ⟨ModularGroup.T ^ m, zpow_mem hΓ m, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ 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) ℝ)
have 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 :
      ℝ)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
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 :
      ℝ)
have 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, sorry⟩) j :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) : Matrix (Fin 2) (Fin 2) ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j :
    ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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 :
      ℝ)
⊢ 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 :
      ℝ)
have 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, sorry⟩) j :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) : Matrix (Fin 2) (Fin 2) ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j :
    ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
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) ℤ) ((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 :
      ℝ)
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) : Matrix (Fin 2) (Fin 2) ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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, ⋯⟩) :
      ℝ)
⊢ 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 :
      ℝ)
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) : Matrix (Fin 2) (Fin 2) ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
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) ℤ) ((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 :
      ℝ)
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) : Matrix (Fin 2) (Fin 2) ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
Tactic: fin_cases j
Cleared hypotheses: j