-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem cons_cons_iff (p) : Red (p :: L₁) (p :: L₂) ↔ Red L₁ L₂ :=
  Iff.intro
    (by
      generalize eq₁ : (p :: L₁ : List _) = LL₁
      generalize eq₂ : (p :: L₂ : List _) = LL₂
      intro h
      induction' h using Relation.ReflTransGen.head_induction_on
        with L₁ L₂ h₁₂ h ih
        generalizing L₁ L₂
      · subst_vars
        cases eq₂
        constructor
      · 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)
    cons_cons

Proof state:
case head.mk
α : Type u
LL₁ L₂✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) L₂✝
⊢ Red L₁ L₂

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

Result:
case head.mk
α : Type u
LL₁ L₂✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : (∃ L, Step L₁ L ∧ L₂✝ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂✝
⊢ Red L₁ L₂

Proof state:
case head.mk.inl.intro.intro
α : 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)}, (a, b) :: L₁ = (a, b) :: L → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red L₁ L₂

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

Result:
no goals

Proof state:
case head.mk
α : Type u
LL₁ L₂✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : (∃ L, Step L₁ L ∧ L₂✝ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂✝
⊢ Red L₁ L₂

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

Result:
case head.mk.inl.intro.intro
α : 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)}, (a, b) :: L₁ = (a, b) :: L → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red L₁ L₂

case head.mk.inr
α : Type u
LL₁ L₂✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: L₂✝) L₂

Proof state:
case head
α : Type u
p : α × Bool
LL₁ LL₂ L₁✝ L₂✝ : List (α × Bool)
h₁₂ : Step L₁✝ L₂✝
h : ReflTransGen Step L₂✝ LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = LL₂ → Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = L₁✝
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

Tactic:
subst_vars

Result:
case head
α : Type u
p : α × Bool
LL₁ L₂✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step L₂✝ (p :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂_1 = p :: L₂ → Red L₁ L₂_1
h₁₂ : Step (p :: L₁) L₂✝
⊢ Red L₁ L₂

Proof state:
case head.mk.inr
α : Type u
LL₁ L₂✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: L₂✝) L₂

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

Result:
no goals

Proof state:
case refl
α : Type u
p : α × Bool
LL₁ L₁ L₂ : List (α × Bool)
eq₂ : p :: L₂ = p :: L₁
⊢ Red L₁ L₂

Tactic:
cases eq₂

Result:
case refl.refl
α : Type u
p : α × Bool
LL₁ L₁ : List (α × Bool)
⊢ Red L₁ L₁

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
⊢ Red LL₁ LL₂ → Red L₁ L₂

Tactic:
intro h

Result:
α : 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₂
⊢ Red L₁ L₂

Proof state:
α : 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₂
⊢ Red L₁ L₂

Tactic:
induction' h using Relation.ReflTransGen.head_induction_on
  with L₁ L₂ h₁₂ h ih
  generalizing L₁ L₂

Result:
case refl
α : Type u
p : α × Bool
LL₁ LL₂ L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

case head
α : Type u
p : α × Bool
LL₁ LL₂ L₁✝ L₂✝ : List (α × Bool)
h₁₂ : Step L₁✝ L₂✝
h : ReflTransGen Step L₂✝ LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = LL₂ → Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = L₁✝
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
⊢ Red (p :: L₁) (p :: L₂) → Red L₁ L₂

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

Result:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂

Proof state:
case head
α : Type u
p : α × Bool
LL₁ L₂✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step L₂✝ (p :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂_1 = p :: L₂ → Red L₁ L₂_1
h₁₂ : Step (p :: L₁) L₂✝
⊢ Red L₁ L₂

Tactic:
obtain ⟨a, b⟩ := p

Result:
case head.mk
α : Type u
LL₁ L₂✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) L₂✝
⊢ Red L₁ L₂

Proof state:
case refl
α : Type u
p : α × Bool
LL₁ LL₂ L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

Tactic:
subst_vars

Result:
case refl
α : Type u
p : α × Bool
LL₁ L₁ L₂ : List (α × Bool)
eq₂ : p :: L₂ = p :: L₁
⊢ Red L₁ L₂

Proof state:
case refl.refl
α : Type u
p : α × Bool
LL₁ L₁ : List (α × Bool)
⊢ Red L₁ L₁

Tactic:
constructor

Result:
no goals

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂

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

Result:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
⊢ Red LL₁ LL₂ → Red L₁ L₂