case refine'_1
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ Terminates (destruct s) ↔ Terminates (destruct t)

case refine'_2
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ destruct s → b ∈ destruct t → LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) a b
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ Computation.LiftRel (LiftRelO (fun x x_1 => x = x_1) fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (destruct s)
    (destruct t)
refine' liftRel_def.2 ⟨_, _⟩
case refine'_1
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ Terminates (head s) ↔ Terminates (head t)
case refine'_1
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ Terminates (destruct s) ↔ Terminates (destruct t)
rw [← head_terminates_iff, ← head_terminates_iff]
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ Terminates (head s) ↔ Terminates (head t)
exact terminates_congr (h 0)
case refine'_2
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a b : Option (α × WSeq α)
ma : a ∈ destruct s
mb : b ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) a b
case refine'_2
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ destruct s → b ∈ destruct t → LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) a b
intro a b ma mb
case refine'_2.none.none
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
ma : none ∈ destruct s
mb : none ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) none none

case refine'_2.none.some
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
ma : none ∈ destruct s
b : α × WSeq α
mb : some b ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) none (some b)

case refine'_2.some.none
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α × WSeq α
ma : some a ∈ destruct s
mb : none ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some a) none

case refine'_2.some.some
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α × WSeq α
ma : some a ∈ destruct s
b : α × WSeq α
mb : some b ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some a) (some b)
case refine'_2
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a b : Option (α × WSeq α)
ma : a ∈ destruct s
mb : b ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) a b
cases' a with a <;> cases' b with b
no goals
case refine'_2.none.none
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
ma : none ∈ destruct s
mb : none ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) none none
trivial
no goals
case refine'_2.none.some
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
ma : none ∈ destruct s
b : α × WSeq α
mb : some b ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) none (some b)
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
no goals
case refine'_2.some.none
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α × WSeq α
ma : some a ∈ destruct s
mb : none ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some a) none
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
case refine'_2.some.some.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
b : α × WSeq α
mb : some b ∈ destruct t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some (a, s')) (some b)
case refine'_2.some.some
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α × WSeq α
ma : some a ∈ destruct s
b : α × WSeq α
mb : some b ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some a) (some b)
cases' a with a s'
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some (a, s')) (some (b, t'))
case refine'_2.some.some.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
b : α × WSeq α
mb : some b ∈ destruct t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some (a, s')) (some b)
cases' b with b t'
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some (a, s')) (some (b, t'))
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some (a, s')) (some (b, t'))
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
  ab
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ get? s' n ~ get? t' n
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
⊢ LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) (some (a, s')) (some (b, t'))
refine' ⟨ab, fun n => _⟩
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ get? (tail s) n ~ get? (tail t) n
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ get? s' n ~ get? t' n
refine'
  (get?_congr (flatten_equiv (Computation.mem_map _ ma)) n).symm.trans
    ((_ : get? (tail s) n ~ get? (tail t) n).trans
      (get?_congr (flatten_equiv (Computation.mem_map _ mb)) n))
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ get? s (n + 1) ~ get? t (n + 1)
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ get? (tail s) n ~ get? (tail t) n
rw [get?_tail, get?_tail]
no goals
case refine'_2.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), get? s✝ n ~ get? t✝ n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), get? s n ~ get? t n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ destruct s
b : α
t' : WSeq α
mb : some (b, t') ∈ destruct t
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ get? s (n + 1) ~ get? t (n + 1)
apply h