-- Mathlib/Data/Seq/WSeq.lean
theorem Equiv.ext {s t : WSeq α} (h : ∀ n, get? s n ~ get? t n) : s ~ʷ t :=
  ⟨fun s t => ∀ n, get? s n ~ get? t n, h, fun {s t} h => by
    refine liftRel_def.2 ⟨?_, ?_⟩
    · rw [← head_terminates_iff, ← head_terminates_iff]
      exact terminates_congr (h 0)
    · intro a b ma mb
      rcases a with - | a <;> rcases b with - | b
      · trivial
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · obtain ⟨a, s'⟩ := a
        obtain ⟨b, t'⟩ := b
        injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab
        refine ⟨ab, fun 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))
        rw [get?_tail, get?_tail]
        apply h⟩

Proof state:
case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
intro a b ma mb

Result:
case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a b : Option (α × WSeq α)
ma : a ∈ s.destruct
mb : b ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Proof state:
case refine_2.some.some.mk.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ s'.get? n ~ t'.get? n

Tactic:
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))

Result:
case refine_2.some.some.mk.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ s.tail.get? n ~ t.tail.get? n

Proof state:
case refine_2.some.some.mk.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ s.tail.get? n ~ t.tail.get? n

Tactic:
rw [get?_tail, get?_tail]

Result:
case refine_2.some.some.mk.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').fst = (b, t').fst
n : ℕ
⊢ s.get? (n + 1) ~ t.get? (n + 1)

Proof state:
case refine_2.none.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)

Tactic:
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))

Result:
no goals

Proof state:
case refine_1
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ s.destruct.Terminates ↔ t.destruct.Terminates

Tactic:
rw [← head_terminates_iff, ← head_terminates_iff]

Result:
case refine_1
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ s.head.Terminates ↔ t.head.Terminates

Proof state:
case refine_2.some.some.mk.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some (b, t'))

Tactic:
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
  ab

Result:
case refine_2.some.some.mk.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').fst = (b, t').fst
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some (b, t'))

Proof state:
case refine_1
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ s.head.Terminates ↔ t.head.Terminates

Tactic:
exact terminates_congr (h 0)

Result:
no goals

Proof state:
case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a b : Option (α × WSeq α)
ma : a ∈ s.destruct
mb : b ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
rcases a with - | a <;> rcases b with - | b

Result:
case refine_2.none.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) none none

case refine_2.none.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)

case refine_2.some.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) none

case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)

Proof state:
case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)

Tactic:
obtain ⟨a, s'⟩ := a

Result:
case refine_2.some.some.mk
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : α × WSeq α
mb : some b ∈ t.destruct
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some b)

Proof state:
case refine_2.none.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO (fun x1 x2 => x1 = x2) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) none none

Tactic:
trivial

Result:
no goals