-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
a :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₁ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₂ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₃ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₄ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₅ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₆ a₇ a₈ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₉ a₁₀ a₁₁ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₁₂ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₁₃ :
  ∀ (hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
      !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto