Lean 4 (non-competing), 1057 bytes

This is non-competing due to using Lean 4, instead of Lean 3 as required in the question. Specifically this utilizes the builtin grind tactic a lot, which was only released at the beginning of this month. I am not counting the size of the formalized statement in the byte count, only stuff I added (and the import Mathlib line).

import Mathlib

inductive bracket_t
| left
| right

inductive balanced : List bracket_t → Prop
| empty : balanced []
| wrap (initial : List bracket_t) : balanced initial → balanced ([bracket_t.left] ++ initial ++ [bracket_t.right])
| append (initial1 initial2 : List bracket_t) : balanced initial1 → balanced initial2 → balanced (initial1 ++ initial2)

def balance_factor : ∀ length : ℕ, ∀ string : List bracket_t, ℤ
| 0, _ => 0
| _, [] => 0
| n + 1, bracket_t.left::rest => 1 + balance_factor n rest
| n + 1, bracket_t.right::rest => -1 + balance_factor n rest

def balance_factor_predicate (string : List bracket_t) := balance_factor string.length string = 0 ∧ ∀ n : ℕ, n < string.length → 0 ≤ balance_factor n string

attribute [grind,simp] balance_factor balance_factor_predicate
macro"g":tactic=>`(tactic|first|grind|simp_all)
@[simp,grind]
theorem A:∀n≤a.length,balance_factor n (a++b)=balance_factor n a:=by
induction' a with a
g
rintro(_|_)<;>cases a<;>g
@[simp,grind]
lemma B:∀n>a.length,balance_factor n (a++b)=balance_factor a.length a+balance_factor (n-a.length) b:=by
induction' a with a
g
rintro(_|_)<;>cases a<;>g
lemma X (string : List bracket_t) : balanced string ↔ balance_factor_predicate string :=
⟨λh↦by induction h;g;simp_all;rintro(_|_)_<;>g;g,λh↦by
by_cases H:∃n<string.length,0<n∧balance_factor n string=0
obtain⟨n,o,t⟩:=H
obtain⟨a,b,rfl,rfl⟩:∃a b,a++b=_∧a.length=n:= ⟨_,_,string.take_append_drop n,by g⟩
simp at o h
apply balanced.append<;>(rw[X];g;intro n;have:=h.2 n;have:=h.2 (a.length + n);g)
rcases string with _|⟨a,b⟩<;>simp_all[balanced.empty]
have:0≤balance_factor 1 (a::b):=by g
cases a<;>g
cases b using List.reverseRecOn<;>g
rename_i b a
cases a
have:=h.2 (b.length+1)
g
apply balanced.wrap
rw [X]
g
intro n
have:=h.2 (n+1)
g⟩
termination_by string.length
decreasing_by
g;g;g

Try it online!

Ungolfed:

import Mathlib

inductive bracket_t
| left
| right

inductive balanced : List bracket_t → Prop
| empty : balanced []
| wrap (initial : List bracket_t) : balanced initial → balanced ([bracket_t.left] ++ initial ++ [bracket_t.right])
| append (initial1 initial2 : List bracket_t) : balanced initial1 → balanced initial2 → balanced (initial1 ++ initial2)

def balance_factor : ℕ → List bracket_t → ℤ
| 0, _ => 0
| _, [] => 0
| n + 1, bracket_t.left::rest => 1 + balance_factor n rest
| n + 1, bracket_t.right::rest => -1 + balance_factor n rest

def balance_factor_predicate (string : List bracket_t) := balance_factor string.length string = 0 ∧ ∀ n : ℕ, n < string.length → 0 ≤ balance_factor n string

attribute [grind,simp] balance_factor balance_factor_predicate

@[simp,grind]
lemma balance_factor_of_le  : ∀ n ≤ a.length, balance_factor n (a ++ b) = balance_factor n a := by
  induction' a with a _
  · simp
  · rintro (_|_) <;> cases a <;> grind

@[simp,grind]
lemma balance_factor_of_lt : ∀ n > a.length, balance_factor n (a ++ b) = balance_factor a.length a + balance_factor (n - a.length) b := by
  induction' a with a _
  · simp
  · rintro (_|_) <;> cases a <;> grind

lemma X (string : List bracket_t) : balanced string ↔ balance_factor_predicate string := by
  constructor <;> intro h
  · induction h
    · grind
    · simp_all
      rintro (_|_) _ <;> grind
    · grind
  · by_cases hs : ∃ n < string.length, 0 < n ∧ balance_factor n string = 0
    · obtain ⟨n, h1, h2⟩ := hs
      obtain ⟨a, b, rfl, rfl⟩ : ∃ a b, a ++ b = string ∧ a.length = n := ⟨_, _, string.take_append_drop n, by grind⟩
      simp at h1
      apply balanced.append <;> rw [X]
      · simp at h
        simp_all
        intro n
        have := h.2 n
        grind
      · simp at h
        simp_all
        intro n
        have := h.2 (a.length + n)
        grind
    · rcases string with _|⟨a,b⟩ <;> simp_all [balanced.empty]
      have : 0 ≤ balance_factor 1 (a :: b) := by grind
      cases a <;> simp_all
      cases b using List.reverseRecOn <;> simp_all [-List.cons_append_fun, ← List.cons_append]
      rename_i b a
      cases a
      · have := h.2 (b.length + 1) (by grind)
        grind
      · apply balanced.wrap
        rw [X]
        simp_all
        intro n _
        have := h.2 (n + 1) (by grind)
        grind
termination_by string.length
decreasing_by
  all_goals grind

Try it online!