-- 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⁻¹
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 =
    @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 -
      -D2 g⁻¹ -
    D2 g⁻¹
Tactic: rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]