awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
fst_eq : x3 = x_4
⊢ b3 = x_5

Tactic:
injections
-- 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
fst_eq : x3 = x_4
snd_eq : b3 = x_5
⊢ tl.append ((x_2, x_3) :: (x_2, !x_3) :: x) = x_1

Tactic:
injections
-- 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
fst_eq : x3 = x_4
snd_eq : b3 = x_5
tail_eq : tl.append ((x_2, x_3) :: (x_2, !x_3) :: x) = x_1
⊢ x4 = x_4

Tactic:
injections
-- 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
fst_eq : x3 = x_4
snd_eq : b3 = x_5
tail_eq : tl.append ((x_2, x_3) :: (x_2, !x_3) :: x) = x_1
fst_eq₁ : x4 = x_4
⊢ b4 = !x_5

Tactic:
injections
-- 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
fst_eq : x3 = x_4
snd_eq : b3 = x_5
tail_eq : tl.append ((x_2, x_3) :: (x_2, !x_3) :: x) = x_1
fst_eq_1 : x4 = x_4
snd_eq_1 : b4 = !x_5
subst_vars :
  (x_4, x_5) :: (x_4, !x_5) :: tl ++ x = [] ++ tl.append ((x_2, x_3) :: (x_2, !x_3) :: x) ∨
    ∃ (L₅ : List (α × Bool)),
      Step ((x_4, x_5) :: (x_4, !x_5) :: tl ++ x) L₅ ∧ Step ([] ++ tl.append ((x_2, x_3) :: (x_2, !x_3) :: x)) L₅
⊢ (x3, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ 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 ((x_3, x_4) :: (x_3, !x_4) :: tl ++ x) L₅ ∧ Step ([] ++ tl.append ((x_1, x_2) :: (x_1, !x_2) :: x)) L₅
⊢ (x_3, x_4) :: (x_3, !x_4) :: tl ++ x = [] ++ tl.append ((x_1, x_2) :: (x_1, !x_2) :: x) ∨
    ∃ (L₅ : List (α × Bool)),
      Step ((x_3, x_4) :: (x_3, !x_4) :: tl ++ x) L₅ ∧ Step ([] ++ tl.append ((x_1, x_2) :: (x_1, !x_2) :: 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 ((x_3, x_4) :: (x_3, !x_4) :: tl ++ x) L₅ ∧ Step ([] ++ tl.append ((x_1, x_2) :: (x_1, !x_2) :: x)) L₅

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

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

Tactic:
simpa [H1] using Step.cons H4

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

Tactic:
ReflTransGen.single

Premises used: Relation.ReflTransGen.single, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ L₃ x b_1 c b : List (α × Bool)
hab hac : Step x b
⊢ ReflGen Step b b

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ L₃ x b_1 c b : List (α × Bool)
hab hac : Step x b
⊢ ReflTransGen Step b b

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
⊢ Red L₁ L₂ → Red (p :: L₁) (p :: L₂)

Tactic:
ReflTransGen.lift (List.cons p) fun _ _ => Step.cons

Premises used: Relation.ReflTransGen.lift, List.cons, FreeGroup.Red.Step.cons, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
generalize : ∀ (LL₁ : List (α × Bool)) (eq₁ : p :: L₁ = LL₁), Red LL₁ (p :: L₂) → Red L₁ L₂
⊢ Red (p :: L₁) (p :: L₂) → Red L₁ L₂

Tactic:
generalize eq₁ : (p :: L₁ : List _) = LL₁

Premises used: List.cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
generalize : ∀ (LL₂ : List (α × Bool)) (eq₂ : p :: L₂ = LL₂), Red LL₁ LL₂ → Red L₁ L₂
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂

Tactic:
generalize eq₂ : (p :: L₂ : List _) = LL₂

Premises used: List.cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ LL₂ L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ p :: L₂ = p :: L₁

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ L₁ L₂ : List (α × Bool)
eq₂ : p :: L₂ = p :: L₁
refl : Red L₁ L₁
⊢ Red L₁ L₂

Tactic:
cases eq₂
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ L₁ : List (α × Bool)
⊢ Red L₁ L₁

Tactic:
constructor
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ LL₂ a c : List (α × Bool)
h₁₂ : Step a c
h : ReflTransGen Step c LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = a
eq₂ : p :: L₂ = LL₂
⊢ ReflTransGen Step c (p :: L₂)

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ LL₂ a c : List (α × Bool)
h₁₂ : Step a c
h : ReflTransGen Step c LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = a
eq₂ : p :: L₂ = LL₂
h₁ : ReflTransGen Step c (p :: L₂)
⊢ ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂_1 = p :: L₂), Red L₁ L₂_1

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ LL₂ a c : List (α × Bool)
h₁₂ : Step a c
h : ReflTransGen Step c LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = a
eq₂ : p :: L₂ = LL₂
h₁ : ReflTransGen Step c (p :: L₂)
ih₁ : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂_1 = p :: L₂), Red L₁ L₂_1
⊢ Step (p :: L₁) c

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
p : α × Bool
LL₁ c L₁ L₂ : List (α × Bool)
h : ReflTransGen Step c (p :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂_1 = p :: L₂), Red L₁ L₂_1
h₁₂ : Step (p :: L₁) c
head :
  ∀ (a : α) (b : Bool) (h : ReflTransGen Step c ((a, b) :: L₂))
    (ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = c) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1)
    (h₁₂ : Step ((a, b) :: L₁) c), Red L₁ L₂
⊢ Red L₁ L₂

Tactic:
obtain ⟨a, b⟩ := p
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
LL₁ c L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = c) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) c
⊢ (∃ (L : List (α × Bool)), Step L₁ L ∧ c = (a, b) :: L) ∨ L₁ = (a, !b) :: c

Tactic:
rw [Step.cons_left_iff] at h₁₂

Premises used: FreeGroup.Red.Step.cons_left_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
LL₁ c L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = c) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
h₁₂ : (∃ (L : List (α × Bool)), Step L₁ L ∧ c = (a, b) :: L) ∨ L₁ = (a, !b) :: c
head :
  ∀ (L : List (α × Bool)) (h₁₂ : Step L₁ L) (h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂))
    (ih :
      ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = (a, b) :: L) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂),
        Red L₁ L₂_1),
    Red L₁ L₂
head₁ : Red ((a, !b) :: c) L₂
⊢ Red L₁ L₂

Tactic:
rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
LL₁ L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h₁₂ : Step L₁ L
h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = (a, b) :: L) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
⊢ Red L₁ L₂

Tactic:
(ih rfl rfl).head h₁₂

Premises used: Relation.ReflTransGen.head, rfl, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
LL₁ L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h₁₂ : Step L₁ L
h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = (a, b) :: L) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
⊢ Red L₁ L₂

Tactic:
exact (ih rfl rfl).head h₁₂

Premises used: Relation.ReflTransGen.head, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
LL₁ c L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = c) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
⊢ Red ((a, !b) :: c) L₂

Tactic:
(cons_cons h).tail Step.cons_not_rev

Premises used: FreeGroup.Red.cons_cons, FreeGroup.Red.Step.cons_not_rev, Relation.ReflTransGen.tail, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
LL₁ c L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = c) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
⊢ Red ((a, !b) :: c) L₂

Tactic:
exact (cons_cons h).tail Step.cons_not_rev

Premises used: FreeGroup.Red.cons_cons, FreeGroup.Red.Step.cons_not_rev, Relation.ReflTransGen.tail
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
refl : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = LL₂) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
head :
  ∀ {a c : List (α × Bool)} (h₁₂ : Step a c) (h : ReflTransGen Step c LL₂)
    (ih : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂) {L₁ L₂ : List (α × Bool)}
    (eq₁ : p :: L₁ = a) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
⊢ Red L₁ L₂

Tactic:
induction h using Relation.ReflTransGen.head_induction_on generalizing L₁ L₂ with
      | refl =>
        subst_vars
        cases eq₂
        constructor
      | head h₁₂ h ih =>
        subst_vars
        obtain ⟨a, b⟩ := p
        rw [Step.cons_left_iff] at h₁₂
        rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
        · exact (ih rfl rfl).head h₁₂
        · exact (cons_cons h).tail Step.cons_not_rev

Premises used: FreeGroup.Red.cons_cons, FreeGroup.Red.refl, Relation.ReflTransGen.tail, FreeGroup.Red.Step.cons_left_iff, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
L : List (α × Bool)
⊢ Red (p :: L ++ L₁) (p :: L ++ L₂) ↔ Red L₁ L₂

Tactic:
simp [append_append_left_iff L, cons_cons_iff]

Premises used: FreeGroup.Red.cons_cons_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ L₃ L₄ : List (α × Bool)
h₁ : Red L₁ L₃
h₂ : Red L₂ L₄
⊢ Red (L₁ ++ L₂) (L₃ ++ L₄)

Tactic:
(h₁.lift (fun L => L ++ L₂) fun _ _ => Step.append_right).trans ((append_append_left_iff _).2 h₂)

Premises used: Iff.mpr, Relation.ReflTransGen.lift, Relation.ReflTransGen.trans, FreeGroup.Red.append_append_left_iff, FreeGroup.Red.Step.append_right, HAppend.hAppend, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ : List (α × Bool)
generalize :
  ∀ (L₁₂ : List (α × Bool)) (eq : L₁ ++ L₂ = L₁₂),
    Red L L₁₂ → ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
⊢ Red L (L₁ ++ L₂) → ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
generalize eq : L₁ ++ L₂ = L₁₂
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₁ L₁

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₂ L₂

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
exact ⟨_, _, eq.symm, by rfl, by rfl⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ b c : List (α × Bool)
hLL' : ReflTransGen Step L b
h : Step b c
ih :
  ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = b),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = c
tail :
  ∀ {s e : List (α × Bool)} {a : α} {b : Bool} (hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e))
    (ih :
      ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂)
    (eq : L₁ ++ L₂ = s ++ e), ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
obtain @⟨s, e, a, b⟩ := h
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
tail :
  ∀ (s' : List (α × Bool)) (hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e))
    (ih :
      ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂)
    (eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
tail₁ :
  ∀ (e' : List (α × Bool)) (hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂)))
    (ih :
      ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1)
    (eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)

Premises used: Iff.mp, rfl, List.append_eq_append_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e

Tactic:
have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) =
            L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
tail :
  ∀ (w₁ w₂ : List (α × Bool)) (hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e))
    (ih :
      ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂)
    (h₁ : Red w₁ L₁) (h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
h₁ : Red w₁ L₁
h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩

Premises used: FreeGroup.Red.Step.not, And.intro, Relation.ReflTransGen.tail, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
h₁ : Red w₁ L₁
h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)

Tactic:
have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ =
            s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
tail :
  ∀ (w₁ w₂ : List (α × Bool)) (hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂)))
    (ih :
      ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1)
    (h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')) (h₂ : Red w₂ L₂),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')
h₂ : Red w₂ L₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩

Premises used: FreeGroup.Red.Step.not, And.intro, Relation.ReflTransGen.tail, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')
h₂ : Red w₂ L₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩