awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
have false : Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
false : Step (L₁ ++ (x, !Bool.false) :: (x, Bool.false) :: L₂) (L₁ ++ L₂)
⊢ Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
have true : Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂))
have rw : Step (x ++ L₁ ++ (x_1, b) :: (x_1, !b) :: L₂) (x ++ L₁ ++ L₂)
Tactic: rw [← List.append_assoc, ← List.append_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L : List (α × Bool)
⊢ ¬Step [] L
have generalize : ∀ (L' : List (α × Bool)) (h' : [] = L'), ¬Step L' L
Tactic: generalize h' : [] = L'
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False
have rcases : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} (h' : [] = L₁ ++ (x, b) :: (x, !b) :: L₂), False
Tactic: rcases h with - | ⟨L₁, L₂⟩
Cleared hypotheses: L, L', h', h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
have mp : Step ((a, b) :: L₁) L₂ → (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
have mpr : (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ → (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
have 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₂
Tactic: generalize hL : ((a, b) :: L₁ : List _) = L
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have fst_eq : x_2 = x_4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have snd_eq : x_3 = x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have tail_eq : x = x_1
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have snd_eq₁ : (!x_3) = !x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ [] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have 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₅
Tactic: subst_vars
Cleared hypotheses: x, x_2, x_3, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅
have fst_eq : x_2 = x3
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅
have snd_eq : x_3 = b3
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅
have tail_eq : x = (x_4, !x_5) :: x_1
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅
have fst_eq₁ : x_2 = x_4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅
have snd_eq₁ : (!x_3) = x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ [] ++ x = [(x3, b3)] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ([(x3, b3)] ++ x_1) L₅
have 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₅
Tactic: subst_vars
Cleared hypotheses: x, x3, b3, x_2, x_5, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have fst_eq : x3 = x_4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ [(x3, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have snd_eq : b3 = x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ [(x3, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have tail_eq : (x_2, !x_3) :: x = x_1
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ [(x3, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have fst_eq₁ : x_2 = x_4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ [(x3, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have snd_eq₁ : x_3 = !x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ [(x3, b3)] ++ x = [] ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), Step ([(x3, b3)] ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have 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₅
Tactic: subst_vars
Cleared hypotheses: x3, b3, x_1, x_2, x_3, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅
have fst_eq : x_2 = x3
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅
have snd_eq : x_3 = b3
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅
have tail_eq : x = tl.append ((x_4, x_5) :: (x_4, !x_5) :: x_1)
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅
have fst_eq₁ : x_2 = x4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅
have snd_eq₁ : (!x_3) = b4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ [] ++ x = (x3, b3) :: (x4, b4) :: tl ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ([] ++ x) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x_1) L₅
have 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₅
Tactic: subst_vars
Cleared hypotheses: x, x3, b3, x4, b4, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
tl x : List (α × Bool)
x_1 : α
x_2 : Bool
x_3 : α
x_4 : Bool
⊢ [] ++ 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₅
have 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₅
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have fst_eq : x3 = x_4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ (x3, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have snd_eq : b3 = x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ (x3, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have tail_eq : tl.append ((x_2, x_3) :: (x_2, !x_3) :: x) = x_1
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ (x3, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have fst_eq₁ : x4 = x_4
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ (x3, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have snd_eq₁ : b4 = !x_5
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ (x3, b3) :: (x4, b4) :: tl ++ x = [] ++ x_1 ∨
    ∃ (L₅ : List (α × Bool)), Step ((x3, b3) :: (x4, b4) :: tl ++ x) L₅ ∧ Step ([] ++ x_1) L₅
have 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₅
Tactic: subst_vars
Cleared hypotheses: x3, b3, x4, b4, x_1, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
tl x : List (α × Bool)
x_1 : α
x_2 : Bool
x_3 : α
x_4 : Bool
⊢ (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₅
have 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₅
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
⊢ Red (p :: L₁) (p :: L₂) → Red L₁ L₂
have generalize : ∀ (LL₁ : List (α × Bool)) (eq₁ : p :: L₁ = LL₁), Red LL₁ (p :: L₂) → Red L₁ L₂
Tactic: generalize eq₁ : (p :: L₁ : List _) = LL₁
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂
have generalize : ∀ (LL₂ : List (α × Bool)) (eq₂ : p :: L₂ = LL₂), Red LL₁ LL₂ → Red L₁ L₂
Tactic: generalize eq₂ : (p :: L₂ : List _) = LL₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
Goal:
α : Type u
p : α × Bool
LL₁ LL₂ L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂
have eq₃ : p :: L₂ = p :: L₁
Tactic: subst_vars
Cleared hypotheses: LL₂, eq₁, eq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
p : α × Bool
LL₁ L₁ L₂ : List (α × Bool)
eq₂ : p :: L₂ = p :: L₁
⊢ Red L₁ L₂
have refl : Red L₁ L₁
Tactic: cases eq₂
Cleared hypotheses: L₂, eq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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₂
⊢ Red L₁ L₂
have h₁ : ReflTransGen Step c (p :: L₂)
Tactic: subst_vars
Cleared hypotheses: LL₂, a, h₁₂, h, ih, eq₁, eq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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₂)
⊢ Red L₁ L₂
have ih₁ : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂_1 = p :: L₂), Red L₁ L₂_1
Tactic: subst_vars
Cleared hypotheses: LL₂, a, h₁₂, h, ih, eq₁, eq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ Red L₁ L₂
have h₁₃ : Step (p :: L₁) c
Tactic: subst_vars
Cleared hypotheses: LL₂, a, h₁₂, h, ih, eq₁, eq₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ Red L₁ L₂
have 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₂
Tactic: obtain ⟨a, b⟩ := p
Cleared hypotheses: p, h, ih, h₁₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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
⊢ Red L₁ L₂
have h₁₃ : (∃ (L : List (α × Bool)), Step L₁ L ∧ c = (a, b) :: L) ∨ L₁ = (a, !b) :: c
Tactic: rw [Step.cons_left_iff] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ Red L₁ L₂
have 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₂
Tactic: rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
Cleared hypotheses: c, h, ih, h₁₂