awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)
have refine_2 : IsReduced ((replicate n L₂).flatten ++ L₂)
Tactic: refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced ((replicate n L₂).flatten ++ L₂)
have refine_2 : IsReduced (replicate (n + 1) L₂).flatten
Tactic: rw [← flatten_concat, ← replicate_succ']
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
have if : ∀ (h : L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
Tactic: 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
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
if : ∀ (h : L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
have if₁ : ∀ (h : ¬L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
Tactic: 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
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
⊢ IsCyclicallyReduced (reduceCyclically L)
have induction : ∀ (h : IsReduced.{u} (α := α) []), IsCyclicallyReduced.{u} (α := α) (reduceCyclically [])
Tactic: induction L using List.bidirectionalRec
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
induction : ∀ (h : IsReduced.{u} (α := α) []), IsCyclicallyReduced.{u} (α := α) (reduceCyclically [])
⊢ IsCyclicallyReduced (reduceCyclically L)
have induction₁ : ∀ (a : α × Bool) (h : IsReduced [a]), IsCyclicallyReduced (reduceCyclically [a])
Tactic: induction L using List.bidirectionalRec
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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])
⊢ IsCyclicallyReduced (reduceCyclically L)
have 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])))
Tactic: induction L using List.bidirectionalRec
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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]))
⊢ IsCyclicallyReduced (reduceCyclically (a :: (l ++ [b])))
have rw : IsCyclicallyReduced (if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b])
Tactic: rw [reduceCyclically.cons_append]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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]))
⊢ IsCyclicallyReduced (if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b])
have split : b.1 = a.1 ∧ (!b.2) = a.2 → IsCyclicallyReduced (reduceCyclically l)
Tactic: split
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ IsCyclicallyReduced (if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b])
have isFalse : ¬(b.1 = a.1 ∧ (!b.2) = a.2) → IsCyclicallyReduced (a :: l ++ [b])
Tactic: split
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ IsCyclicallyReduced (a :: l ++ [b])
have rw : IsReduced (a :: l ++ [b]) ∧ (b.1 = a.1 → b.2 = a.2)
Tactic: rw [isCyclicallyReduced_cons_append_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
inst : DecidableEq α
L : List (α × Bool)
⊢ conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L
have induction : HAppend.hAppend (α := List (α × Bool)) (conjugator []) (reduceCyclically []) ++ invRev (conjugator []) = []
Tactic: induction L using List.bidirectionalRec
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
inst : DecidableEq α
L : List (α × Bool)
induction : HAppend.hAppend (α := List (α × Bool)) (conjugator []) (reduceCyclically []) ++ invRev (conjugator []) = []
⊢ conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L
have induction₁ : ∀ (a : α × Bool), conjugator [a] ++ reduceCyclically [a] ++ invRev (conjugator [a]) = [a]
Tactic: induction L using List.bidirectionalRec
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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]
⊢ conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L
have 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])
Tactic: induction L using List.bidirectionalRec
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
⊢ conjugator (a :: (l ++ [b])) ++ reduceCyclically (a :: (l ++ [b])) ++ invRev (conjugator (a :: (l ++ [b]))) =
    a :: (l ++ [b])
have 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])
Tactic: rw [reduceCyclically.cons_append, conjugator.cons_append]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
⊢ ((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])
have isTrue : b.1 = a.1 ∧ (!b.2) = a.2 → a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) = a :: (l ++ [b])
Tactic: split
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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])
⊢ ((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])
have split : ¬(b.1 = a.1 ∧ (!b.2) = a.2) → [] ++ (a :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])
Tactic: split
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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])
have nth_rw : a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) =
  a :: (conjugator l ++ reduceCyclically l ++ invRev (conjugator l) ++ [b])
Tactic: nth_rw 4 [← eq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
n : ℕ
⊢ reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
have induction : reduce (replicate (HAdd.hAdd (α := ℕ) 0 1) L).flatten =
  conjugator L ++ (replicate (HAdd.hAdd (α := ℕ) 0 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
have 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)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ reduce (replicate (n + 1 + 1) L).flatten =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
have 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)
Tactic: rw [replicate_succ, flatten_cons, ← reduce_append_reduce_reduce, ih, h.reduce_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ 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)
have 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)
Tactic: nth_rewrite 1 [← conj_conjugator_reduceCyclically L]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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₅)
have H : mk (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Tactic: apply reduce.sound
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
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)
⊢ 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)
have this : ∀ {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
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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₅)
⊢ 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)
have rw : IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))
Tactic: rw [this, ← flatten_cons, ← replicate_succ, ← isReduced_iff_reduce_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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₅)
⊢ IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))
have h₁ : IsCyclicallyReduced (reduceCyclically L)
Tactic: apply IsReduced.append_flatten_replicate_append (hn := by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))
have h₂ : IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))
Tactic: apply IsReduced.append_flatten_replicate_append (hn := by simp)
-- 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)
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)
have simp_rw : x ^ (n * 2) = y ^ (n * 2)
Tactic: simp_rw [mul_comm, pow_mul, heq]
-- 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)
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)
⊢ x ^ (2 * n) = y ^ (2 * n)
have simp_rw₁ : HPow.hPow (β := ℕ) (x ^ n) 2 = HPow.hPow (β := ℕ) (y ^ n) 2
Tactic: simp_rw [mul_comm, pow_mul, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
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 = y
have heq₂ : x ^ (2 * n) = y ^ (2 * n)
Tactic: have heq₂ : x ^ (2 * n) = y ^ (2 * n) := by simp_rw [mul_comm, pow_mul, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
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))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ x = y
have heq₁ : g x n = g y n
Tactic: replace heq : g x n = g y n := by
      simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
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))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
heq : g x n = g y n
⊢ x = y
have heq₃ : g x (2 * n) = g y (2 * n)
Tactic: 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₂
Cleared hypotheses: heq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
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))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
⊢ x = y
have leq : f x n = f y n
Tactic: have leq : f x n = f y n := by simpa [g] using congr_arg List.length heq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
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))
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
have leq₂ : f x (2 * n) = f y (2 * n)
Tactic: have leq₂ : f x (2 * n) = f y (2 * n) := by simpa [g] using congr_arg List.length heq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
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))
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
have hc : conjugator x.toWord = conjugator y.toWord
Tactic: obtain ⟨hc, heq'⟩ := List.append_inj heq (by grind)