Theorem: FreeGroup.exists_of_step (Lectures/WordProblem/FreeGroup.lean)

State before:
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
⊢ Step L L' → ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
Tactic:
intro step
State after:
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
step : Step L L'
⊢ ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂

State before:
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
step : Step L L'
⊢ ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
Tactic:
induction step with
| @not L₁ L₂ x b =>  use x, b, L₁, L₂
State after:
no goals

State before:
case not
α : Type
inst✝ : DecidableEq α
L L' L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ ∃ x_1 b_1 L₁_1 L₂_1,
    L₁ ++ (x, b) :: (x, !b) :: L₂ = L₁_1 ++ (x_1, b_1) :: (x_1, !b_1) :: L₂_1 ∧ L₁ ++ L₂ = L₁_1 ++ L₂_1
Tactic:
use x, b, L₁, L₂
State after:
no goals