-- 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)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
a :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M)) z
        i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₃ :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (1 + M • (A₁.num * k * A₂.num)) i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₄ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          1 :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
a₅ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
a₆ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
      ((M • (A₁.num * k * A₂.num)).map (⇑(Int.castRingHom (ZMod M)) : (a : ℤ) → ZMod M)) i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
a₇ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
      ((M • (A₁.num * k * A₂.num)).map fun (x : ℤ) ↦ (↑x : ZMod M)) i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
⊢ Eq (α := ZMod M)
    ((↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M)) : (a : SL(2, ℤ)) → SL(2, ZMod M))
            (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j)
have a₈ : HAdd.hAdd (α := ZMod M) (1 i j) ((M • (A₁.num * k * A₂.num)).map (fun (x : ℤ) ↦ (↑x : ZMod M)) i j) =
  (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
Tactic: simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
    Int.cast_natCast, ZMod.natCast_self M, zero_mul]