awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z x y : FreeAbelianGroup T
hx :
  (fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        x) =
    x
hy :
  (fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        y) =
    y
simp :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            x :
          ℤ)
        (of default) +
      HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            y :
          ℤ)
        (of default) =
    x + y
⊢ (fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        (x + y)) =
    x + y

Tactic:
simp only [map_add, add_smul] at *

Premises used: map_add, add_smul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z x y : FreeAbelianGroup T
hx :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          x :
        ℤ)
      (of default) =
    x
hy :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          y :
        ℤ)
      (of default) =
    y
rw :
  x +
      HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            y :
          ℤ)
        (of default) =
    x + y
rw₁ rw₂ : x + y = x + y
⊢ HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            x :
          ℤ)
        (of default) +
      HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            y :
          ℤ)
        (of default) =
    x + y

Tactic:
rw [hx, hy]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
n : ℤ
rw : HSMul.hSMul (β := ℤ) n 1 = n
⊢ (((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
        (a : FreeAbelianGroup T) → ℤ)
      ((fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default)) n) =
    n

Tactic:
rw [map_zsmul, lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of, map_zsmul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
n : ℤ
⊢ HSMul.hSMul (β := ℤ) n 1 = n

Tactic:
zsmul_one n

Premises used: zsmul_one
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
n : ℤ
⊢ HSMul.hSMul (β := ℤ) n 1 = n

Tactic:
exact zsmul_one n

Premises used: zsmul_one
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
rw :
  (map (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
rw₁ : (map id : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
rw₂ : (AddMonoidHom.id (FreeAbelianGroup α) : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
rw₃ rw₄ : x = x
⊢ (map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α)
      ((map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) =
    x

Tactic:
rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]

Premises used: Equiv.symm_comp_self, AddMonoidHom.id_apply, FreeAbelianGroup.map_id, FreeAbelianGroup.map_comp_apply
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
rw :
  (map (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := α) (⇑f : (a : α) → β) (⇑f.symm : (a : β) → α)) :
        (a : FreeAbelianGroup β) → FreeAbelianGroup β)
      x =
    x
rw₁ : (map id : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
rw₂ : (AddMonoidHom.id (FreeAbelianGroup β) : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
rw₃ rw₄ : x = x
⊢ (map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β)
      ((map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α) x) =
    x

Tactic:
rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]

Premises used: AddMonoidHom.id_apply, FreeAbelianGroup.map_id, Equiv.self_comp_symm, FreeAbelianGroup.map_comp_apply
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
⊢ Red L L

Tactic:
ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
⊢ Red L₁ L₂ → Red L₂ L₃ → Red L₁ L₃

Tactic:
ReflTransGen.trans

Premises used: Relation.ReflTransGen.trans, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
rw : L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length
⊢ (L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length

Tactic:
rw [List.length_append, List.length_append]

Premises used: List.length_append
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
false : Step (L₁ ++ (x, !Bool.false) :: (x, Bool.false) :: L₂) (L₁ ++ L₂)
true : Step (L₁ ++ (x, !Bool.true) :: (x, Bool.true) :: L₂) (L₁ ++ L₂)
⊢ Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

Tactic:
cases b
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)

Tactic:
Step.not

Premises used: FreeGroup.Red.Step.not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)

Tactic:
exact Step.not

Premises used: FreeGroup.Red.Step.not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)

Tactic:
Step.not

Premises used: FreeGroup.Red.Step.not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)

Tactic:
exact Step.not

Premises used: FreeGroup.Red.Step.not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
⊢ Step ((x, b) :: (x, !b) :: L) L

Tactic:
@Step.not _ [] _ _ _

Premises used: FreeGroup.Red.Step.not, List.append
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
⊢ Step ((x, !b) :: (x, b) :: L) L

Tactic:
@Red.Step.not_rev _ [] _ _ _

Premises used: FreeGroup.Red.Step.not_rev, List.append
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x L₁ L₂ : List (α × Bool)
x_1 : α
b : Bool
rw : Step (x ++ L₁ ++ (x_1, b) :: (x_1, !b) :: L₂) (x ++ L₁ ++ L₂)
⊢ Step (x ++ (L₁ ++ (x_1, b) :: (x_1, !b) :: L₂)) (x ++ (L₁ ++ L₂))

Tactic:
rw [← List.append_assoc, ← List.append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x L₁ L₂ : List (α × Bool)
x_1 : α
b : Bool
⊢ Step (x ++ L₁ ++ (x_1, b) :: (x_1, !b) :: L₂) (x ++ L₁ ++ L₂)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α × Bool
H : Step L₁ L₂
⊢ Step (x :: L₁) (x :: L₂)

Tactic:
@Step.append_left _ [x] _ _ H

Premises used: List.append, FreeGroup.Red.Step.append_left
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x L₁ L₂ : List (α × Bool)
x_1 : α
b : Bool
⊢ Step (L₁ ++ (x_1, b) :: (x_1, !b) :: L₂ ++ x) (L₁ ++ L₂ ++ x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
generalize : ∀ (L' : List (α × Bool)) (h' : [] = L'), ¬Step L' L
⊢ ¬Step [] L

Tactic:
generalize h' : [] = L'
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
h : Step L' L
rcases : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} (h' : [] = L₁ ++ (x, b) :: (x, !b) :: L₂), False
⊢ False

Tactic:
rcases h with - | ⟨L₁, L₂⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
h' : [] = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False

Tactic:
simp at h'
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
mp : Step ((a, b) :: L₁) L₂ → (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
mpr : (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
constructor
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
mp :
  ∀ (L : List (α × Bool)) (hL : (a, b) :: L₁ = L),
    Step L L₂ → (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
⊢ Step ((a, b) :: L₁) L₂ → (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
generalize hL : ((a, b) :: L₁ : List _) = L

Premises used: Prod.mk, List.cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a, b) :: L₁ = [] ++ (a', b') :: (a', !b') :: e
⊢ (∃ (L : List (α × Bool)), Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) :: L₁ = p :: s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ (L : List (α × Bool)), Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)

Tactic:
Step.cons h

Premises used: FreeGroup.Red.Step.cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)

Tactic:
exact Step.cons h

Premises used: FreeGroup.Red.Step.cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
Step.cons_not

Premises used: FreeGroup.Red.Step.cons_not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
exact Step.cons_not

Premises used: FreeGroup.Red.Step.cons_not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
a : α
b : Bool
⊢ ¬Step [(a, b)] L

Tactic:
simp [Step.cons_left_iff, not_step_nil]

Premises used: FreeGroup.Red.not_step_nil, FreeGroup.Red.Step.cons_left_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂

Tactic:
simp +contextual [Step.cons_left_iff, iff_def, or_imp]

Premises used: iff_def, or_imp, FreeGroup.Red.Step.cons_left_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ Step ([] ++ L₁) ([] ++ L₂) ↔ Step L₁ L₂

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
l : List (α × Bool)
⊢ Step (p :: l ++ L₁) (p :: l ++ L₂) ↔ Step L₁ L₂

Tactic:
simp [Step.append_left_iff l, Step.cons_cons_iff]

Premises used: FreeGroup.Red.Step.cons_cons_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
⊢ x_2 = x_4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x_4
⊢ x_3 = x_5

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x_4
snd_eq : x_3 = x_5
⊢ x = x_1

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x_4
snd_eq : x_3 = x_5
tail_eq : x = x_1
⊢ x_2 = x_4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x_4
snd_eq : x_3 = x_5
tail_eq : x = x_1
fst_eq₁ : x_2 = x_4
⊢ (!x_3) = !x_5

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
fst_eq : x_2 = x_4
snd_eq : x_3 = x_5
tail_eq : x = x_1
fst_eq_1 : x_2 = x_4
snd_eq_1 : (!x_3) = !x_5
subst_vars :
  x_4 = x_4 →
    (!x_5) = !x_5 → [] ++ x_1 = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x_1) L₅ ∧ Step ([] ++ x_1) L₅
⊢ [] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x_1) L₅

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x_1 : α
x_2 : Bool
fst_eq : x_1 = x_1
snd_eq : (!x_2) = !x_2
⊢ [] ++ x = [] ++ x ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x) L₅

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [(x3, b3)] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
⊢ x_2 = x3

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [(x3, b3)] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
⊢ x_3 = b3

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [(x3, b3)] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
snd_eq : x_3 = b3
⊢ x = (x_4, !x_5) :: x_1

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [(x3, b3)] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
snd_eq : x_3 = b3
tail_eq : x = (x_4, !x_5) :: x_1
⊢ x_2 = x_4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [(x3, b3)] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
snd_eq : x_3 = b3
tail_eq : x = (x_4, !x_5) :: x_1
fst_eq₁ : x_2 = x_4
⊢ (!x_3) = x_5

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
fst_eq : x_2 = x3
snd_eq : x_3 = b3
tail_eq : x = (x_4, !x_5) :: x_1
fst_eq_1 : x_2 = x_4
snd_eq_1 : (!x_3) = x_5
subst_vars :
  [] ++ (x_4, !!x_3) :: x_1 = [(x_4, x_3)] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ (x_4, !!x_3) :: x_1) L₅ ∧ Step ([(x_4, x_3)] ++ x_1) L₅
⊢ [] ++ x = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x_1 : Bool
x_2 : α
⊢ [] ++ (x_2, !!x_1) :: x = [(x_2, x_1)] ++ x ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ (x_2, !!x_1) :: x) L₅ ∧ Step ([(x_2, x_1)] ++ x) L₅

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [(x3, b3)] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
⊢ x3 = x_4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [(x3, b3)] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x3 = x_4
⊢ b3 = x_5

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [(x3, b3)] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x3 = x_4
snd_eq : b3 = x_5
⊢ (x_2, !x_3) :: x = x_1

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [(x3, b3)] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x3 = x_4
snd_eq : b3 = x_5
tail_eq : (x_2, !x_3) :: x = x_1
⊢ x_2 = x_4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [(x3, b3)] ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x3 = x_4
snd_eq : b3 = x_5
tail_eq : (x_2, !x_3) :: x = x_1
fst_eq₁ : x_2 = x_4
⊢ x_3 = !x_5

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
fst_eq : x3 = x_4
snd_eq : b3 = x_5
tail_eq : (x_2, !x_3) :: x = x_1
fst_eq_1 : x_2 = x_4
snd_eq_1 : x_3 = !x_5
subst_vars :
  [(x_4, x_5)] ++ x = [] ++ (x_4, !!x_5) :: x ∨
    ∃ (L₅ : List (α × Bool)), Step ([(x_4, x_5)] ++ x) L₅ ∧ Step ([] ++ (x_4, !!x_5) :: x) L₅
⊢ [(x3, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x_1 : α
x_2 : Bool
⊢ [(x_1, x_2)] ++ x = [] ++ (x_1, !!x_2) :: x ∨
    ∃ (L₅ : List (α × Bool)), Step ([(x_1, x_2)] ++ x) L₅ ∧ Step ([] ++ (x_1, !!x_2) :: x) L₅

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
⊢ x_2 = x3

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
⊢ x_3 = b3

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
snd_eq : x_3 = b3
⊢ x = tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1)

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
snd_eq : x_3 = b3
tail_eq : x = tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1)
⊢ x_2 = x4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : [] ++ (x_2, x_3) :: (x_2, !x_3) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
fst_eq : x_2 = x3
snd_eq : x_3 = b3
tail_eq : x = tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1)
fst_eq₁ : x_2 = x4
⊢ (!x_3) = b4

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
fst_eq : x_2 = x3
snd_eq : x_3 = b3
tail_eq : x = tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1)
fst_eq_1 : x_2 = x4
snd_eq_1 : (!x_3) = b4
subst_vars :
  [] ++ tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1) = (x_2, x_3) :: (x_2, !x_3) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)),
      Step ([] ++ tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1)) L₅ ∧ Step ((x_2, x_3) :: (x_2, !x_3) :: tl ++ x_1) L₅
⊢ [] ++ x = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
tl x : List (α × Bool)
x_1 : α
x_2 : Bool
x_3 : α
x_4 : Bool
h :
  ∃ (L₅ : List (α × Bool)),
    Step ([] ++ tl.append ((x_3, x_4) :: (x_3, !x_4) :: x)) L₅ ∧ Step ((x_1, x_2) :: (x_1, !x_2) :: tl ++ x) L₅
⊢ [] ++ tl.append ((x_3, x_4) :: (x_3, !x_4) :: x) = (x_1, x_2) :: (x_1, !x_2) :: tl ++ x ∨
    ∃ (L₅ : List (α × Bool)),
      Step ([] ++ tl.append ((x_3, x_4) :: (x_3, !x_4) :: x)) L₅ ∧ Step ((x_1, x_2) :: (x_1, !x_2) :: tl ++ x) L₅

Tactic:
right
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
tl x : List (α × Bool)
x_1 : α
x_2 : Bool
x_3 : α
x_4 : Bool
⊢ ∃ (L₅ : List (α × Bool)),
    Step ([] ++ tl.append ((x_3, x_4) :: (x_3, !x_4) :: x)) L₅ ∧ Step ((x_1, x_2) :: (x_1, !x_2) :: tl ++ x) L₅

Tactic:
⟨_, Red.Step.not, Red.Step.cons_not⟩

Premises used: FreeGroup.Red.Step.cons_not, FreeGroup.Red.Step.not, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
tl x : List (α × Bool)
x_1 : α
x_2 : Bool
x_3 : α
x_4 : Bool
⊢ ∃ (L₅ : List (α × Bool)),
    Step ([] ++ tl.append ((x_3, x_4) :: (x_3, !x_4) :: x)) L₅ ∧ Step ((x_1, x_2) :: (x_1, !x_2) :: tl ++ x) L₅

Tactic:
exact ⟨_, Red.Step.not, Red.Step.cons_not⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x x_1 : List (α × Bool)
x_2 : α
x_3 : Bool
x_4 : α
x_5 : Bool
H : (x3, b3) :: (x4, b4) :: tl ++ (x_2, x_3) :: (x_2, !x_3) :: x = [] ++ (x_4, x_5) :: (x_4, !x_5) :: x_1
⊢ x3 = x_4

Tactic:
injections