awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
H : Summable (G2Term z)
⊢ ∀ (c : ℤ), Summable (α := ℂ) fun (b : ℤ) ↦ G2Term z ![b, c]
have H₁ : Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
Tactic: rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ G2 z = (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ)
have rw : G2 z = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
Tactic: rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
rw : G2 z = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
⊢ G2 z = (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ)
have rw₁ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])
Tactic: rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
rw : G2 z = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
rw₁ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])
⊢ G2 z = (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ)
have rw₂ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (m : Fin 2 → ℤ), G2Term z m)
Tactic: rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
rw : G2 z = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
rw₁ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])
rw₂ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (m : Fin 2 → ℤ), G2Term z m)
⊢ G2 z = (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ)
have rw₃ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])
Tactic: rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 T G2 = G2
have h : ∀ (z : ℍ),
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 T G2 z = G2 z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 T G2 z = G2 z
have h : G2 (HVAdd.hVAdd (α := ℝ) 1 z) *
    HPow.hPow (β := ℤ)
      (denom
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T))
        (↑z : ℂ))
      (-2) =
  G2 z
Tactic: simp_rw [SL_slash_def, modular_T_smul z]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ G2 (HVAdd.hVAdd (α := ℝ) 1 z) *
      HPow.hPow (β := ℤ)
        (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T))
          (↑z : ℂ))
        (-2) =
    G2 z
have h : Eq (α := ℂ)
  (∑' (n : ℕ+),
    (↑((ArithmeticFunction.sigma 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (1 + (↑z : ℂ))) ^ (↑n : ℕ))
  (∑' (n : ℕ+),
    (↑((ArithmeticFunction.sigma 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑z : ℂ) + 2 * (↑π : ℂ) * I) ^ (↑n : ℕ))
Tactic: simp [G2_eq_tsum_cexp, T, denom_apply, ← exp_periodic.nat_mul 1 (2 * π * I * z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
γ : SL(2, ℤ)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ G2 = G2 - D2 γ
have this : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ
Tactic: have : γ ∈ Subgroup.closure {S, T} := by simp [SpecialLinearGroup.SL2Z_generators]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
γ g : SL(2, ℤ)
hg : Membership.mem (γ := Set SL(2, ℤ)) {S, T} g
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
have hg₁ : g = S ∨ g = T
Tactic: simp only [mem_insert_iff, mem_singleton_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
hg : g = S ∨ g = T
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
have mem : ∀ (h1 : g = S),
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
Tactic: rcases hg with (h1 | h2)
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
hg : g = S ∨ g = T
mem :
  ∀ (h1 : g = S),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
have mem₁ : ∀ (h2 : g = T),
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
Tactic: rcases hg with (h1 | h2)
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
h1 : g = S
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
have mem : ∀ (z : ℍ),
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 z =
    (G2 - D2 g) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 z =
    (G2 - D2 g) z
have mem : HPow.hPow (β := ℤ) (↑z : ℂ) (-2) * G2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ } =
  (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ } -
      I * ((↑π : ℂ) * -2) / (↑z : ℂ) -
    I * ((↑π : ℂ) * 2) / (↑z : ℂ)
Tactic: simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
⊢ HPow.hPow (β := ℤ) (↑z : ℂ) (-2) * G2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } =
    (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } -
        I * ((↑π : ℂ) * -2) / (↑z : ℂ) -
      I * ((↑π : ℂ) * 2) / (↑z : ℂ)
have mem : HPow.hPow (β := ℤ) (↑z : ℂ) (-2) * G2 { coe := -(↑z : ℂ)⁻¹, coe_im_pos := sorry : ℍ } =
  HPow.hPow (β := ℕ) (↑z : ℂ)⁻¹ 2 * G2 { coe := -(↑z : ℂ)⁻¹, coe_im_pos := sorry : ℍ }
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g h : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
hy : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) h
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
ih : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 h G2 = G2 - D2 h
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 (g * h) G2 =
    G2 - D2 (g * h)
have mul : G2 - D2 h +
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 h (-D2 g) =
  G2 -
    (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 h (D2 g) + D2 h)
Tactic: rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2) =
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ (G2 - D2 g)
have rw : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ (G2 - D2 g) =
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ (G2 - D2 g)
Tactic: rw [ig]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
γ g : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 = G2 - D2 g⁻¹
have H1 : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹
    (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2) =
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ (G2 - D2 g)
Tactic: have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
γ g : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
H1 :
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2) =
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ (G2 - D2 g)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 = G2 - D2 g⁻¹
have H1₁ : G2 =
  @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
        GL (Fin 2) ℝ)
      G2 +
    -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        SubNegMonoid.toAddMonoid _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        (D2 g)
Tactic: simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
H1 :
  G2 =
    @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        G2 +
      -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
          SubNegMonoid.toAddMonoid _ 2
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)
          (D2 g)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 = G2 - D2 g⁻¹
have inv : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 =
  @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        G2 +
      -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
          SubNegMonoid.toAddMonoid _ 2
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)
          (D2 g) -
    D2 g⁻¹
Tactic: nth_rw 2 [H1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
γ g : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
H1 :
  G2 =
    @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        G2 +
      -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
          SubNegMonoid.toAddMonoid _ 2
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)
          (D2 g)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 =
    @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
          (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)
          G2 +
        -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
            SubNegMonoid.toAddMonoid _ 2
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
              GL (Fin 2) ℝ)
            (D2 g) -
      D2 g⁻¹
have this : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ (D2 g) = -D2 g⁻¹
Tactic: have := D2_inv g
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ g : SL(2, ℤ)
hx : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g
ig : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
H1 :
  G2 =
    @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        G2 +
      -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
          SubNegMonoid.toAddMonoid _ 2
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)
          (D2 g)
this :
  @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
        GL (Fin 2) ℝ)
      (D2 g) =
    -D2 g⁻¹
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 =
    @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
          (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)
          G2 +
        -@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
            SubNegMonoid.toAddMonoid _ 2
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
              GL (Fin 2) ℝ)
            (D2 g) -
      D2 g⁻¹
have inv : @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 =
  @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        G2 -
      @SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        SubNegMonoid.toAddMonoid _ 2
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        (D2 g) -
    D2 g⁻¹
Tactic: rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ : SL(2, ℤ)
this : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ G2 = G2 - D2 γ
have one : @SlashAction.map ℤ SL(2, ℤ) _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 1 G2 =
  G2 - D2 1
Tactic: induction this using Subgroup.closure_induction with
  | one => simp only [SlashAction.slash_one, D2_one, sub_zero]
  | mem g hg =>
      simp only [mem_insert_iff, mem_singleton_iff] at hg
      rcases hg with (h1 | h2)
      · ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop
      · simpa only [h2, D2_T, sub_zero] using G2_T_transform
  | mul g h _ _ ig ih =>
      rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
      grind [SlashAction.neg_slash, SL_slash]
  | inv g _ ig =>
      have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ : SL(2, ℤ)
this : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ
one :
  @SlashAction.map ℤ SL(2, ℤ) _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 1 G2 =
    G2 - D2 1
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ G2 = G2 - D2 γ
have mem : ∀ (g : SL(2, ℤ)) (hg : Membership.mem (γ := Set SL(2, ℤ)) {S, T} g),
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
Tactic: induction this using Subgroup.closure_induction with
  | one => simp only [SlashAction.slash_one, D2_one, sub_zero]
  | mem g hg =>
      simp only [mem_insert_iff, mem_singleton_iff] at hg
      rcases hg with (h1 | h2)
      · ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop
      · simpa only [h2, D2_T, sub_zero] using G2_T_transform
  | mul g h _ _ ig ih =>
      rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
      grind [SlashAction.neg_slash, SL_slash]
  | inv g _ ig =>
      have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]
Cleared hypotheses: this