awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑N : ℤ)) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
have h : (↑N : ℤ) ∣ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
Tactic: rwa [Int.mem_zmultiples_iff, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
-- 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 ∈ 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) ℝ)
have h : ∀ (x_1 : ℤ) (h : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) x_1 (↑N : ℤ)) = x),
  ∃ (x_2 : SL(2, ℤ)),
    (Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
      Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
        ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
            (↑x_2 : 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: simp only [AddSubgroup.mem_map, AddSubgroup.mem_zmultiples_iff, existsAndEq, true_and,
      Units.ext_iff, mapGL_coe_matrix, map_apply_coe, forall_exists_index]
-- 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 : ℤ) (h : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) x_1 (↑N : ℤ)) = x),
    ∃ (x_2 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
          ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
              (↑x_2 : 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) ℝ)
have h : ∀ (a : ℤ) (ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x),
  Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : 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 a ha ↦ ⟨ModularGroup.T ^ (a * N), by simp [ModularGroup.coe_T_zpow], ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : 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) ℝ)
have h : ∀ (i j : Fin 2),
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) i j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) i j : ℝ)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
i j : Fin 2
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) i j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
i j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) i j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
j : Fin 2
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
j : Fin 2
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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 ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : 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:
N : ℕ
inst : NeZero N
⊢ strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N)) = (↑N : ℝ)
have hsp : strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) = AddSubgroup.zmultiples (↑N : ℝ)
Tactic: have hsp := strictPeriods_Gamma N
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
N : ℕ
inst : NeZero N
hsp : strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) = AddSubgroup.zmultiples (↑N : ℝ)
⊢ strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N)) = (↑N : ℝ)
have hsp₁ : (↑N : ℝ) = strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N)) ∨ -(↑N : ℝ) = strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N))
Tactic: rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff
      (not_isOfFinAddOrder_of_isAddTorsionFree (NeZero.ne _))] at hsp
Cleared hypotheses: hsp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
n : ℕ
z : ℂ
⊢ eta_q n z = cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
have simp : cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (2 * (↑π : ℂ) * I * z)) =
  cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
Tactic: simp [eta_q, Periodic.qParam, ← Complex.exp_nsmul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ 1 - eta_q n z ≠ 0
have rw : 1 ≠ cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
Tactic: rw [eta_q_eq_cexp, sub_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
q : ℂ
hq : ‖q‖ < 1
⊢ Multipliable (α := ℂ) fun (n : ℕ) ↦ 1 - q ^ (n + 1)
have apply : Summable (α := ℝ) fun (i : ℕ) ↦ ‖-q ^ (i + 1)‖
Tactic: apply multipliable_one_add_of_summable (f := fun n ↦ -q ^ (n + 1))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
⊢ MultipliableLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 - q ^ (n + 1)) (Metric.ball 0 1)
have h : HasProdLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 - q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1)))
  (Metric.ball 0 1)
Tactic: use fun q ↦ ∏' n, (1 - q ^ (n + 1))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
⊢ HasProdLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1))
    (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) (Metric.ball 0 1)
have h : ∀ K ⊆ Metric.ball 0 1,
  IsCompact K →
    HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1)))
      K
Tactic: apply hasProdLocallyUniformlyOn_of_forall_compact Metric.isOpen_ball
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
have h : ∀ (hN : K = ∅),
  HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Tactic: rcases K.eq_empty_or_nonempty with hN | hN
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
h :
  ∀ (hN : K = ∅),
    HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1)))
      K
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
have h₁ : ∀ (hN : K.Nonempty),
  HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Tactic: rcases K.eq_empty_or_nonempty with hN | hN
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
have h : ∀ (q₀ : ℂ) (hq₀ : q₀ ∈ K),
  sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖ →
    ∀ (HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖),
      HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1))
        (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Tactic: obtain ⟨q₀, hq₀, _, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN
      (show ContinuousOn (fun q : ℂ ↦ ‖q‖) K by fun_prop)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left : sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
have h : ∀ (n : ℕ) (x : ℂ) (hx : x ∈ K), ‖-x ^ (n + 1)‖ ≤ ‖q₀‖ ^ (n + 1)
Tactic: refine ((summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _)
      (by simpa [Metric.mem_ball, dist_zero_right] using hK hq₀))).hasProdUniformlyOn_nat_one_add
      hcK (.of_forall fun n x hx ↦ ?_) (fun _ ↦ by fun_prop)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Ne (α := ℂ) (∏' (n : ℕ), (1 - eta_q n z)) 0
have refine_1 : ∀ (i : ℕ), HAdd.hAdd (α := ℂ) 1 ((fun (n : ℕ) ↦ -eta_q n z) i) ≠ 0
Tactic: refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℂ
hz : z ∈ ℍₒ
refine_1 : ∀ (i : ℕ), HAdd.hAdd (α := ℂ) 1 ((fun (n : ℕ) ↦ -eta_q n z) i) ≠ 0
⊢ Ne (α := ℂ) (∏' (n : ℕ), (1 - eta_q n z)) 0
have refine_2 : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((fun (n : ℕ) ↦ -eta_q n z) x)
Tactic: refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
r : ℂ
⊢ Eq (α := (x : ℂ) → ℂ) (logDeriv fun (z : ℂ) ↦ 1 - r * cexp z) fun (z : ℂ) ↦ -r * cexp z / (1 - r * cexp z)
have h : ∀ (z : ℂ), logDeriv (fun (z : ℂ) ↦ 1 - r * cexp z) z = -r * cexp z / (1 - r * cexp z)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
⊢ Eq (α := (x : ℂ) → ℂ) (logDeriv ((fun (z : ℂ) ↦ 1 - r * cexp z) ∘ g)) fun (z : ℂ) ↦
    -r * deriv g z * cexp (g z) / (1 - r * cexp (g z))
have h : ∀ (y : ℂ), logDeriv ((fun (z : ℂ) ↦ 1 - r * cexp z) ∘ g) y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))
Tactic: ext y
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
y : ℂ
⊢ logDeriv ((fun (z : ℂ) ↦ 1 - r * cexp z) ∘ g) y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))
have h : (fun (z : ℂ) ↦ -r * cexp z / (1 - r * cexp z)) (g y) * deriv g y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))
Tactic: rw [logDeriv_comp (by fun_prop) (hg y), logDeriv_one_sub_cexp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (hypothesis)
Goal:
z : ℂ
n : ℕ
⊢ logDeriv (fun (x : ℂ) ↦ 1 - eta_q n x) z =
    2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n z / (1 - eta_q n z)
have h2 : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
  ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)
Tactic: have h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (n + 1) * x)) =
      ((fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (n + 1) * x) := by aesop
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℂ
n : ℕ
h2 :
  Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
    ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)
⊢ logDeriv (fun (x : ℂ) ↦ 1 - eta_q n x) z =
    2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n z / (1 - eta_q n z)
have simp_rw : -1 * (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z) /
    (1 - 1 * cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)) =
  2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z) /
    (1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z))
Tactic: simp_rw [eta_q_eq_cexp, h2, logDeriv_one_sub_mul_cexp_comp 1
    (g := fun x ↦ (2 * π * I * (n + 1) * x)) (by fun_prop), deriv_const_mul_id]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℂ
⊢ ∑' (n : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q n x) z =
    2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n z / (1 - eta_q n z)
have rw : Eq (α := ℂ) (∑' (b : ℕ), 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 * -eta_q b z / (1 - eta_q b z))
  (∑' (x : ℕ), 2 * (↑π : ℂ) * I * (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 * -eta_q x z / (1 - eta_q x z)))
Tactic: rw [tsum_congr (one_sub_eta_logDeriv_eq z), ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (hypothesis)
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) z
have hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 z)
Tactic: have hq : 𝕢 1 z ∈ Metric.ball 0 1 := by simpa using norm_qParam_lt_one 1 ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
h : ℝ
z : ℂ
⊢ 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
have h₁ : ∀ (x : ℂ), 𝕢 h x = (cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x) x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (hypothesis)
Goal:
h : ℝ
z : ℂ
⊢ logDeriv (𝕢 h) z = 2 * (↑π : ℂ) * I / (↑h : ℂ)
have this : 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
Tactic: have : 𝕢 h = cexp ∘ ((2 * π * I / h) * ·) := by
    ext
    grind [Periodic.qParam]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
⊢ logDeriv (𝕢 h) z = 2 * (↑π : ℂ) * I / (↑h : ℂ)
have rw : logDeriv cexp (2 * (↑π : ℂ) * I / (↑h : ℂ) * z) * (2 * (↑π : ℂ) * I / (↑h : ℂ)) = 2 * (↑π : ℂ) * I / (↑h : ℂ)
Tactic: rw [this, logDeriv_comp (by fun_prop) (by fun_prop), deriv_const_mul_id]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (hypothesis)
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) z
have this : Summable (α := ℂ) fun (n : ℕ) ↦
  HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n /
    (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n)
Tactic: have := summable_norm_pow_mul_geometric_div_one_sub 1 (norm_qParam_lt_one 1 ⟨z, hz⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℂ
hz : z ∈ ℍₒ
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n /
      (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n)
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) z
have h : Eq (α := ℕ → ℂ) (fun (i : ℕ) ↦ logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) z) fun (i : ℕ) ↦
  -2 * (↑π : ℂ) * I *
    (HPow.hPow (α := ℂ) (β := ℕ) (↑(i + 1) : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1) /
      (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1)))
Tactic: convert! ((summable_nat_add_iff 1).mpr this).mul_left (-2 * π * I) using 1 with n