awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n : ℕ
hn : n ≠ 0
⊢ IsReduced (L₁ ++ (replicate n L₂).flatten ++ L₃)

Tactic:
match n with
  | 0 => contradiction
  | n + 1 =>
    if h : L₂ = [] then simp_all else
    have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]
    refine IsReduced.append_overlap ?_ ?_ (hn := h')
    · rw [replicate_succ, flatten_cons, ← append_assoc]
      refine IsReduced.append_overlap (h₂.infix ⟨[], L₃, by simp⟩) ?_ h
      rw [← flatten_cons, ← replicate_succ]
      exact (h₁.flatten_replicate _).isReduced
    · rw [replicate_succ', flatten_concat]
      refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h
      rw [← flatten_concat, ← replicate_succ']
      exact (h₁.flatten_replicate _).isReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
⊢ Eq.{u + 1} (α := List (α × Bool)) (reduceCyclically []) []

Tactic:
simp [reduceCyclically]

Premises used: FreeGroup.reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
⊢ reduceCyclically [a] = [a]

Tactic:
simp [reduceCyclically]

Premises used: FreeGroup.reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a b : α × Bool
L : List (α × Bool)
⊢ reduceCyclically (a :: (L ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically L else a :: L ++ [b]

Tactic:
simp [reduceCyclically]

Premises used: FreeGroup.reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
induction : ∀ (h : IsReduced.{u} (α := α) []), IsCyclicallyReduced.{u} (α := α) (reduceCyclically [])
induction₁ : ∀ (a : α × Bool) (h : IsReduced [a]), IsCyclicallyReduced (reduceCyclically [a])
cons_append :
  ∀ (a : α × Bool) (l : List (α × Bool)) (b : α × Bool),
    (∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)) →
      ∀ (h : IsReduced (a :: (l ++ [b]))), IsCyclicallyReduced (reduceCyclically (a :: (l ++ [b])))
⊢ IsCyclicallyReduced (reduceCyclically L)

Tactic:
induction L using List.bidirectionalRec
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced.{u} (α := α) []
⊢ IsCyclicallyReduced.{u} (α := α) (reduceCyclically [])

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced.{u} (α := α) []
⊢ IsCyclicallyReduced.{u} (α := α) (reduceCyclically [])

Tactic:
case nil => simp

Premises used: List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
h : IsReduced [a]
⊢ IsCyclicallyReduced (reduceCyclically [a])

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
h : IsReduced [a]
⊢ IsCyclicallyReduced (reduceCyclically [a])

Tactic:
case singleton => simp

Premises used: Singleton.singleton
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
rw : IsCyclicallyReduced (if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b])
⊢ IsCyclicallyReduced (reduceCyclically (a :: (l ++ [b])))

Tactic:
rw [reduceCyclically.cons_append]

Premises used: FreeGroup.reduceCyclically.cons_append
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
split : b.1 = a.1 ∧ (!b.2) = a.2 → IsCyclicallyReduced (reduceCyclically l)
isFalse : ¬(b.1 = a.1 ∧ (!b.2) = a.2) → IsCyclicallyReduced (a :: l ++ [b])
⊢ IsCyclicallyReduced (if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b])

Tactic:
split
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h_1 : b.1 = a.1 ∧ (!b.2) = a.2
⊢ IsCyclicallyReduced (reduceCyclically l)

Tactic:
ih (h.infix ⟨[a], [b], rfl⟩)

Premises used: List.cons, Exists.intro, FreeGroup.IsReduced.infix, rfl, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h_1 : b.1 = a.1 ∧ (!b.2) = a.2
⊢ IsCyclicallyReduced (reduceCyclically l)

Tactic:
exact ih (h.infix ⟨[a], [b], rfl⟩)

Premises used: List.cons, Exists.intro, FreeGroup.IsReduced.infix, rfl, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h_1 : b.1 = a.1 ∧ (!b.2) = a.2
⊢ IsCyclicallyReduced (reduceCyclically l)

Tactic:
case isTrue => exact ih (h.infix ⟨[a], [b], rfl⟩)

Premises used: Decidable.isTrue, List.cons, Exists.intro, FreeGroup.IsReduced.infix, rfl, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h' : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
rw : IsReduced (a :: l ++ [b]) ∧ (b.1 = a.1 → b.2 = a.2)
⊢ IsCyclicallyReduced (a :: l ++ [b])

Tactic:
rw [isCyclicallyReduced_cons_append_iff]

Premises used: FreeGroup.isCyclicallyReduced_cons_append_iff
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h' : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ b.1 = a.1 → b.2 = a.2

Tactic:
simpa using h'
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : ∀ (h : IsReduced l), IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h' : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ IsReduced (a :: l ++ [b]) ∧ (b.1 = a.1 → b.2 = a.2)

Tactic:
exact ⟨h, by simpa using h'⟩
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
⊢ Eq.{u + 1} (α := List (α × Bool)) (conjugator []) []

Tactic:
simp [conjugator]

Premises used: FreeGroup.reduceCyclically.conjugator
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
⊢ conjugator [a] = []

Tactic:
simp [conjugator]

Premises used: FreeGroup.reduceCyclically.conjugator
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a b : α × Bool
L : List (α × Bool)
⊢ conjugator (a :: (L ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator L else []

Tactic:
simp [conjugator]

Premises used: FreeGroup.reduceCyclically.conjugator
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
L : List (α × Bool)
induction : HAppend.hAppend (α := List (α × Bool)) (conjugator []) (reduceCyclically []) ++ invRev (conjugator []) = []
induction₁ : ∀ (a : α × Bool), conjugator [a] ++ reduceCyclically [a] ++ invRev (conjugator [a]) = [a]
cons_append :
  ∀ (a : α × Bool) (l : List (α × Bool)) (b : α × Bool),
    conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l →
      conjugator (a :: (l ++ [b])) ++ reduceCyclically (a :: (l ++ [b])) ++ invRev (conjugator (a :: (l ++ [b]))) =
        a :: (l ++ [b])
⊢ conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L

Tactic:
induction L using List.bidirectionalRec
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
⊢ HAppend.hAppend (α := List (α × Bool)) (conjugator []) (reduceCyclically []) ++ invRev (conjugator []) = []

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
⊢ HAppend.hAppend (α := List (α × Bool)) (conjugator []) (reduceCyclically []) ++ invRev (conjugator []) = []

Tactic:
case nil => simp

Premises used: List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
⊢ conjugator [a] ++ reduceCyclically [a] ++ invRev (conjugator [a]) = [a]

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
⊢ conjugator [a] ++ reduceCyclically [a] ++ invRev (conjugator [a]) = [a]

Tactic:
case singleton => simp

Premises used: Singleton.singleton
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
rw :
  ((if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator l else []) ++
        if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b]) ++
      invRev (if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator l else []) =
    a :: (l ++ [b])
⊢ conjugator (a :: (l ++ [b])) ++ reduceCyclically (a :: (l ++ [b])) ++ invRev (conjugator (a :: (l ++ [b]))) =
    a :: (l ++ [b])

Tactic:
rw [reduceCyclically.cons_append, conjugator.cons_append]

Premises used: FreeGroup.reduceCyclically.conjugator.cons_append, FreeGroup.reduceCyclically.cons_append
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
isTrue :
  b.1 = a.1 ∧ (!b.2) = a.2 → a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) = a :: (l ++ [b])
split : ¬(b.1 = a.1 ∧ (!b.2) = a.2) → [] ++ (a :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])
⊢ ((if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator l else []) ++
        if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b]) ++
      invRev (if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator l else []) =
    a :: (l ++ [b])

Tactic:
split
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : b.1 = a.1 ∧ (!b.2) = a.2
nth_rw :
  a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) =
    a :: (conjugator l ++ reduceCyclically l ++ invRev (conjugator l) ++ [b])
⊢ a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) = a :: (l ++ [b])

Tactic:
nth_rw 4 [← eq]
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : b.1 = a.1 ∧ (!b.2) = a.2
⊢ a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) =
    a :: (conjugator l ++ reduceCyclically l ++ invRev (conjugator l) ++ [b])

Tactic:
simp [invRev, h.1.symm, h.2.symm]

Premises used: FreeGroup.invRev, And.right, And.left, Eq.symm
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : b.1 = a.1 ∧ (!b.2) = a.2
⊢ a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) = a :: (l ++ [b])

Tactic:
case isTrue h =>
      nth_rw 4 [← eq]
      simp [invRev, h.1.symm, h.2.symm]

Premises used: Decidable.isTrue, FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ [] ++ (a :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ [] ++ (a :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])

Tactic:
case isFalse => simp

Premises used: Decidable.isFalse
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
induction :
  reduce (replicate (HAdd.hAdd (α := ℕ) 0 1) L).flatten =
    conjugator L ++ (replicate (HAdd.hAdd (α := ℕ) 0 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
succ :
  ∀ (n : ℕ),
    reduce (replicate (n + 1) L).flatten =
        conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L) →
      reduce (replicate (n + 1 + 1) L).flatten =
        conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
⊢ reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
induction n
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
⊢ reduce (replicate (HAdd.hAdd (α := ℕ) 0 1) L).flatten =
    conjugator L ++ (replicate (HAdd.hAdd (α := ℕ) 0 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
simpa [← append_assoc, conj_conjugator_reduceCyclically, ← isReduced_iff_reduce_eq]

Premises used: List.append_assoc, FreeGroup.isReduced_iff_reduce_eq, FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
⊢ reduce (replicate (HAdd.hAdd (α := ℕ) 0 1) L).flatten =
    conjugator L ++ (replicate (HAdd.hAdd (α := ℕ) 0 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
case zero =>
    simpa [← append_assoc, conj_conjugator_reduceCyclically, ← isReduced_iff_reduce_eq]

Premises used: List.append_assoc, FreeGroup.isReduced_iff_reduce_eq, FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
rw :
  reduce (L ++ (conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
⊢ reduce (replicate (n + 1 + 1) L).flatten =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
rw [replicate_succ, flatten_cons, ← reduce_append_reduce_reduce, ih, h.reduce_eq]

Premises used: FreeGroup.reduce_append_reduce_reduce, FreeGroup.IsReduced.reduce_eq, List.replicate_succ, List.flatten_cons
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
nth_rewrite :
  reduce
      (conjugator L ++ reduceCyclically L ++ invRev (conjugator L) ++
        (conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
⊢ reduce (L ++ (conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
nth_rewrite 1 [← conj_conjugator_reduceCyclically L]

Premises used: FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
H : mk (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
apply reduce.sound

Premises used: FreeGroup.reduce.sound
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * (mk L₃)⁻¹ * (mk L₃ * mk L₄ * mk L₅) = mk L₁ * (mk L₂ * mk L₄) * mk L₅

Tactic:
group
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
⊢ ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
have {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)} : reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) =
        reduce (L₁ ++ (L₂ ++ L₄) ++ L₅) := by
      apply reduce.sound
      repeat rw [← mul_mk]
      rw [← inv_mk]
      group
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
rw : IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))
⊢ reduce
      (conjugator L ++ reduceCyclically L ++ invRev (conjugator L) ++
        (conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
rw [this, ← flatten_cons, ← replicate_succ, ← isReduced_iff_reduce_eq]

Premises used: FreeGroup.isReduced_iff_reduce_eq, List.replicate_succ, List.flatten_cons
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
h₁ : IsCyclicallyReduced (reduceCyclically L)
h₂ : IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))
⊢ n + 1 + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
h₁ : IsCyclicallyReduced (reduceCyclically L)
h₂ : IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))
⊢ IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))

Tactic:
apply IsReduced.append_flatten_replicate_append (hn := by simp)

Premises used: FreeGroup.IsReduced.append_flatten_replicate_append
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsCyclicallyReduced (reduceCyclically L)

Tactic:
isCyclicallyReduced h

Premises used: FreeGroup.reduceCyclically.isCyclicallyReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsCyclicallyReduced (reduceCyclically L)

Tactic:
exact isCyclicallyReduced h

Premises used: FreeGroup.reduceCyclically.isCyclicallyReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
h₂ h₃ h₄ h₅ : IsReduced L
⊢ IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))

Tactic:
rwa [conj_conjugator_reduceCyclically]

Premises used: FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
⊢ reduce (replicate 0 L).flatten =
    if Eq (α := ℕ) 0 0 then [] else conjugator L ++ (replicate 0 (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
f : (a : FreeGroup α) → (n : ℕ) → ℕ :=
  fun (a : FreeGroup α) (n : ℕ) ↦
    (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) :=
  fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
simp_rw : x ^ (n * 2) = y ^ (n * 2)
simp_rw₁ : HPow.hPow (β := ℕ) (x ^ n) 2 = HPow.hPow (β := ℕ) (y ^ n) 2
⊢ x ^ (2 * n) = y ^ (2 * n)

Tactic:
simp_rw [mul_comm, pow_mul, heq]

Premises used: pow_mul, mul_comm
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
f : (a : FreeGroup α) → (n : ℕ) → ℕ :=
  fun (a : FreeGroup α) (n : ℕ) ↦
    (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : (a : FreeGroup α) → (k : ℕ) → List (α × Bool) :=
  fun (a : FreeGroup α) (k : ℕ) ↦
    conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
⊢ x ^ (2 * n) = y ^ (2 * n)

Tactic:
have heq₂ : x ^ (2 * n) = y ^ (2 * n) := by simp_rw [mul_comm, pow_mul, heq]