-- 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
⊢ 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));
∀ (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
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: heq