-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
h0 :
  ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 0 0 =
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ∧
    ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 0 1 =
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1 +
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ∧
      ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0 =
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
            (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ∧
        ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 1 =
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1 +
            (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1
simp :
  (HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) +
        HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) *
      ((↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        (HMul.hMul (α := ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) -
          HMul.hMul (α := ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ)
            (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        ((HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) +
              HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)
                (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) *
            (↑z : ℂ) +
          (HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
              (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) +
            HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)
              (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))
⊢ (↑((↑(A * B) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
      denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) B))
        (↑z : ℂ) =
    HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑(↑B : Matrix (Fin 2) (Fin 2) ℤ).det : ℂ) +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        denom
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) B) :
              GL (Fin 2) ℝ))
          (↑z : ℂ)

Tactic:
simp only [Fin.isValue, coe_mul, h0.2.2.1, Int.cast_add, Int.cast_mul, ModularGroup.denom_apply,
    Matrix.det_fin_two B.1, Int.cast_sub, ← map_mul, h0.2.2.2]

Premises used: Int.cast_sub, ModularGroup.denom_apply, Int.cast_add, map_mul, Int.cast_mul, And.right, Fin.isValue, And.left, Matrix.det_fin_two, Subtype.val, Matrix.SpecialLinearGroup.coe_mul