awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⟨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, ⋯⟩) :
      ℝ)
⊢ 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) ⟨1, 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) ⟨1, sorry⟩) :
    ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
⊢ strictWidthInfty (map (mapGL ℝ) Γ) = 1
have hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
Tactic: have hsp := strictPeriods_eq_zmultiples_one_of_T_mem hΓ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))
have rw : DiscreteTopology ↥(AddSubgroup.zmultiples 1)
Tactic: rw [hsp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
⊢ strictWidthInfty (map (mapGL ℝ) Γ) = 1
have this : DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))
Tactic: have : DiscreteTopology (Γ : Subgroup (GL (Fin 2) ℝ)).strictPeriods := by
    -- In fact the image of `Γ` in `GL (Fin 2) ℝ` is itself discrete, but this is quicker:
    rw [hsp]
    infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
this : DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))
⊢ strictWidthInfty (map (mapGL ℝ) Γ) = 1
have hsp₁ : 1 = strictWidthInfty (map (mapGL ℝ) Γ) ∨ -1 = strictWidthInfty (map (mapGL ℝ) Γ)
Tactic: rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff (not_isOfFinAddOrder_of_isAddTorsionFree one_ne_zero)]
    at hsp
Cleared hypotheses: hsp, this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
have pos : ∀ (h : DiscreteTopology ↥𝒢.strictPeriods), 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
Tactic: by_cases h : DiscreteTopology 𝒢.strictPeriods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
pos : ∀ (h : DiscreteTopology ↥𝒢.strictPeriods), 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
have neg : ∀ (h : ¬DiscreteTopology ↥𝒢.strictPeriods), 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
Tactic: by_cases h : DiscreteTopology 𝒢.strictPeriods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
have this : 𝒢.widthInfty ∈ 𝒢.periods
Tactic: have := 𝒢.widthInfty_mem_periods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
this : 𝒢.widthInfty ∈ 𝒢.periods
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
have this₁ : Membership.mem (α := GL (Fin 2) ℝ) 𝒢.adjoinNegOne ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)
Tactic: simp only [Subgroup.periods, mem_strictPeriods_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
this :
  Membership.mem (α := GL (Fin 2) ℝ) 𝒢.adjoinNegOne
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
have inl : ∀ (h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)),
  2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
Tactic: rcases this with (h | h)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
this :
  Membership.mem (α := GL (Fin 2) ℝ) 𝒢.adjoinNegOne
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)
inl :
  ∀ (h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)),
    2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
have inr : ∀ (h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)),
  2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
Tactic: rcases this with (h | h)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.strictWidthInfty ↔ IsCusp ∞ 𝒢
have mp : 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
mp : 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢
⊢ 0 < 𝒢.strictWidthInfty ↔ IsCusp ∞ 𝒢
have mpr : IsCusp ∞ 𝒢 → 0 < 𝒢.strictWidthInfty
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢
have mp : ∀ (h : 0 < 𝒢.strictWidthInfty),
  GeneralLinearGroup.IsParabolic (R := ℝ)
    ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
      ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty))
Tactic: refine fun h ↦ ⟨_, mem_strictPeriods_iff.mpr 𝒢.strictWidthInfty_mem_strictPeriods, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
mp :
  ∀ (h : 0 < 𝒢.strictWidthInfty),
    GeneralLinearGroup.IsParabolic (R := ℝ)
      ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
        ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty))
⊢ 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢
have mp₁ : ∀ (h : 0 < 𝒢.strictWidthInfty),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
          ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty) :
        GL (Fin 2) ℝ)
      ∞ =
    ∞
Tactic: refine fun h ↦ ⟨_, mem_strictPeriods_iff.mpr 𝒢.strictWidthInfty_mem_strictPeriods, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ GeneralLinearGroup.IsParabolic (R := ℝ)
    ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
      ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty))
have mp : Eq (α := ℝ)
    ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
            ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
        Matrix (Fin 2) (Fin 2) ℝ)
      0 0)
    ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
            ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
        Matrix (Fin 2) (Fin 2) ℝ)
      1 1) ∧
  Ne (α := ℝ)
    ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
            ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
        Matrix (Fin 2) (Fin 2) ℝ)
      0 1)
    0
Tactic: rw [GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
⊢ 0 < 𝒢.strictWidthInfty
have mpr : 𝒢.strictWidthInfty ≠ 0
Tactic: apply 𝒢.strictWidthInfty_nonneg.lt_of_ne'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
⊢ 𝒢.strictWidthInfty ≠ 0
have mpr : Ne (α := AddSubgroup ℝ) (AddSubgroup.zmultiples 𝒢.strictWidthInfty) ⊥
Tactic: rw [← AddSubgroup.zmultiples_ne_bot]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
⊢ Ne (α := AddSubgroup ℝ) (AddSubgroup.zmultiples 𝒢.strictWidthInfty) ⊥
have mpr : ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
Tactic: simp only [AddSubgroup.ne_bot_iff_exists_ne_zero, Subtype.exists, Ne, AddSubgroup.mk_eq_zero,
      exists_prop, and_comm, ← strictPeriods_eq_zmultiples_strictWidthInfty, mem_strictPeriods_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
have hgi₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
Tactic: rw [smul_infty_eq_self_iff] at hgi
Cleared hypotheses: hgi
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
have hgp₁ : (∃ (x : ℝ), x ≠ 0 ∧ g = (upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) ∨
  ∃ (x : ℝ), x ≠ 0 ∧ g = -(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x
Tactic: rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp
Cleared hypotheses: hgp, hgi
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp :
  (∃ (x : ℝ), x ≠ 0 ∧ g = (upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) ∨
    ∃ (x : ℝ), x ≠ 0 ∧ g = -(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x
hgi : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
have mpr : ∀ (x : ℝ) (hx : x ≠ 0)
  (hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
  (hgi : Eq (α := ℝ) ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0),
  ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
Tactic: rcases hgp with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩
Cleared hypotheses: g, hgg, hgp, hgi
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp :
  (∃ (x : ℝ), x ≠ 0 ∧ g = (upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) ∨
    ∃ (x : ℝ), x ≠ 0 ∧ g = -(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x
hgi : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
mpr :
  ∀ (x : ℝ) (hx : x ≠ 0)
    (hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
    (hgi : Eq (α := ℝ) ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0),
    ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
have mpr₁ : ∀ (x : ℝ) (hx : x ≠ 0)
  (hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
  (hgi : Eq (α := ℝ) ((↑(-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0),
  ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
Tactic: rcases hgp with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩
Cleared hypotheses: g, hgg, hgp, hgi
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
⊢ 0 < 𝒢.strictWidthInfty
have rw : IsCusp ∞ 𝒢
Tactic: rw [strictWidthInfty_pos_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
⊢ IsCusp ∞ 𝒢
have refine : GeneralLinearGroup.IsParabolic (R := ℝ) ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)
Tactic: refine ⟨upperRightHom h, 𝒢.mem_strictPeriods_iff.mp h𝒢, ?_, smul_infty_eq_self_iff.mpr rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
inst_1 : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢
have this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
Tactic: have : DiscreteTopology 𝒢.adjoinNegOne.strictPeriods := ‹_›
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
inst_1 : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢
have rw : 0 < 𝒢.adjoinNegOne.strictWidthInfty ↔ IsCusp ∞ 𝒢
Tactic: rw [widthInfty, strictWidthInfty_pos_iff, (commensurable_adjoinNegOne_self 𝒢).isCusp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
inst_1 : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
rw : 0 < 𝒢.adjoinNegOne.strictWidthInfty ↔ IsCusp ∞ 𝒢
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢
have rw₁ : IsCusp ∞ 𝒢.adjoinNegOne ↔ IsCusp ∞ 𝒢
Tactic: rw [widthInfty, strictWidthInfty_pos_iff, (commensurable_adjoinNegOne_self 𝒢).isCusp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
inst_1 : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
rw : 0 < 𝒢.adjoinNegOne.strictWidthInfty ↔ IsCusp ∞ 𝒢
rw₁ : IsCusp ∞ 𝒢.adjoinNegOne ↔ IsCusp ∞ 𝒢
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢
have rw₂ : IsCusp ∞ 𝒢 ↔ IsCusp ∞ 𝒢
Tactic: rw [widthInfty, strictWidthInfty_pos_iff, (commensurable_adjoinNegOne_self 𝒢).isCusp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
⊢ 𝒢.IsRegularAtInfty ↔ 𝒢.widthInfty ∈ 𝒢.strictPeriods
have refine : ∀ (h : 𝒢.widthInfty ∈ 𝒢.strictPeriods), 𝒢.IsRegularAtInfty
Tactic: refine ⟨fun h ↦ h ▸ widthInfty_mem_periods 𝒢, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.IsRegularAtInfty
have apply : 𝒢.periods ≤ 𝒢.strictPeriods
Tactic: apply 𝒢.strictPeriods_le_periods.antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.periods ≤ 𝒢.strictPeriods
have rwa : AddSubgroup.zmultiples 𝒢.widthInfty ≤ 𝒢.strictPeriods
Tactic: rwa [periods_eq_zmultiples_widthInfty, AddSubgroup.zmultiples_le]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
⊢ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) = AddSubgroup.zmultiples (↑N : ℝ)
have h : ∀ (x : ℝ),
  x ∈ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (↑N : ℝ)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
N : ℕ
x : ℝ
⊢ x ∈ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (↑N : ℝ)) x
have this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
Tactic: have : AddSubgroup.zmultiples ↑N = .map (Int.castAddHom ℝ) (.zmultiples N) := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
⊢ x ∈ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (↑N : ℝ)) x
have h : (∃ (x_1 : SL(2, ℤ)),
    (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
      Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
        ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) ↔
  x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
Tactic: simp only [this, mem_strictPeriods_iff, Subgroup.mem_map, Gamma_mem]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
⊢ (∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) ↔
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
have h : (∃ (x_1 : SL(2, ℤ)),
    (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
      Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
        ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) →
  x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
h :
  (∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) →
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
⊢ (∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) ↔
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
have h₁ : x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ)) →
  ∃ (x_1 : SL(2, ℤ)),
    (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
      Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
        ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
g : SL(2, ℤ)
hx :
  Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hg : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
have h : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
Tactic: rw [show x = g 0 1 by simpa using congr_arg (· 0 1) hx.symm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
g : SL(2, ℤ)
hx :
  Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hg : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
⊢ (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
have h : Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑N : ℤ)) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
Tactic: apply AddSubgroup.mem_map_of_mem