awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Summable (G2Term z)

Tactic:
have := G2Term_summable z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
this : Summable (G2Term z)
⊢ Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))

Tactic:
rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at this

Premises used: Equiv.trans, Equiv.prodComm, Equiv.summable_iff, Equiv.symm, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
this :
  Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
this.prod

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Summable.prod, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
this :
  Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
exact this.prod

Premises used: Summable.prod
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
rw :
  Eq (α := ℂ) (∑' (c : ℤ × ℤ), G2Term z (((finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ) c))
    (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])
⊢ Eq (α := ℂ) (∑' (m : Fin 2 → ℤ), G2Term z m) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])

Tactic:
rw [← (finTwoArrowEquiv _).symm.tsum_eq]

Premises used: Equiv.tsum_eq, Equiv.symm, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Eq (α := ℂ) (∑' (c : ℤ × ℤ), G2Term z (((finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ) c))
    (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])

Tactic:
Summable.tsum_prod' (G2Term_prod_summable z) ((G2Term_prod_summable z).prod_factor)

Premises used: Eq.mpr, Summable.tsum_prod', Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, _private.0.EisensteinSeries.G2Term_prod_summable, Summable.prod_factor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Eq (α := ℂ) (∑' (c : ℤ × ℤ), G2Term z (((finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ) c))
    (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])

Tactic:
exact Summable.tsum_prod' (G2Term_prod_summable z) ((G2Term_prod_summable z).prod_factor)

Premises used: Summable.tsum_prod', _private.0.EisensteinSeries.G2Term_prod_summable, Summable.prod_factor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
h : Summable (α := ℂ) (β := ℤ × ℤ) (Function.uncurry fun (m n : ℤ) ↦ G2Term z ![m, n])
h₁ : ∀ (b : ℤ), Summable (α := ℂ) fun (n : ℤ) ↦ G2Term z ![b, n]
h₂ : ∀ (c : ℤ), Summable (α := ℂ) fun (b : ℤ) ↦ G2Term z ![b, c]
⊢ Eq (α := ℂ) (∑' (m : Fin 2 → ℤ), G2Term z m) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])

Tactic:
rw [Summable.tsum_comm', tsum_G2Term_eq_tsum]

Premises used: _private.0.EisensteinSeries.tsum_G2Term_eq_tsum, Summable.tsum_comm'
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Summable (α := ℂ) (β := ℤ × ℤ) (Function.uncurry fun (m n : ℤ) ↦ G2Term z ![m, n])

Tactic:
G2Term_prod_summable z

Premises used: _private.0.EisensteinSeries.G2Term_prod_summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Summable (α := ℂ) (β := ℤ × ℤ) (Function.uncurry fun (m n : ℤ) ↦ G2Term z ![m, n])

Tactic:
exact G2Term_prod_summable z

Premises used: _private.0.EisensteinSeries.G2Term_prod_summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ ∀ (b : ℤ), Summable (α := ℂ) fun (n : ℤ) ↦ G2Term z ![b, n]

Tactic:
(G2Term_prod_summable z).prod_factor

Premises used: _private.0.EisensteinSeries.G2Term_prod_summable, Summable.prod_factor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ ∀ (b : ℤ), Summable (α := ℂ) fun (n : ℤ) ↦ G2Term z ![b, n]

Tactic:
exact (G2Term_prod_summable z).prod_factor

Premises used: _private.0.EisensteinSeries.G2Term_prod_summable, Summable.prod_factor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Summable (G2Term z)

Tactic:
have H := G2Term_summable z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
H : Summable (G2Term z)
⊢ Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))

Tactic:
rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at H

Premises used: Equiv.trans, Equiv.prodComm, Equiv.summable_iff, Equiv.symm, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
H :
  Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
⊢ ∀ (c : ℤ), Summable (α := ℂ) fun (b : ℤ) ↦ G2Term z ![b, c]

Tactic:
H.prod_factor

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, Summable.prod_factor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
H :
  Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
⊢ ∀ (c : ℤ), Summable (α := ℂ) fun (b : ℤ) ↦ G2Term z ![b, c]

Tactic:
exact H.prod_factor

Premises used: Summable.prod_factor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)
rw₃ rw₄ : Eq (α := ℂ) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])
⊢ G2 z = (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ)

Tactic:
rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]

Premises used: _private.0.EisensteinSeries.G2_eq_tsum_G2Term, _private.0.EisensteinSeries.G2_S_action_eq_tsum_G2Term, _private.0.EisensteinSeries.tsum_G2Term_eq_tsum, _private.0.EisensteinSeries.tsum_G2Term_eq_tsum'
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
h :
  ∀ (z : ℍ),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 T G2 z = G2 z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 T G2 = G2

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
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
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 T G2 z = G2 z

Tactic:
simp_rw [SL_slash_def, modular_T_smul z]

Premises used: ModularForm.SL_slash_def, UpperHalfPlane.modular_T_smul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
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 : ℕ))
⊢ 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 [G2_eq_tsum_cexp, T, denom_apply, ← exp_periodic.nat_mul 1 (2 * π * I * z)]

Premises used: Real.pi, HMul.hMul, UpperHalfPlane.coe, ModularGroup.denom_apply, Function.Periodic.nat_mul, Complex.exp_periodic, ModularGroup.T, Complex.ofReal, EisensteinSeries.G2_eq_tsum_cexp, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ 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:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ : SL(2, ℤ)
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ

Tactic:
simp [SpecialLinearGroup.SL2Z_generators]

Premises used: SpecialLinearGroup.SL2Z_generators
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ : SL(2, ℤ)
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ

Tactic:
have : γ ∈ Subgroup.closure {S, T} := by simp [SpecialLinearGroup.SL2Z_generators]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ : SL(2, ℤ)
⊢ @SlashAction.map ℤ SL(2, ℤ) _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 1 G2 =
    G2 - D2 1

Tactic:
simp only [SlashAction.slash_one, D2_one, sub_zero]

Premises used: sub_zero, SlashAction.slash_one, EisensteinSeries.D2_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ g : SL(2, ℤ)
hg : Membership.mem (γ := Set SL(2, ℤ)) {S, T} g
⊢ g = S ∨ g = T

Tactic:
simp only [mem_insert_iff, mem_singleton_iff] at hg

Premises used: Set.mem_singleton_iff, Set.mem_insert_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
mem₁ :
  ∀ (h2 : g = T),
    @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

Tactic:
rcases hg with (h1 | h2)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ g : SL(2, ℤ)
h1 : g = S
mem :
  ∀ (z : ℍ),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 z =
      (G2 - D2 g) z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
mem :
  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 : ℂ)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 z =
    (G2 - D2 g) 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]

Premises used: EisensteinSeries.G2, EisensteinSeries.D2_S, EisensteinSeries.G2_S_transform, UpperHalfPlane.modular_S_smul, SlashInvariantForm.slash_S_apply, mul_comm, OfNat.ofNat, Pi.sub_apply
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
mem :
  HPow.hPow (β := ℤ) (↑z : ℂ) (-2) * G2 { coe := -(↑z : ℂ)⁻¹, coe_im_pos := ⋯ : ℍ } =
    HPow.hPow (β := ℕ) (↑z : ℂ)⁻¹ 2 * G2 { coe := -(↑z : ℂ)⁻¹, coe_im_pos := ⋯ : ℍ }
⊢ 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 : ℂ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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 := ⋯ : ℍ }

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ g : SL(2, ℤ)
h2 : g = T
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g

Tactic:
simpa only [h2, D2_T, sub_zero] using G2_T_transform

Premises used: sub_zero, EisensteinSeries.D2_T, EisensteinSeries.G2_T_transform
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
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)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 (g * h) G2 =
    G2 - D2 (g * h)

Tactic:
rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]

Premises used: sub_eq_add_neg, SlashAction.slash_mul, SlashAction.add_slash, EisensteinSeries.D2_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
⊢ 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:
grind [SlashAction.neg_slash, SL_slash]

Premises used: ModularForm.SL_slash, SlashAction.neg_slash
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
rw 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)
⊢ @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:
rw [ig]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)

Tactic:
have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)
⊢ 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

Premises used: ModularForm.SL_slash, sub_eq_add_neg, SlashAction.slash_one, SlashAction.neg_slash, SlashAction.slash_mul, SlashAction.add_slash, mul_inv_cancel
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)
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⁻¹
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 = G2 - D2 g⁻¹

Tactic:
nth_rw 2 [H1]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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⁻¹ (D2 g) = -D2 g⁻¹

Tactic:
have := D2_inv g