[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ List.length (L1 ++ L2) + 2 = List.length (L1 ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
rw [List.length_append, List.length_append]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ List.length L1 + List.length L2 + 2 = List.length L1 + List.length ((x, b) :: (x, !b) :: L2)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
⊢ Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)
[PROOFSTEP]
exact Step.not
[GOAL]
case true
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)
[PROOFSTEP]
exact Step.not
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (x✝¹ ++ (L₁✝ ++ L₂✝))
[PROOFSTEP]
rw [← List.append_assoc, ← List.append_assoc]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)
[PROOFSTEP]
constructor
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝ ++ x✝¹) (L₁✝ ++ L₂✝ ++ x✝¹)
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ¬Step [] L
[PROOFSTEP]
generalize h' : [] = L'
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L' : List (α × Bool)
h' : [] = L'
⊢ ¬Step L' L
[PROOFSTEP]
intro h
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False
[PROOFSTEP]
cases' h with L₁ L₂
[GOAL]
case not
α : Type u
L₁✝ L₂✝ L₃ L₄ L₁ L₂ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂
⊢ False
[PROOFSTEP]
simp [List.nil_eq_append] at h' 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
[PROOFSTEP]
generalize hL : ((a, b) :: L₁ : List _) = L
[GOAL]
case mp
α : Type u
L✝ L₁ L₂ 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₂
[PROOFSTEP]
rintro @⟨_ | ⟨p, s'⟩, e, a', b'⟩
[GOAL]
case mp.not.nil
α : Type u
L L₁ L₃ 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)
[PROOFSTEP]
simp at hL 
[GOAL]
case mp.not.nil
α : Type u
L L₁ L₃ 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)
[PROOFSTEP]
simp [*]
[GOAL]
case mp.not.cons
α : Type u
L L₁ L₃ 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)
[PROOFSTEP]
simp at hL 
[GOAL]
case mp.not.cons
α : Type u
L L₁ L₃ 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)
[PROOFSTEP]
rcases hL with ⟨rfl, rfl⟩
[GOAL]
case mp.not.cons.intro
α : Type u
L L₃ L₄ : List (α × Bool)
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)
[PROOFSTEP]
refine' Or.inl ⟨s' ++ e, Step.not, _⟩
[GOAL]
case mp.not.cons.intro
α : Type u
L L₃ L₄ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
s' : List (α × Bool)
⊢ (a, b) :: s' ++ e = (a, b) :: (s' ++ e)
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂
[PROOFSTEP]
rintro (⟨L, h, rfl⟩ | rfl)
[GOAL]
case mpr.inl.intro.intro
α : Type u
L✝ L₁ L₃ L₄ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)
[PROOFSTEP]
exact Step.cons h
[GOAL]
case mpr.inr
α : Type u
L L₂ L₃ L₄ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂
[PROOFSTEP]
exact Step.cons_not
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
a : α
b : Bool
⊢ ¬Step [(a, b)] L
[PROOFSTEP]
simp [Step.cons_left_iff, not_step_nil]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂
[PROOFSTEP]
simp (config := { contextual := true }) [Step.cons_left_iff, iff_def, or_imp]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Step ([] ++ L₁) ([] ++ L₂) ↔ Step L₁ L₂
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
l : List (α × Bool)
⊢ Step (p :: l ++ L₁) (p :: l ++ L₂) ↔ Step L₁ L₂
[PROOFSTEP]
simp [Step.append_left_iff l, Step.cons_cons_iff]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
[PROOFSTEP]
injections
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x✝¹
snd_eq✝¹ : x✝² = x✝
tail_eq✝ : x✝⁵ = x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : (!x✝²) = !x✝
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝² : List (α × Bool)
x✝¹ : α
x✝ : Bool
fst_eq✝ : x✝¹ = x✝¹
snd_eq✝ : (!x✝) = !x✝
⊢ [] ++ x✝² = [] ++ x✝² ∨ ∃ L₅, Step ([] ++ x✝²) L₅ ∧ Step ([] ++ x✝²) L₅
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [(x3, b3)] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅
[PROOFSTEP]
injections
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x3
snd_eq✝¹ : x✝² = b3
tail_eq✝ : x✝⁵ = (x✝¹, !x✝) :: x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : (!x✝²) = x✝
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝² : List (α × Bool)
x✝¹ : Bool
x✝ : α
⊢ [] ++ (x✝, !!x✝¹) :: x✝² = [(x✝, x✝¹)] ++ x✝² ∨
    ∃ L₅, Step ([] ++ (x✝, !!x✝¹) :: x✝²) L₅ ∧ Step ([(x✝, x✝¹)] ++ x✝²) L₅
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [(x3, b3)] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
[PROOFSTEP]
injections
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x3 = x✝¹
snd_eq✝¹ : b3 = x✝
tail_eq✝ : (x✝³, !x✝²) :: x✝⁵ = x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : x✝² = !x✝
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝² : List (α × Bool)
x✝¹ : α
x✝ : Bool
⊢ [(x✝¹, x✝)] ++ x✝² = [] ++ (x✝¹, !!x✝) :: x✝² ∨
    ∃ L₅, Step ([(x✝¹, x✝)] ++ x✝²) L₅ ∧ Step ([] ++ (x✝¹, !!x✝) :: x✝²) L₅
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁴) L₅
[PROOFSTEP]
injections
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x3
snd_eq✝¹ : x✝² = b3
tail_eq✝ : x✝⁵ = List.append tl ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
fst_eq✝ : x✝³ = x4
snd_eq✝ : (!x✝²) = b4
⊢ [] ++ x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁴) L₅
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ [] ++ List.append tl ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴) = (x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴ ∨
    ∃ L₅,
      Step ([] ++ List.append tl ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴) L₅
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ tl ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴ = (x✝³, x✝²) :: (x✝³, !x✝²) :: (tl ++ x✝⁴) ∨
    ∃ L₅, Step (tl ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: (tl ++ x✝⁴)) L₅
[PROOFSTEP]
right
[GOAL]
case h
α : Type u
L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ ∃ L₅, Step (tl ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: (tl ++ x✝⁴)) L₅
[PROOFSTEP]
exact ⟨_, Red.Step.not, Red.Step.cons_not⟩
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: (x4, b4) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
[PROOFSTEP]
injections
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x3 = x✝¹
snd_eq✝¹ : b3 = x✝
tail_eq✝ : List.append tl ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = x✝⁴
fst_eq✝ : x4 = x✝¹
snd_eq✝ : b4 = !x✝
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ (x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴ = [] ++ List.append tl ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴) ∨
    ∃ L₅,
      Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴) L₅ ∧ Step ([] ++ List.append tl ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴)) L₅
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ (x✝¹, x✝) :: (x✝¹, !x✝) :: (tl ++ x✝⁴) = tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴ ∨
    ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: (tl ++ x✝⁴)) L₅ ∧ Step (tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴) L₅
[PROOFSTEP]
right
[GOAL]
case h
α : Type u
L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: (tl ++ x✝⁴)) L₅ ∧ Step (tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴) L₅
[PROOFSTEP]
exact ⟨_, Red.Step.cons_not, Red.Step.not⟩
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : List.append tl ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = List.append tl2 ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
H3 : tl ++ x✝⁵ = tl2 ++ x✝⁴
⊢ (x3, b3) :: tl ++ x✝⁵ = (x4, b4) :: tl2 ++ x✝⁴
[PROOFSTEP]
simp [H1, H3]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : List.append tl ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = List.append tl2 ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
L₅ : List (α × Bool)
H3 : Step (tl ++ x✝⁵) L₅
H4 : Step (tl2 ++ x✝⁴) L₅
⊢ Step ((x4, b4) :: tl2 ++ x✝⁴) ((x3, b3) :: L₅)
[PROOFSTEP]
simpa [H1] using Step.cons H4
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ a b✝ c b : List (α × Bool)
hab hac : Step a b
⊢ ReflGen Step b b
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ a b✝ c b : List (α × Bool)
hab hac : Step a b
⊢ ReflTransGen Step b b
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
⊢ Red (p :: L₁) (p :: L₂) → Red L₁ L₂
[PROOFSTEP]
generalize eq₁ : (p :: L₁ : List _) = LL₁
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂
[PROOFSTEP]
generalize eq₂ : (p :: L₂ : List _) = LL₂
[GOAL]
α : Type u
L L₁ L₂ 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₂
[PROOFSTEP]
intro h
[GOAL]
α : Type u
L L₁ L₂ 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₂
[PROOFSTEP]
induction' h using Relation.ReflTransGen.head_induction_on with L₁ L₂ h₁₂ h ih generalizing L₁ L₂
[GOAL]
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁✝ : p :: L₁✝ = LL₁
LL₂ : List (α × Bool)
eq₂✝ : p :: L₂✝ = LL₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂
[PROOFSTEP]
subst_vars
[GOAL]
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = p :: L₂✝
eq₂ : p :: L₂ = p :: L₂✝
⊢ Red L₁ L₂
[PROOFSTEP]
cases eq₂
[GOAL]
case refl.refl
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
L₁ : List (α × Bool)
eq₁ : p :: L₁ = p :: L₂
⊢ Red L₁ L₂
[PROOFSTEP]
cases eq₁
[GOAL]
case refl.refl.refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
⊢ Red L₂ L₂
[PROOFSTEP]
constructor
[GOAL]
case head
α : Type u
L L₁✝¹ L₂✝¹ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁✝ : p :: L₁✝¹ = LL₁
LL₂ : List (α × Bool)
eq₂✝ : p :: L₂✝¹ = 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₂
[PROOFSTEP]
subst_vars
[GOAL]
case head
α : Type u
L L₁✝ L₂✝¹ L₃ L₄ : List (α × Bool)
p : α × Bool
L₂✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step L₂✝ (p :: L₂✝¹)
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = p :: L₂✝¹ → Red L₁ L₂
eq₂ : p :: L₂ = p :: L₂✝¹
h₁₂ : Step (p :: L₁) L₂✝
⊢ Red L₁ L₂
[PROOFSTEP]
cases eq₂
[GOAL]
case head.refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
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₂✝
[PROOFSTEP]
cases' p with a b
[GOAL]
case head.refl.mk
α : Type u
L L₁✝ L₂✝ L₃ 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₂✝
[PROOFSTEP]
rw [Step.cons_left_iff] at h₁₂ 
[GOAL]
case head.refl.mk
α : Type u
L L₁✝ L₂✝ L₃ 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₂✝
[PROOFSTEP]
rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
[GOAL]
case head.refl.mk.inl.intro.intro
α : Type u
L✝ L₁✝ L₂ L₃ 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₂
[PROOFSTEP]
exact (ih rfl rfl).head h₁₂
[GOAL]
case head.refl.mk.inr
α : Type u
L L₁ L₂✝ 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
⊢ Red ((a, !b) :: L₂) L₂✝
[PROOFSTEP]
exact (cons_cons h).tail Step.cons_not_rev
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
L : List (α × Bool)
⊢ Red (p :: L ++ L₁) (p :: L ++ L₂) ↔ Red L₁ L₂
[PROOFSTEP]
simp [append_append_left_iff L, cons_cons_iff]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Red L (L₁ ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
[PROOFSTEP]
generalize eq : L₁ ++ L₂ = L₁₂
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ Red L L₁₂ → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
[PROOFSTEP]
intro h
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
[PROOFSTEP]
induction' h with L' L₁₂ hLL' h ih generalizing L₁ L₂
[GOAL]
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂✝ = L₁₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
[PROOFSTEP]
exact ⟨_, _, eq.symm, by rfl, by rfl⟩
[GOAL]
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂✝ = L₁₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₁ L₁
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂✝ = L₁₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₂ L₂
[PROOFSTEP]
rfl
[GOAL]
case tail
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁₂✝ : List (α × Bool)
eq✝ : L₁✝ ++ L₂✝ = L₁₂✝
L' L₁₂ : List (α × Bool)
hLL' : ReflTransGen Step L L'
h : Step L' L₁₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = L' → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
[PROOFSTEP]
cases' h with s e a b
[GOAL]
case tail.not
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂✝ = L₁₂
L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
[PROOFSTEP]
rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
[GOAL]
case tail.not.inl.intro.intro
α : Type u
L L₁✝ L₂ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂ = L₁₂
L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
[PROOFSTEP]
have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) = L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
[GOAL]
α : Type u
L L₁✝ L₂ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂ = L₁₂
L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
[PROOFSTEP]
simp
[GOAL]
case tail.not.inl.intro.intro
α : Type u
L L₁✝ L₂ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂ = L₁₂
L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
[PROOFSTEP]
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
[GOAL]
case tail.not.inl.intro.intro.intro.intro.intro.intro
α : Type u
L₁✝ L₂ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁✝ ++ L₂ = L₁₂
L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
h₁ : Red w₁ L₁
h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
[PROOFSTEP]
exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩
[GOAL]
case tail.not.inr.intro.intro
α : Type u
L L₁ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁ ++ L₂✝ = L₁₂
L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
[PROOFSTEP]
have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ = s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
[GOAL]
α : Type u
L L₁ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁ ++ L₂✝ = L₁₂
L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
[PROOFSTEP]
simp
[GOAL]
case tail.not.inr.intro.intro
α : Type u
L L₁ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁ ++ L₂✝ = L₁₂
L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
[PROOFSTEP]
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
[GOAL]
case tail.not.inr.intro.intro.intro.intro.intro.intro
α : Type u
L₁ L₂✝ L₃ L₄ L₁₂ : List (α × Bool)
eq✝ : L₁ ++ L₂✝ = L₁₂
L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')
h₂ : Red w₂ L₂
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
[PROOFSTEP]
exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
⊢ Red L [(x, !b)]
[PROOFSTEP]
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]
[PROOFSTEP]
have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]
[PROOFSTEP]
let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]
[PROOFSTEP]
rw [singleton_iff] at h₁ 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]
[PROOFSTEP]
subst L'
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]
[PROOFSTEP]
assumption
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]
[PROOFSTEP]
apply reflTransGen_iff_eq
[GOAL]
case h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
[PROOFSTEP]
generalize eq : [(x1, not b1), (x2, b2)] = L'
[GOAL]
case h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
⊢ ∀ (b : List (α × Bool)), ¬Step L' b
[PROOFSTEP]
intro L h'
[GOAL]
case h
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
L : List (α × Bool)
h' : Step L' L
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
case h.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : [(x1, !b1), (x2, b2)] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False
[PROOFSTEP]
simp [List.cons_eq_append_iff, List.nil_eq_append] at eq 
[GOAL]
case h.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : L₁✝ = [] ∧ (x✝ = x1 ∧ b✝ = !b1) ∧ (x✝ = x2 ∧ (!b✝) = b2) ∧ L₂✝ = []
⊢ False
[PROOFSTEP]
rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩
[GOAL]
case h.not.intro.intro.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
[PROOFSTEP]
subst_vars
[GOAL]
case h.not.intro.intro.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
[PROOFSTEP]
have : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂) := H2
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
[PROOFSTEP]
rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩
[GOAL]
case intro.nil.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
[PROOFSTEP]
simp [nil_iff] at h₁ 
[GOAL]
case intro.cons.intro.intro.intro
α : Type u
L L₁ L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
[PROOFSTEP]
cases eq
[GOAL]
case intro.cons.intro.intro.intro.refl
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red (List.append L₃ L₄) ((x1, !b1) :: (x2, b2) :: L₂)
[PROOFSTEP]
show Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)
[GOAL]
case intro.cons.intro.intro.intro.refl
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)
[PROOFSTEP]
apply append_append _ h₂
[GOAL]
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red L₃ [(x1, !b1), (x2, b2)]
[PROOFSTEP]
have h₁ : Red ((x1, not b1) :: (x1, b1) :: L₃) [(x1, not b1), (x2, b2)] := cons_cons h₁
[GOAL]
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]
[PROOFSTEP]
have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
[GOAL]
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
⊢ Red L₃ [(x1, !b1), (x2, b2)]
[PROOFSTEP]
rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩
[GOAL]
case intro.intro
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
[PROOFSTEP]
rw [red_iff_irreducible H1] at h₁ 
[GOAL]
case intro.intro
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
[PROOFSTEP]
rwa [h₁] at h₂ 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁
[PROOFSTEP]
cases H
[GOAL]
case not
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
[PROOFSTEP]
simp
[GOAL]
case not
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
[PROOFSTEP]
constructor
[GOAL]
case not.a
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ (x✝, !b✝) :: L₂✝
[PROOFSTEP]
constructor
[GOAL]
case not.a.a
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ L₂✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
induction' L1 with hd tl ih
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
case cons
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
case nil =>
  -- dsimp [sizeOf]
  dsimp
  simp only [Bool.sizeOf_eq_one]
  have H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + ((1 + 1) + (1 + 1) + 1)) := by ac_rfl
  rw [H]
  apply Nat.lt_add_of_pos_right
  apply Nat.lt_add_right
  apply Nat.zero_lt_one
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
case nil =>
  -- dsimp [sizeOf]
  dsimp
  simp only [Bool.sizeOf_eq_one]
  have H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + ((1 + 1) + (1 + 1) + 1)) := by ac_rfl
  rw [H]
  apply Nat.lt_add_of_pos_right
  apply Nat.lt_add_right
  apply Nat.zero_lt_one
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)
[PROOFSTEP]
simp only [Bool.sizeOf_eq_one]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2)
[PROOFSTEP]
have H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + ((1 + 1) + (1 + 1) + 1)) := by ac_rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ sizeOf L2 < 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2)
[PROOFSTEP]
rw [H]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ sizeOf L2 < sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
[PROOFSTEP]
apply Nat.lt_add_of_pos_right
[GOAL]
case h
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ 0 < 1 + (1 + 1 + (1 + 1) + 1)
[PROOFSTEP]
apply Nat.lt_add_right
[GOAL]
case h.h
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ 0 < 1
[PROOFSTEP]
apply Nat.zero_lt_one
[GOAL]
case cons
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
case cons =>
  dsimp
  exact Nat.add_lt_add_left ih _
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
case cons =>
  dsimp
  exact Nat.add_lt_add_left ih _
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
[PROOFSTEP]
exact Nat.add_lt_add_left ih _
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, List.length L₁ = List.length L₂ + 2 * n
[PROOFSTEP]
induction' h with L₂ L₃ _h₁₂ h₂₃ ih
[GOAL]
case refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∃ n, List.length L₁ = List.length L₁ + 2 * n
[PROOFSTEP]
exact ⟨0, rfl⟩
[GOAL]
case tail
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
ih : ∃ n, List.length L₁ = List.length L₂ + 2 * n
⊢ ∃ n, List.length L₁ = List.length L₃ + 2 * n
[PROOFSTEP]
rcases ih with ⟨n, eq⟩
[GOAL]
case tail.intro
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : List.length L₁ = List.length L₂ + 2 * n
⊢ ∃ n, List.length L₁ = List.length L₃ + 2 * n
[PROOFSTEP]
exists 1 + n
[GOAL]
case tail.intro
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : List.length L₁ = List.length L₂ + 2 * n
⊢ List.length L₁ = List.length L₃ + 2 * (1 + n)
[PROOFSTEP]
simp [mul_add, eq, (Step.length h₂₃).symm, add_assoc]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ a b✝ c b : List (α × Bool)
hab hac : Red.Step a b
⊢ ReflGen Red.Step b b
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ a b✝ c b : List (α × Bool)
hab hac : Red.Step a b
⊢ ReflTransGen Red.Step b b
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ List.length (invRev L₁) = List.length L₁
[PROOFSTEP]
simp [invRev]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ invRev (invRev L₁) = L₁
[PROOFSTEP]
simp [invRev, List.map_reverse, (· ∘ ·)]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ (Red.Step ⇒ Red.Step) invRev invRev
[PROOFSTEP]
intro a b h
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
h : Red.Step a b
⊢ Red.Step (invRev a) (invRev b)
[PROOFSTEP]
cases h
[GOAL]
case not
α : Type u
L L₁ L₂ L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (invRev (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (invRev (L₁✝ ++ L₂✝))
[PROOFSTEP]
simp [invRev]
[GOAL]
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁ L₂ : List (α × Bool)
h : Step L₁ L₂
⊢ Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
[PROOFSTEP]
cases' h with a b x y
[GOAL]
case not
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
x : α
y : Bool
⊢ Step (FreeGroup.invRev (a ++ (x, y) :: (x, !y) :: b)) (FreeGroup.invRev (a ++ b))
[PROOFSTEP]
simp [FreeGroup.invRev]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
⊢ Step L₁ L₂
[PROOFSTEP]
simpa only [invRev_invRev] using h.invRev
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂
[PROOFSTEP]
simpa only [invRev_invRev] using h.invRev
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a b c : FreeGroup α), a * b * c = a * (b * c)
[PROOFSTEP]
rintro ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩
[GOAL]
case mk.mk.mk
α : Type u
L L₁✝ L₂✝ L₃✝ L₄ : List (α × Bool)
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
c✝ : FreeGroup α
L₃ : List (α × Bool)
⊢ Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃ =
    Quot.mk Red.Step L₁ * (Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃)
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), 1 * a = a
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ 1 * Quot.mk Red.Step L = Quot.mk Red.Step L
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a * 1 = a
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ Quot.mk Red.Step L * 1 = Quot.mk Red.Step L
[PROOFSTEP]
simp [one_eq_mk]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a⁻¹ * a = 1
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ (Quot.mk Red.Step L)⁻¹ * Quot.mk Red.Step L = 1
[PROOFSTEP]
exact List.recOn L rfl fun ⟨x, b⟩ tl ih => Eq.trans (Quot.sound <| by simp [invRev, one_eq_mk]) ih
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (Quot.mk Red.Step tl)⁻¹ * Quot.mk Red.Step tl = 1
x : α
b : Bool
⊢ Red.Step (invRev ((x, b) :: tl) ++ (x, b) :: tl) (invRev tl ++ tl)
[PROOFSTEP]
simp [invRev, one_eq_mk]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
let ⟨L₁, hx, hy⟩ := Red.exact.1 H
[GOAL]
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝
[PROOFSTEP]
simp [Red.singleton_iff] at hx hy 
[GOAL]
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝
[PROOFSTEP]
aesop
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
H : Step L₁ L₂
⊢ Lift.aux f L₁ = Lift.aux f L₂
[PROOFSTEP]
cases' H with _ _ _ b
[GOAL]
case not
α : Type u
L L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b : Bool
⊢ Lift.aux f (L₁✝ ++ (x✝, b) :: (x✝, !b) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)
[PROOFSTEP]
cases b
[GOAL]
case not.false
α : Type u
L L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, false) :: (x✝, !false) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)
[PROOFSTEP]
simp [Lift.aux]
[GOAL]
case not.true
α : Type u
L L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, true) :: (x✝, !true) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)
[PROOFSTEP]
simp [Lift.aux]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ ∀ (a b : FreeGroup α),
    Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
      Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
        Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b
[PROOFSTEP]
rintro ⟨L₁⟩ ⟨L₂⟩
[GOAL]
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂)
      (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂)
        (Quot.mk Red.Step L₁) *
      Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂)
        (Quot.mk Red.Step L₂)
[PROOFSTEP]
simp [Lift.aux]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
⊢ ∀ (x : FreeGroup α),
    ↑((fun f =>
              MonoidHom.mk'
                (Quot.lift (Lift.aux f)
                  (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
                (_ :
                  ∀ (a b : FreeGroup α),
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                      Quot.lift (Lift.aux f)
                          (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                        Quot.lift (Lift.aux f)
                          (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
            ((fun g => ↑g ∘ of) g))
        x =
      ↑g x
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
x✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step L) =
    ↑g (Quot.mk Red.Step L)
[PROOFSTEP]
exact
  List.recOn L (g.map_one.symm)
    (by
      rintro ⟨x, _ | _⟩ t (ih : _ = g (mk t))
      · show _ = g ((of x)⁻¹ * mk t)
        simpa [Lift.aux] using ih
      · show _ = g (of x * mk t)
        simpa [Lift.aux] using ih)
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
x✝ : FreeGroup α
L : List (α × Bool)
⊢ ∀ (head : α × Bool) (tail : List (α × Bool)),
    ↑((fun f =>
                MonoidHom.mk'
                  (Quot.lift (Lift.aux f)
                    (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
                  (_ :
                    ∀ (a b : FreeGroup α),
                      Quot.lift (Lift.aux f)
                          (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                        Quot.lift (Lift.aux f)
                            (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                          Quot.lift (Lift.aux f)
                            (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
              ((fun g => ↑g ∘ of) g))
          (Quot.mk Red.Step tail) =
        ↑g (Quot.mk Red.Step tail) →
      ↑((fun f =>
                MonoidHom.mk'
                  (Quot.lift (Lift.aux f)
                    (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
                  (_ :
                    ∀ (a b : FreeGroup α),
                      Quot.lift (Lift.aux f)
                          (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                        Quot.lift (Lift.aux f)
                            (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                          Quot.lift (Lift.aux f)
                            (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
              ((fun g => ↑g ∘ of) g))
          (Quot.mk Red.Step (head :: tail)) =
        ↑g (Quot.mk Red.Step (head :: tail))
[PROOFSTEP]
rintro ⟨x, _ | _⟩ t (ih : _ = g (mk t))
[GOAL]
case mk.false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
g : FreeGroup α →* β
x✝ : FreeGroup α
L : List (α × Bool)
x : α
t : List (α × Bool)
ih :
  ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step t) =
    ↑g (mk t)
⊢ ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step ((x, false) :: t)) =
    ↑g (Quot.mk Red.Step ((x, false) :: t))
[PROOFSTEP]
show _ = g ((of x)⁻¹ * mk t)
[GOAL]
case mk.false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
g : FreeGroup α →* β
x✝ : FreeGroup α
L : List (α × Bool)
x : α
t : List (α × Bool)
ih :
  ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step t) =
    ↑g (mk t)
⊢ ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step ((x, false) :: t)) =
    ↑g ((of x)⁻¹ * mk t)
[PROOFSTEP]
simpa [Lift.aux] using ih
[GOAL]
case mk.true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
g : FreeGroup α →* β
x✝ : FreeGroup α
L : List (α × Bool)
x : α
t : List (α × Bool)
ih :
  ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step t) =
    ↑g (mk t)
⊢ ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step ((x, true) :: t)) =
    ↑g (Quot.mk Red.Step ((x, true) :: t))
[PROOFSTEP]
show _ = g (of x * mk t)
[GOAL]
case mk.true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
g : FreeGroup α →* β
x✝ : FreeGroup α
L : List (α × Bool)
x : α
t : List (α × Bool)
ih :
  ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step t) =
    ↑g (mk t)
⊢ ↑((fun f =>
            MonoidHom.mk'
              (Quot.lift (Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂))
              (_ :
                ∀ (a b : FreeGroup α),
                  Quot.lift (Lift.aux f)
                      (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) (a * b) =
                    Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) a *
                      Quot.lift (Lift.aux f)
                        (_ : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → Lift.aux f L₁ = Lift.aux f L₂) b))
          ((fun g => ↑g ∘ of) g))
      (Quot.mk Red.Step ((x, true) :: t)) =
    ↑g (of x * mk t)
[PROOFSTEP]
simpa [Lift.aux] using ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
⊢ MonoidHom.range (↑lift f) ≤ s
[PROOFSTEP]
rintro _ ⟨⟨L⟩, rfl⟩
[GOAL]
case intro.mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑(↑lift f) (Quot.mk Red.Step L) ∈ s
[PROOFSTEP]
exact
  List.recOn L s.one_mem fun ⟨x, b⟩ tl ih =>
    Bool.recOn b (by simp at ih ⊢; exact s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih)
      (by simp at ih ⊢; exact s.mul_mem (H ⟨x, rfl⟩) ih)
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : ↑(↑lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ ↑(↑lift f) (Quot.mk Red.Step ((x, false) :: tl)) ∈ s
[PROOFSTEP]
simp at ih ⊢
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
x : α
b : Bool
⊢ (f x)⁻¹ * List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
[PROOFSTEP]
exact s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : ↑(↑lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ ↑(↑lift f) (Quot.mk Red.Step ((x, true) :: tl)) ∈ s
[PROOFSTEP]
simp at ih ⊢
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
x : α
b : Bool
⊢ f x * List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
[PROOFSTEP]
exact s.mul_mem (H ⟨x, rfl⟩) ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ MonoidHom.range (↑lift f) = Subgroup.closure (Set.range f)
[PROOFSTEP]
apply le_antisymm (lift.range_le Subgroup.subset_closure)
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ Subgroup.closure (Set.range f) ≤ MonoidHom.range (↑lift f)
[PROOFSTEP]
rw [Subgroup.closure_le]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
⊢ Set.range f ⊆ ↑(MonoidHom.range (↑lift f))
[PROOFSTEP]
rintro _ ⟨a, rfl⟩
[GOAL]
case intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
a : α
⊢ f a ∈ ↑(MonoidHom.range (↑lift f))
[PROOFSTEP]
exact ⟨FreeGroup.of a, by simp only [lift.of]⟩
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
a : α
⊢ ↑(↑lift f) (FreeGroup.of a) = f a
[PROOFSTEP]
simp only [lift.of]
[GOAL]
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁ L₂ : List (α × Bool)
H : Red.Step L₁ L₂
⊢ Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂)
[PROOFSTEP]
cases H
[GOAL]
case not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (List.map (fun x => (f x.fst, x.snd)) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝))
    (List.map (fun x => (f x.fst, x.snd)) (L₁✝ ++ L₂✝))
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
⊢ ∀ (a b : FreeGroup α),
    Quot.map (List.map fun x => (f x.fst, x.snd))
        (_ :
          ∀ (L₁ L₂ : List (α × Bool)),
            Red.Step L₁ L₂ →
              Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂))
        (a * b) =
      Quot.map (List.map fun x => (f x.fst, x.snd))
          (_ :
            ∀ (L₁ L₂ : List (α × Bool)),
              Red.Step L₁ L₂ →
                Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂))
          a *
        Quot.map (List.map fun x => (f x.fst, x.snd))
          (_ :
            ∀ (L₁ L₂ : List (α × Bool)),
              Red.Step L₁ L₂ →
                Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂))
          b
[PROOFSTEP]
rintro ⟨L₁⟩ ⟨L₂⟩
[GOAL]
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.map (List.map fun x => (f x.fst, x.snd))
      (_ :
        ∀ (L₁ L₂ : List (α × Bool)),
          Red.Step L₁ L₂ → Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂))
      (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.map (List.map fun x => (f x.fst, x.snd))
        (_ :
          ∀ (L₁ L₂ : List (α × Bool)),
            Red.Step L₁ L₂ →
              Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂))
        (Quot.mk Red.Step L₁) *
      Quot.map (List.map fun x => (f x.fst, x.snd))
        (_ :
          ∀ (L₁ L₂ : List (α × Bool)),
            Red.Step L₁ L₂ →
              Red.Step (List.map (fun x => (f x.fst, x.snd)) L₁) (List.map (fun x => (f x.fst, x.snd)) L₂))
        (Quot.mk Red.Step L₂)
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝ y x : FreeGroup α
⊢ ↑(map _root_.id) x = x
[PROOFSTEP]
rcases x with ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝ y x : FreeGroup α
L : List (α × Bool)
⊢ ↑(map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L
[PROOFSTEP]
simp [List.map_id']
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f✝ : α → β
x✝ y : FreeGroup α
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ ↑(map g) (↑(map f) x) = ↑(map (g ∘ f)) x
[PROOFSTEP]
rcases x with ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f✝ : α → β
x✝ y : FreeGroup α
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ ↑(map g) (↑(map f) (Quot.mk Red.Step L)) = ↑(map (g ∘ f)) (Quot.mk Red.Step L)
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, ↑g x = ↑(map f) x
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑g (Quot.mk Red.Step L) = ↑(map f) (Quot.mk Red.Step L)
[PROOFSTEP]
exact
  List.recOn L g.map_one fun ⟨x, b⟩ t (ih : g (FreeGroup.mk t) = map f (FreeGroup.mk t)) =>
    Bool.recOn b
      (show g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) = FreeGroup.map f ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) by
        simp [g.map_mul, g.map_inv, hg, ih])
      (show g (FreeGroup.of x * FreeGroup.mk t) = FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by
        simp [g.map_mul, hg, ih])
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝² y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : ↑g (FreeGroup.mk t) = ↑(map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ ↑g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) = ↑(map f) ((FreeGroup.of x)⁻¹ * FreeGroup.mk t)
[PROOFSTEP]
simp [g.map_mul, g.map_inv, hg, ih]
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝² y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : ↑g (FreeGroup.mk t) = ↑(map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ ↑g (FreeGroup.of x * FreeGroup.mk t) = ↑(map f) (FreeGroup.of x * FreeGroup.mk t)
[PROOFSTEP]
simp [g.map_mul, hg, ih]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝ y : FreeGroup α
x : α
⊢ ↑(↑lift (of ∘ f)) (of x) = of (f x)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.99493
β : Type ?u.99494
e : α ≃ β
x : FreeGroup α
⊢ ↑(map ↑e.symm) (↑(map ↑e) x) = x
[PROOFSTEP]
simp [Function.comp, map.comp]
[GOAL]
α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.99493
β : Type ?u.99494
e : α ≃ β
x : FreeGroup β
⊢ ↑(map ↑e) (↑(map ↑e.symm) x) = x
[PROOFSTEP]
simp [Function.comp, map.comp]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ↑(↑lift f) x = ↑prod (↑(map f) x)
[PROOFSTEP]
rw [← lift.unique (prod.comp (map f))]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ↑(MonoidHom.comp prod (map f)) x = ↑prod (↑(map f) x)
[PROOFSTEP]
rfl
[GOAL]
case hg
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), ↑(MonoidHom.comp prod (map f)) (of x) = f x
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Function.LeftInverse (fun x => 1) fun x => ()
[PROOFSTEP]
rintro ⟨_ | ⟨⟨⟨⟩, _⟩, _⟩⟩
[GOAL]
case mk.nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Empty
⊢ (fun x => 1) ((fun x => ()) (Quot.mk Red.Step [])) = Quot.mk Red.Step []
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
⊢ FreeGroup ℤ
[PROOFSTEP]
revert x
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ FreeGroup Unit → FreeGroup ℤ
[PROOFSTEP]
change (FreeGroup Unit →* FreeGroup ℤ)
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ FreeGroup Unit →* FreeGroup ℤ
[PROOFSTEP]
apply map fun _ => (1 : ℤ)
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Function.LeftInverse (fun x => of () ^ x) fun x =>
    sum
      ((let_fun this := map fun x => 1;
        ↑this)
        x)
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Unit
L : List (Unit × Bool)
⊢ (fun x => of () ^ x)
      ((fun x =>
          sum
            ((let_fun this := map fun x => 1;
              ↑this)
              x))
        (Quot.mk Red.Step L)) =
    Quot.mk Red.Step L
[PROOFSTEP]
simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Unit
L : List (Unit × Bool)
⊢ of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) L) = mk L
[PROOFSTEP]
exact List.recOn L (by rfl) (fun ⟨⟨⟩, b⟩ tl ih => by cases b <;> simp [zpow_add] at ih ⊢ <;> rw [ih] <;> rfl)
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Unit
L : List (Unit × Bool)
⊢ of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) []) = mk []
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
b : Bool
⊢ of () ^
      List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) ((PUnit.unit, b) :: tl)) =
    mk ((PUnit.unit, b) :: tl)
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
⊢ of () ^
      List.sum
        (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) ((PUnit.unit, false) :: tl)) =
    mk ((PUnit.unit, false) :: tl)
[PROOFSTEP]
simp [zpow_add] at ih ⊢
[GOAL]
case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
⊢ of () ^
      List.sum
        (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) ((PUnit.unit, true) :: tl)) =
    mk ((PUnit.unit, true) :: tl)
[PROOFSTEP]
simp [zpow_add] at ih ⊢
[GOAL]
case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
⊢ (of ())⁻¹ * of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) =
    mk ((PUnit.unit, false) :: tl)
[PROOFSTEP]
rw [ih]
[GOAL]
case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
⊢ of () * of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) =
    mk ((PUnit.unit, true) :: tl)
[PROOFSTEP]
rw [ih]
[GOAL]
case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
⊢ (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ List.sum (List.map ((fun x => bif x.snd then x.fst else -x.fst) ∘ fun x => (1, x.snd)) tl) = mk tl
⊢ of () * mk tl = mk ((PUnit.unit, true) :: tl)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
⊢ (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) 0) =
    0
[PROOFSTEP]
simp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih :
  (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) ↑i) =
    ↑i
⊢ (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) (↑i + 1)) =
    ↑i + 1
[PROOFSTEP]
simp only [zpow_coe_nat, map_pow, map.of] at ih 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : sum (of 1 ^ i) = ↑i
⊢ (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) (↑i + 1)) =
    ↑i + 1
[PROOFSTEP]
simp [zpow_add, ih]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih :
  (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) (-↑i)) =
    -↑i
⊢ (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) (-↑i - 1)) =
    -↑i - 1
[PROOFSTEP]
simp only [zpow_neg, zpow_coe_nat, map_inv, map_pow, map.of, sum.map_inv, neg_inj] at ih 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : sum (of 1 ^ i) = ↑i
⊢ (fun x =>
        sum
          ((let_fun this := map fun x => 1;
            ↑this)
            x))
      ((fun x => of () ^ x) (-↑i - 1)) =
    -↑i - 1
[PROOFSTEP]
simp [zpow_add, ih, sub_eq_add_neg]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ id <$> (pure x)⁻¹ = (pure x)⁻¹
[PROOFSTEP]
rw [map_inv, ih]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x * y) = x * y
[PROOFSTEP]
rw [map_mul, ihx, ihy]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), 1 >>= f >>= g = 1 >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ 1 >>= f✝ >>= g✝ = 1 >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
iterate 3 rw [one_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ 1 >>= f✝ >>= g✝ = 1 >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [one_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ 1 >>= g✝ = 1 >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [one_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ 1 = 1 >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [one_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ pure x >>= f✝ >>= g✝ = pure x >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
iterate 2 rw [pure_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ pure x >>= f✝ >>= g✝ = pure x >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [pure_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ f✝ x >>= g✝ = pure x >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [pure_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), (pure x)⁻¹ >>= f >>= g = (pure x)⁻¹ >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (pure x)⁻¹ >>= f✝ >>= g✝ = (pure x)⁻¹ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
iterate 3 rw [inv_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (pure x)⁻¹ >>= f✝ >>= g✝ = (pure x)⁻¹ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [inv_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (pure x >>= f✝)⁻¹ >>= g✝ = (pure x)⁻¹ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [inv_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (pure x >>= f✝ >>= g✝)⁻¹ = (pure x)⁻¹ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [inv_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), pure x >>= f >>= g = pure x >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (pure x >>= f✝ >>= g✝)⁻¹ = (pure x >>= fun x => f✝ x >>= g✝)⁻¹
[PROOFSTEP]
rw [ih]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ x y : FreeGroup α✝
ihx : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x => f x >>= g
ihy : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x => f x >>= g
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x * y >>= f >>= g = x * y >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ x y : FreeGroup α✝
ihx : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x => f x >>= g
ihy : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ x * y >>= f✝ >>= g✝ = x * y >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
iterate 3 rw [mul_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ x y : FreeGroup α✝
ihx : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x => f x >>= g
ihy : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ x * y >>= f✝ >>= g✝ = x * y >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [mul_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ x y : FreeGroup α✝
ihx : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x => f x >>= g
ihy : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (x >>= f✝) * (y >>= f✝) >>= g✝ = x * y >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [mul_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ x y : FreeGroup α✝
ihx : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x => f x >>= g
ihy : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (x >>= f✝ >>= g✝) * (y >>= f✝ >>= g✝) = x * y >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rw [mul_bind]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x✝ x y : FreeGroup α✝
ihx : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x => f x >>= g
ihy : ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x => f x >>= g
f✝ : α✝ → FreeGroup β✝
g✝ : β✝ → FreeGroup γ✝
⊢ (x >>= f✝ >>= g✝) * (y >>= f✝ >>= g✝) = (x >>= fun x => f✝ x >>= g✝) * (y >>= fun x => f✝ x >>= g✝)
[PROOFSTEP]
rw [ihx, ihy]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ (do
      let y ← 1
      pure (f y)) =
    f <$> 1
[PROOFSTEP]
rw [one_bind, map_one]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeGroup α✝
x : α✝
⊢ (do
      let y ← pure x
      pure (f y)) =
    f <$> pure x
[PROOFSTEP]
rw [pure_bind, map_pure]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeGroup α✝
x : α✝
ih :
  (do
      let y ← pure x
      pure (f y)) =
    f <$> pure x
⊢ (do
      let y ← (pure x)⁻¹
      pure (f y)) =
    f <$> (pure x)⁻¹
[PROOFSTEP]
rw [inv_bind, map_inv, ih]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeGroup α✝
ihx :
  (do
      let y ← x
      pure (f y)) =
    f <$> x
ihy :
  (do
      let y ← y
      pure (f y)) =
    f <$> y
⊢ (do
      let y ← x * y
      pure (f y)) =
    f <$> (x * y)
[PROOFSTEP]
rw [mul_bind, map_mul, ihx, ihy]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red L (reduce L)
[PROOFSTEP]
induction' L with hd1 tl1 ih
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
[PROOFSTEP]
case nil => constructor
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])
[PROOFSTEP]
case nil => constructor
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])
[PROOFSTEP]
constructor
[GOAL]
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
[PROOFSTEP]
case cons =>
  dsimp
  revert ih
  generalize htl : reduce tl1 = TL
  intro ih
  cases' TL with hd2 tl2
  case nil => exact Red.cons_cons ih
  case cons =>
    dsimp only
    split_ifs with h
    · trans
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
    · exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
[PROOFSTEP]
case cons =>
  dsimp
  revert ih
  generalize htl : reduce tl1 = TL
  intro ih
  cases' TL with hd2 tl2
  case nil => exact Red.cons_cons ih
  case cons =>
    dsimp only
    split_ifs with h
    · trans
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
    · exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (reduce tl1))
[PROOFSTEP]
revert ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
⊢ Red tl1 (reduce tl1) →
    Red (hd1 :: tl1)
      (List.rec [hd1]
        (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
        (reduce tl1))
[PROOFSTEP]
generalize htl : reduce tl1 = TL
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
⊢ Red tl1 TL →
    Red (hd1 :: tl1)
      (List.rec [hd1]
        (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) TL)
[PROOFSTEP]
intro ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
ih : Red tl1 TL
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) TL)
[PROOFSTEP]
cases' TL with hd2 tl2
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) [])
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
[PROOFSTEP]
case nil => exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) [])
[PROOFSTEP]
case nil => exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) [])
[PROOFSTEP]
exact Red.cons_cons ih
[GOAL]
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
[PROOFSTEP]
case cons =>
  dsimp only
  split_ifs with h
  · trans
    · cases hd1
      cases hd2
      cases h
      dsimp at *
      subst_vars
      apply Red.trans (Red.cons_cons ih)
      exact Red.Step.cons_not_rev.to_red
  · exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
[PROOFSTEP]
case cons =>
  dsimp only
  split_ifs with h
  · trans
    · cases hd1
      cases hd2
      cases h
      dsimp at *
      subst_vars
      apply Red.trans (Red.cons_cons ih)
      exact Red.Step.cons_not_rev.to_red
  · exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1) (if hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd then tl2 else hd1 :: hd2 :: tl2)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd
⊢ Red (hd1 :: tl1) tl2
[PROOFSTEP]
trans
[GOAL]
case pos
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd
⊢ Red (hd1 :: tl1) tl2
[PROOFSTEP]
cases hd1
[GOAL]
case pos.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
fst✝ : α
snd✝ : Bool
h : (fst✝, snd✝).fst = hd2.fst ∧ (fst✝, snd✝).snd = !hd2.snd
⊢ Red ((fst✝, snd✝) :: tl1) tl2
[PROOFSTEP]
cases hd2
[GOAL]
case pos.mk.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
h : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd = !(fst✝, snd✝).snd
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
[PROOFSTEP]
cases h
[GOAL]
case pos.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
right✝ : (fst✝¹, snd✝¹).snd = !(fst✝, snd✝).snd
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
[PROOFSTEP]
dsimp at *
[GOAL]
case pos.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : fst✝¹ = fst✝
right✝ : snd✝¹ = !snd✝
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
[PROOFSTEP]
subst_vars
[GOAL]
case pos.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
⊢ Red ((fst✝, !snd✝) :: tl1) tl2
[PROOFSTEP]
apply Red.trans (Red.cons_cons ih)
[GOAL]
case pos.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
⊢ Red ((fst✝, !snd✝) :: (fst✝, snd✝) :: tl2) tl2
[PROOFSTEP]
exact Red.Step.cons_not_rev.to_red
[GOAL]
case neg
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
[PROOFSTEP]
exact Red.cons_cons ih
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
p : Prop
L2 L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = L2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p
[PROOFSTEP]
cases L2
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p
[PROOFSTEP]
injections
[GOAL]
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
h : reduce [] = head✝ :: tail✝ ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p
[PROOFSTEP]
injections
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        (reduce L1) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]
cases r : reduce L1 with
| nil =>
  dsimp
  intro h
  exfalso
  have := congr_arg List.length h
  simp [List.length] at this 
  rw [add_comm, add_assoc, add_assoc, add_comm, <- add_assoc] at this 
  simp [Nat.one_eq_succ_zero, Nat.succ_add] at this 
  cases this
| cons hd tail =>
  cases' hd with y c
  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
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
x✝ : List (α × Bool)
r : reduce L1 = x✝
⊢ List.rec [(x, b)] (fun head tail tail_ih => if x = head.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        x✝ =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]
cases r : reduce L1 with
| nil =>
  dsimp
  intro h
  exfalso
  have := congr_arg List.length h
  simp [List.length] at this 
  rw [add_comm, add_assoc, add_assoc, add_comm, <- add_assoc] at this 
  simp [Nat.one_eq_succ_zero, Nat.succ_add] at this 
  cases this
| cons hd tail =>
  cases' hd with y c
  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
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        [] =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]

| nil =>
  dsimp
  intro h
  exfalso
  have := congr_arg List.length h
  simp [List.length] at this 
  rw [add_comm, add_assoc, add_assoc, add_comm, <- add_assoc] at this 
  simp [Nat.one_eq_succ_zero, Nat.succ_add] at this 
  cases this
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        [] =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]
dsimp
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
intro h
[GOAL]
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
exfalso
[GOAL]
case nil.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
have := congr_arg List.length h
[GOAL]
case nil.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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 : List.length [(x, b)] = List.length (L2 ++ (x', b') :: (x', !b') :: L3)
⊢ False
[PROOFSTEP]
simp [List.length] at this 
[GOAL]
case nil.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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 = List.length L2 + (List.length L3 + 1 + 1)
⊢ False
[PROOFSTEP]
rw [add_comm, add_assoc, add_assoc, add_comm, <- add_assoc] at this 
[GOAL]
case nil.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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 = 1 + 1 + List.length L2 + List.length L3
⊢ False
[PROOFSTEP]
simp [Nat.one_eq_succ_zero, Nat.succ_add] at this 
[GOAL]
case nil.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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 : 0 = List.length L2 + List.length L3 + Nat.succ 0
⊢ False
[PROOFSTEP]
cases this
[GOAL]
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
hd : α × Bool
tail : List (α × Bool)
r : reduce L1 = hd :: tail
⊢ List.rec [(x, b)] (fun head tail tail_ih => if x = head.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        (hd :: tail) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]

| cons hd tail =>
  cases' hd with y c
  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
[GOAL]
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
hd : α × Bool
tail : List (α × Bool)
r : reduce L1 = hd :: tail
⊢ List.rec [(x, b)] (fun head tail tail_ih => if x = head.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        (hd :: tail) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]
cases' hd with y c
[GOAL]
case cons.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
⊢ List.rec [(x, b)] (fun head tail tail_ih => if x = head.fst ∧ b = !head.snd then tail else (x, b) :: head :: tail)
        ((y, c) :: tail) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
[PROOFSTEP]
dsimp only
[GOAL]
case cons.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
⊢ tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
[PROOFSTEP]
intro H
[GOAL]
case neg
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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)
⊢ (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
[PROOFSTEP]
intro H
[GOAL]
case pos
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
rw [H] at r 
[GOAL]
case pos
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
[GOAL]
case neg
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
rcases L2 with (_ | ⟨a, L2⟩)
[GOAL]
case neg.nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
⊢ p
[PROOFSTEP]
injections
[GOAL]
case neg.nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
subst_vars
[GOAL]
case neg.nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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
[PROOFSTEP]
simp at h 
[GOAL]
case neg.cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ p
[PROOFSTEP]
refine' @reduce.not _ L1 L2 L3 x' b' _
[GOAL]
case neg.cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
[PROOFSTEP]
injection H with _ H
[GOAL]
case neg.cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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 = List.append L2 ((x', b') :: (x', !b') :: L3)
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
[PROOFSTEP]
rw [r, H]
[GOAL]
case neg.cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
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 = List.append L2 ((x', b') :: (x', !b') :: L3)
⊢ List.append L2 ((x', b') :: (x', !b') :: L3) = L2 ++ (x', b') :: (x', !b') :: L3
[PROOFSTEP]
rfl
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
H : Red (reduce L₁) L₂
⊢ reduce L₁ = L₂
[PROOFSTEP]
induction' H with L1 L' L2 H1 H2 ih
[GOAL]
case refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce L₁ = reduce L₁
[PROOFSTEP]
rfl
[GOAL]
case tail
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
L1 L' : List (α × Bool)
L2 : ReflTransGen Red.Step (reduce L₁) L1
H1 : Red.Step L1 L'
H2 : reduce L₁ = L1
⊢ reduce L₁ = L'
[PROOFSTEP]
cases' H1 with L4 L5 x b
[GOAL]
case tail.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
L4 L5 : List (α × Bool)
x : α
b : Bool
L2 : ReflTransGen Red.Step (reduce L₁) (L4 ++ (x, b) :: (x, !b) :: L5)
H2 : reduce L₁ = L4 ++ (x, b) :: (x, !b) :: L5
⊢ reduce L₁ = L4 ++ L5
[PROOFSTEP]
exact reduce.not H2
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ ∀ {x : FreeGroup α}, mk (toWord x) = x
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L
[PROOFSTEP]
exact reduce.self
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Function.Injective toWord
[PROOFSTEP]
rintro ⟨L₁⟩ ⟨L₂⟩
[GOAL]
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
[PROOFSTEP]
exact reduce.exact
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ ∀ (x : FreeGroup α), reduce (toWord x) = toWord x
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ reduce (toWord (Quot.mk Red.Step L)) = toWord (Quot.mk Red.Step L)
[PROOFSTEP]
exact reduce.idem
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ reduce (invRev w) = invRev (reduce w)
[PROOFSTEP]
apply reduce.min
[GOAL]
case H
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (reduce (invRev w)) (invRev (reduce w))
[PROOFSTEP]
rw [← red_invRev_iff, invRev_invRev]
[GOAL]
case H
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)
[PROOFSTEP]
apply Red.reduce_left
[GOAL]
case H.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red w (invRev (reduce (invRev w)))
[PROOFSTEP]
have : Red (invRev (invRev w)) (invRev (reduce (invRev w))) := reduce.red.invRev
[GOAL]
case H.h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))
[PROOFSTEP]
rwa [invRev_invRev] at this 
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
⊢ toWord x⁻¹ = invRev (toWord x)
[PROOFSTEP]
rcases x with ⟨L⟩
[GOAL]
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
[PROOFSTEP]
rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
⊢ norm x⁻¹ = norm x
[PROOFSTEP]
simp only [norm, toWord_inv, invRev_length]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
⊢ norm x = 0 ↔ x = 1
[PROOFSTEP]
simp only [norm, List.length_eq_zero, toWord_eq_nil_iff]
[GOAL]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ norm (x * y) = norm (mk (toWord x ++ toWord y))
[PROOFSTEP]
rw [← mul_mk, mk_toWord, mk_toWord]
