-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.cons_left_iff {a : α} {b : Bool} :
    Step ((a, b) :: L₁) L₂ ↔ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, ! b) :: L₂

Proof state:
case mp.not.cons.intro
α : Type u
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
s' : List (α × Bool)
⊢ (∃ L, Step (s' ++ (a', b') :: (a', !b') :: e) L ∧ (a, b) :: s' ++ e = (a, b) :: L) ∨
    s' ++ (a', b') :: (a', !b') :: e = (a, !b) :: ((a, b) :: s' ++ e)

Tactic:
refine Or.inl ⟨s' ++ e, Step.not, ?_⟩

Result:
case mp.not.cons.intro
α : Type u
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
s' : List (α × Bool)
⊢ (a, b) :: s' ++ e = (a, b) :: (s' ++ e)

Proof state:
case mp.not.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a, b) :: L₁ = [] ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

Tactic:
simp at hL

Result:
case mp.not.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a = a' ∧ b = b') ∧ L₁ = (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

Proof state:
case mp.not.cons.intro
α : Type u
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
s' : List (α × Bool)
⊢ (a, b) :: s' ++ e = (a, b) :: (s' ++ e)

Tactic:
simp

Result:
no goals

Proof state:
case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
exact Step.cons_not

Result:
no goals

Proof state:
case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂

Tactic:
rintro (⟨L, h, rfl⟩ | rfl)

Result:
case mpr.inl.intro.intro
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)

case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Proof state:
case mp.not.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a = a' ∧ b = b') ∧ L₁ = (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

Tactic:
simp [*]

Result:
no goals

Proof state:
case mp.not.cons
α : 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, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)

Tactic:
simp at hL

Result:
case mp.not.cons
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) = p ∧ L₁ = s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)

Proof state:
case mpr.inl.intro.intro
α : 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

Result:
no goals

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
constructor

Result:
case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂

Proof state:
case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

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

Result:
case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
hL : (a, b) :: L₁ = L
⊢ Step L L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Proof state:
case mp.not.cons
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) = p ∧ L₁ = s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)

Tactic:
rcases hL with ⟨rfl, rfl⟩

Result:
case mp.not.cons.intro
α : Type u
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
s' : List (α × Bool)
⊢ (∃ L, Step (s' ++ (a', b') :: (a', !b') :: e) L ∧ (a, b) :: s' ++ e = (a, b) :: L) ∨
    s' ++ (a', b') :: (a', !b') :: e = (a, !b) :: ((a, b) :: s' ++ e)

Proof state:
case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
hL : (a, b) :: L₁ = L
⊢ Step L L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
rintro @⟨_ | ⟨p, s'⟩, e, a', b'⟩

Result:
case mp.not.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a, b) :: L₁ = [] ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

case mp.not.cons
α : 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, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)