-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : Eq.{u + 1} (α := FreeGroup α) ((fun (a : FreeGroup α) ↦ a ^ n) x) ((fun (a : FreeGroup α) ↦ a ^ n) y)
let let₁ let₂ let₃ : x = y
let₄ : ∀ (heq₂ : x ^ (2 * n) = y ^ (2 * n)), x = y
let₅ :
  let g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) := fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord));
  ∀ (heq₂ : x ^ (2 * n) = y ^ (2 * n)) (heq : g x n = g y n), x = y
let₆ :
  let g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) := fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord));
  ∀ (heq : g x n = g y n) (heq₂ : g x (2 * n) = g y (2 * n)), x = y
let₇ :
  let f : (a : FreeGroup α) → (n : ℕ) → ℕ := fun (a : FreeGroup α) (n : ℕ) ↦
    (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length);
  let g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) := fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord));
  ∀ (heq : g x n = g y n) (heq₂ : g x (2 * n) = g y (2 * n)) (leq : f x n = f y n), x = y
let₈ :
  let f : (a : FreeGroup α) → (n : ℕ) → ℕ := fun (a : FreeGroup α) (n : ℕ) ↦
    (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length);
  let g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) := fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord));
  ∀ (heq : g x n = g y n) (heq₂ : g x (2 * n) = g y (2 * n)) (leq : f x n = f y n) (leq₂ : f x (2 * n) = f y (2 * n)),
    x = y
let₉ :
  let f : (a : FreeGroup α) → (n : ℕ) → ℕ := fun (a : FreeGroup α) (n : ℕ) ↦
    (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length);
  let g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) := fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord));
  ∀ (heq : g x n = g y n) (heq₂ : g x (2 * n) = g y (2 * n)) (leq : f x n = f y n) (leq₂ : f x (2 * n) = f y (2 * n))
    (hc : conjugator x.toWord = conjugator y.toWord)
    (heq' :
      (replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
        (replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)),
    x = y
⊢ x = y
have let₁₀ : let f : (a : FreeGroup α) → (n : ℕ) → ℕ := fun (a : FreeGroup α) (n : ℕ) ↦
  (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length);
let g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) := fun (a : FreeGroup α) (k : ℕ) ↦
  conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord));
∀ (hc : conjugator x.toWord = conjugator y.toWord) (n : ℕ) (hn : n + 1 ≠ 0) (heq : g x (n + 1) = g y (n + 1))
  (heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))) (leq : f x (n + 1) = f y (n + 1))
  (leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1)))
  (heq' :
    (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
      (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)),
  x = y
Tactic: classical
    let f (a : FreeGroup α) (n : ℕ) : ℕ :=
        (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length +
          (conjugator a.toWord).length)
    let g (a : FreeGroup α) (k : ℕ) : List (α × Bool) :=
        conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++
          invRev (conjugator a.toWord))
    have heq₂ : x ^ (2 * n) = y ^ (2 * n) := by simp_rw [mul_comm, pow_mul, heq]
    replace heq : g x n = g y n := by
      simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq
    replace heq₂ : g x (2 * n) = g y (2 * n) := by
      simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq₂
    have leq : f x n = f y n := by simpa [g] using congr_arg List.length heq
    have leq₂ : f x (2 * n) = f y (2 * n) := by simpa [g] using congr_arg List.length heq₂
    obtain ⟨hc, heq'⟩ := List.append_inj heq (by grind)
    obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    have hm : reduceCyclically x.toWord = reduceCyclically y.toWord := by
      simp only [replicate_succ, flatten_cons, append_assoc] at heq'
      exact (List.append_inj heq' <| mul_left_cancel₀ hn <| by grind).1
    have := congr_arg mk <| (conj_conjugator_reduceCyclically x.toWord).symm
    rwa [hc, hm, conj_conjugator_reduceCyclically, mk_toWord, mk_toWord] at this
Cleared hypotheses: n, hn, heq