-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
rw :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      (HSMul.hSMul (α := ℚ) (↑(a₁ * a₂ * M) : ℚ)
        (HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)))
rw₁ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) •
      HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
rw₂ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
rw₃ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₂ * a₁ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
rw₄ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    ((↑A₂.den : ℚ)⁻¹ * HMul.hMul (α := ℚ) (↑(a₂ * a₁) : ℚ) (↑M : ℚ) * (↑A₁.den : ℚ)⁻¹) •
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
⊢ M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
have rw₅ : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  ((↑A₂.den : ℚ)⁻¹ * (HMul.hMul (α := ℚ) (↑a₂ : ℚ) (↑a₁ : ℚ) * (↑M : ℚ)) * (↑A₁.den : ℚ)⁻¹) •
    (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]