awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ g x n = g y n

Tactic:
simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq

Premises used: FreeGroup.toWord, FreeGroup.toWord_pow, congr_arg, FreeGroup.isReduced_toWord, FreeGroup.reduceCyclically.reduce_flatten_replicate
-- 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))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ 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
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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
⊢ g x (2 * n) = g y (2 * n)

Tactic:
simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq₂

Premises used: FreeGroup.toWord, FreeGroup.toWord_pow, congr_arg, FreeGroup.isReduced_toWord, FreeGroup.reduceCyclically.reduce_flatten_replicate
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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
⊢ 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₂
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
⊢ f x n = f y n

Tactic:
simpa [g] using congr_arg List.length heq

Premises used: congr_arg, List.length
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
⊢ f x n = f y n

Tactic:
have leq : f x n = f y n := by simpa [g] using congr_arg List.length heq
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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
⊢ f x (2 * n) = f y (2 * n)

Tactic:
simpa [g] using congr_arg List.length heq₂

Premises used: congr_arg, List.length
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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
⊢ 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₂
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
⊢ (conjugator x.toWord).length = (conjugator y.toWord).length

Tactic:
grind
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
⊢ conjugator x.toWord = conjugator y.toWord

Tactic:
obtain ⟨hc, heq'⟩ := List.append_inj heq (by grind)

Premises used: List.append_inj
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
hc : conjugator x.toWord = conjugator y.toWord
⊢ (replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)

Tactic:
obtain ⟨hc, heq'⟩ := List.append_inj heq (by grind)

Premises used: List.append_inj
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
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)
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)
obtain :
  ∀ (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
⊢ x = y

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
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))
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)
⊢ reduceCyclically x.toWord ++ ((replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord)) =
    reduceCyclically y.toWord ++ ((replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord))

Tactic:
simp only [replicate_succ, flatten_cons, append_assoc] at heq'

Premises used: List.append_assoc, List.replicate_succ, List.flatten_cons
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
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))
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' :
  reduceCyclically x.toWord ++ ((replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord)) =
    reduceCyclically y.toWord ++ ((replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord))
⊢ (n + 1) * (reduceCyclically x.toWord).length = (n + 1) * (reduceCyclically y.toWord).length

Tactic:
grind
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
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))
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' :
  reduceCyclically x.toWord ++ ((replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord)) =
    reduceCyclically y.toWord ++ ((replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord))
⊢ reduceCyclically x.toWord = reduceCyclically y.toWord

Tactic:
exact (List.append_inj heq' <| mul_left_cancel₀ hn <| by grind).1

Premises used: mul_left_cancel₀, And.left, List.append_inj
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
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))
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)
⊢ reduceCyclically x.toWord = reduceCyclically y.toWord

Tactic:
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
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
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))
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)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
⊢ mk x.toWord = mk (conjugator x.toWord ++ reduceCyclically x.toWord ++ invRev (conjugator x.toWord))

Tactic:
have := congr_arg mk <| (conj_conjugator_reduceCyclically x.toWord).symm
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
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))
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)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
this : mk x.toWord = mk (conjugator x.toWord ++ reduceCyclically x.toWord ++ invRev (conjugator x.toWord))
rwa :
  ∀ (this : mk x.toWord = mk (conjugator y.toWord ++ reduceCyclically x.toWord ++ invRev (conjugator y.toWord))), x = y
rwa₁ :
  ∀ (this : mk x.toWord = mk (conjugator y.toWord ++ reduceCyclically y.toWord ++ invRev (conjugator y.toWord))), x = y
rwa₂ : ∀ (this : mk x.toWord = mk y.toWord), x = y
rwa₃ : ∀ (this : x = mk y.toWord), x = y
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : x = y), x = y
⊢ x = y

Tactic:
rwa [hc, hm, conj_conjugator_reduceCyclically, mk_toWord, mk_toWord] at this

Premises used: FreeGroup.mk_toWord, FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
h :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := G) (((↑b.symm : FreeGroup ι →* G) : (a : FreeGroup ι) → G) (FreeGroup.of i) : G)
      (((↑b'.symm : FreeGroup ι →* G) : (a : FreeGroup ι) → G) (FreeGroup.of i) : G)
⊢ Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)

Tactic:
ext i
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
i : ι
⊢ Eq.{u_3 + 1} (α := G) (((↑b.symm : FreeGroup ι →* G) : (a : FreeGroup ι) → G) (FreeGroup.of i) : G)
    (((↑b'.symm : FreeGroup ι →* G) : (a : FreeGroup ι) → G) (FreeGroup.of i) : G)

Tactic:
congr_fun hbb' i

Premises used: congr_fun
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
i : ι
⊢ Eq.{u_3 + 1} (α := G) (((↑b.symm : FreeGroup ι →* G) : (a : FreeGroup ι) → G) (FreeGroup.of i) : G)
    (((↑b'.symm : FreeGroup ι →* G) : (a : FreeGroup ι) → G) (FreeGroup.of i) : G)

Tactic:
exact congr_fun hbb' i

Premises used: congr_fun
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
⊢ Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)

Tactic:
have H : (b.symm : FreeGroup ι →* G) = (b'.symm : FreeGroup ι →* G) := by
      ext i; exact congr_fun hbb' i
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
h :
  ∀ (x : FreeGroup ι),
    Eq.{u_3 + 1} (α := G) ((b.symm : (a : FreeGroup ι) → G) x : G) ((b'.symm : (a : FreeGroup ι) → G) x : G)
⊢ b.symm = b'.symm

Tactic:
ext x
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
x : FreeGroup ι
⊢ Eq.{u_3 + 1} (α := G) ((b.symm : (a : FreeGroup ι) → G) x : G) ((b'.symm : (a : FreeGroup ι) → G) x : G)

Tactic:
DFunLike.congr_fun H x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
x : FreeGroup ι
⊢ Eq.{u_3 + 1} (α := G) ((b.symm : (a : FreeGroup ι) → G) x : G) ((b'.symm : (a : FreeGroup ι) → G) x : G)

Tactic:
exact DFunLike.congr_fun H x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
⊢ b.symm = b'.symm

Tactic:
have : b.symm = b'.symm := by ext x; exact DFunLike.congr_fun H x
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
this : b.symm = b'.symm
rw : b = b'
rw₁ : b.symm.symm = b'
rw₂ : b.symm.symm = b'.symm.symm
rw₃ rw₄ : b'.symm.symm = b'.symm.symm
⊢ { repr := b : FreeGroupBasis ι G } = { repr := b' }

Tactic:
rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]

Premises used: FreeGroupBasis.ofRepr.injEq, MulEquiv.symm_symm