-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
h :
  (∃ y ∈ Γ,
      (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
        HMul.hMul (β := GL (Fin 2) ℝ)
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
              GL (Fin 2) ℝ))
          (((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))⁻¹ :
            GL (Fin 2) ℝ)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
h₁ :
  (∃ y ∈ Γ,
      (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
        HMul.hMul (β := GL (Fin 2) ℝ)
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
              GL (Fin 2) ℝ))
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
h₂ :
  (∃ y ∈ Γ,
      Eq (α := GL (Fin 2) ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) :
          GL (Fin 2) ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (g * x * g⁻¹)) :
          GL (Fin 2) ℝ)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
h₃ :
  (∃ y ∈ Γ,
      Eq (α := SL(2, ℝ)) ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y : SL(2, ℝ))
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (g * x * g⁻¹) : SL(2, ℝ))) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
⊢ x ∈
      conjGL Γ
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
have h₄ : (∃ y ∈ Γ, y = g * x * g⁻¹) ↔
  x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
Tactic: simp_rw [mem_conjGL, ← map_inv, ← map_mul, toGL_injective.eq_iff, map_intCast_injective.eq_iff,
    exists_eq_right, toConjAct_inv, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]