-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem reduce.not {p : Prop} :
    ∀ {L₁ L₂ L₃ : List (α × Bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p
  | [], L2, L3, _, _ => fun h => by cases L2 <;> injections
  | (x, b) :: L1, L2, L3, x', b' => by
    dsimp
    cases r : reduce L1 with
    | nil =>
      dsimp; intro h
      exfalso
      have := congr_arg List.length h
      simp? [List.length] at this says
        simp only [List.length, zero_add, List.length_append] at this
      omega
    | cons hd tail =>
      obtain ⟨y, c⟩ := hd
      dsimp only
      split_ifs with h <;> intro H
      · rw [H] at r
        exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
      rcases L2 with (_ | ⟨a, L2⟩)
      · injections; subst_vars
        simp at h
      · refine @reduce.not _ L1 L2 L3 x' b' ?_
        injection H with _ H
        rw [r, H]; rfl

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
this : [(x, b)].length = (L2 ++ (x', b') :: (x', !b') :: L3).length
⊢ False

Tactic:
simp? [List.length] at this says
  simp only [List.length, zero_add, List.length_append] at this

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
this : 1 = L2.length + (L3.length + 1 + 1)
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L2 L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = L2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

Tactic:
cases L2 <;> injections

Result:
no goals

Proof state:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2.append ((x', b') :: (x', !b') :: L3)
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
rw [r, H]

Result:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2.append ((x', b') :: (x', !b') :: L3)
⊢ L2.append ((x', b') :: (x', !b') :: L3) = L2 ++ (x', b') :: (x', !b') :: L3

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
exfalso

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
⊢ False

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
this : [(x, b)].length = (L2 ++ (x', b') :: (x', !b') :: L3).length
⊢ False

Tactic:
simp only [List.length, zero_add, List.length_append] at this

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
this : 1 = L2.length + (L3.length + 1 + 1)
⊢ False

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
⊢ List.rec [(x, b)] (fun head tail tail_ih => if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail) [] =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
dsimp

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
⊢ [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3 → p

Proof state:
case neg.nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
fst_eq✝¹ : x = x'
snd_eq✝¹ : b = b'
tail_eq✝ : tail = L3
fst_eq✝ : y = x'
snd_eq✝ : c = !b'
⊢ p

Tactic:
subst_vars

Result:
case neg.nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L1 : List (α × Bool)
b' : Bool
tail : List (α × Bool)
y : α
r : reduce L1 = (y, !b') :: tail
h : ¬(y = y ∧ b' = !!b')
⊢ p

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
⊢ reduce ((x, b) :: L1) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
dsimp

Result:
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
⊢ List.rec [(x, b)] (fun head tail tail_ih => if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        (reduce L1) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Proof state:
case cons.mk
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
⊢ (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
split_ifs with h <;> intro H

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

case neg
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p