awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)
have rw : Eq (α := ℂ)
  (deriv
    (fun (x : ℂ) ↦
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) x 2 / τ) * jacobiTheta₂ (x / τ) (-1 / τ))
    z)
  (deriv
    (fun (z : ℂ) ↦
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
    z)
Tactic: rw [funext (jacobiTheta₂_functional_equation · τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z =
    1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
have simp_rw : deriv
    (fun (z : ℂ) ↦
      1 / (-I * τ) ^ (1 / 2) * (cexp (-(↑π : ℂ) * (I * HPow.hPow (β := ℕ) z 2) / τ) * jacobiTheta₂ (z / τ) (-1 / τ)))
    z =
  1 / (-I * τ) ^ (1 / 2) *
    deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * (I * HPow.hPow (β := ℕ) z 2) / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
Tactic: simp_rw [mul_assoc, deriv_const_mul_field]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z)
have rw : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z
Tactic: rw [deriv_fun_mul _ hj.differentiableAt]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have rw : 1 / (-I * τ) ^ (1 / 2) *
    (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
      cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) =
  1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
    (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
Tactic: rw [hj.deriv]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹)) z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))
have rw : (cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * (-(↑π : ℂ) * I * ((↑2 : ℂ) * z ^ HSub.hSub (α := ℕ) 2 1) * τ⁻¹) *
        jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
      cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
    (1 / (-I * τ) ^ (1 / 2)) =
  1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * τ⁻¹ *
    (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))
Tactic: rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have _ : Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
  (deriv
    (fun (z : ℂ) ↦
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
    z)
Tactic: calc
  _ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
  _ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    rw [funext (jacobiTheta₂_functional_equation · τ)]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    simp_rw [mul_assoc, deriv_const_mul_field]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        (deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ)
         + cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) := by
    rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
  _ = _ := by
    rw [hj.deriv]
    simp only [div_eq_mul_inv _ τ]
    rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
    ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
_ :
  Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have _₁ : deriv
    (fun (z : ℂ) ↦
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
    z =
  1 / (-I * τ) ^ (1 / 2) *
    deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
Tactic: calc
  _ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
  _ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    rw [funext (jacobiTheta₂_functional_equation · τ)]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    simp_rw [mul_assoc, deriv_const_mul_field]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        (deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ)
         + cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) := by
    rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
  _ = _ := by
    rw [hj.deriv]
    simp only [div_eq_mul_inv _ τ]
    rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
    ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
_ :
  Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)
_₁ :
  deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z =
    1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have _₂ : 1 / (-I * τ) ^ (1 / 2) *
    deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
  1 / (-I * τ) ^ (1 / 2) *
    (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
      cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z)
Tactic: calc
  _ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
  _ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    rw [funext (jacobiTheta₂_functional_equation · τ)]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    simp_rw [mul_assoc, deriv_const_mul_field]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        (deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ)
         + cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) := by
    rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
  _ = _ := by
    rw [hj.deriv]
    simp only [div_eq_mul_inv _ τ]
    rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
    ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
_ :
  Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)
_₁ :
  deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z =
    1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
_₂ :
  1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z)
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have _₃ : 1 / (-I * τ) ^ (1 / 2) *
    (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
      cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) =
  1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
    (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
Tactic: calc
  _ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
  _ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    rw [funext (jacobiTheta₂_functional_equation · τ)]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    simp_rw [mul_assoc, deriv_const_mul_field]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        (deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ)
         + cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) := by
    rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
  _ = _ := by
    rw [hj.deriv]
    simp only [div_eq_mul_inv _ τ]
    rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
    ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom :
  ‖denom
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑τ : ℂ)‖ ≤
    1
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) (γ • τ) : ℂ)
have this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
Tactic: have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
⊢ k = 0 ∨ c = 0
have this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
Tactic: have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
⊢ k = 0 ∨ c = 0
have hI : (f : (a : ℍ) → ℂ) (S • UpperHalfPlane.I) =
  HMul.hMul (β := ℂ)
    (denom
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
        (↑UpperHalfPlane.I : ℂ) ^
      k)
    ((f : (a : ℍ) → ℂ) UpperHalfPlane.I : ℂ)
Tactic: have hI := slash_action_eqn_SL'' f (mem_Gamma_one S) I
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  (f : (a : ℍ) → ℂ) (S • UpperHalfPlane.I) =
    HMul.hMul (β := ℂ)
      (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
          (↑UpperHalfPlane.I : ℂ) ^
        k)
      ((f : (a : ℍ) → ℂ) UpperHalfPlane.I : ℂ)
⊢ k = 0 ∨ c = 0
have h2I2 : (f : (a : ℍ) → ℂ)
    (S • HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 sorry) UpperHalfPlane.I) =
  HMul.hMul (β := ℂ)
    (denom
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
        (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 sorry) UpperHalfPlane.I) : ℂ) ^
      k)
    ((f : (a : ℍ) → ℂ)
        (HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 sorry) UpperHalfPlane.I) :
      ℂ)
Tactic: have h2I2 := slash_action_eqn_SL'' f (mem_Gamma_one S) ((⟨2, two_pos⟩ : {x : ℝ // 0 < x}) • .I)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = (↑UpperHalfPlane.I : ℂ) ^ k * c
h2I2 :
  c =
    (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) : ℂ) ^ k * c
⊢ k = 0 ∨ c = 0
have suffices : HPow.hPow (α := ℂ) 2 k = 1 ↔ k = 0
Tactic: suffices (2 : ℂ) ^ k = 1 ↔ k = 0 by
    simpa [mul_zpow, zpow_ne_zero, this] using h2I2.symm.trans hI
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
⊢ Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
have rw : Eq (α := Subgroup (GL (Fin 2) ℝ))
  (Subgroup.closure
    (insert (α := GL (Fin 2) ℝ) ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) S : GL (Fin 2) ℝ)
      (singleton (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) T : GL (Fin 2) ℝ))))
  (Subgroup.closure
    (insert (α := GL (Fin 2) ℝ)
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
        GL (Fin 2) ℝ)
      (singleton (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
          GL (Fin 2) ℝ))))
Tactic: rw [MonoidHom.range_eq_map, ← SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure,
      Set.image_pair]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
have h𝒮ℒ : Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
  (Subgroup.closure
    (insert (α := GL (Fin 2) ℝ)
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
        GL (Fin 2) ℝ)
      (singleton (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
          GL (Fin 2) ℝ))))
Tactic: have h𝒮ℒ : 𝒮ℒ = Subgroup.closure ({↑S, ↑T} : Set (GL (Fin 2) ℝ)) := by
    change (Matrix.SpecialLinearGroup.mapGL ℝ).range = _
    rw [MonoidHom.range_eq_map, ← SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure,
      Set.image_pair]
    rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
h𝒮ℒ :
  Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
g : GL (Fin 2) ℝ
hg :
  Membership.mem (γ := Set (GL (Fin 2) ℝ))
    (insert (α := GL (Fin 2) ℝ)
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
        GL (Fin 2) ℝ)
      (singleton (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
          GL (Fin 2) ℝ)))
    g
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f = f
have inl : @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
    (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
    ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
      GL (Fin 2) ℝ)
    f =
  f
Tactic: rcases hg with rfl | rfl
Cleared hypotheses: g, hg