-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_dropn_destruct {R : α → β → Prop} {s t} (H : LiftRel R s t) :
    ∀ n, Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (drop s n)) (destruct (drop t n))
  | 0 => liftRel_destruct H
  | n + 1 => by
    simp only [LiftRelO, drop, Nat.add_eq, Nat.add_zero, destruct_tail, tail.aux]
    apply liftRel_bind
    · apply liftRel_dropn_destruct H n
    exact fun {a b} o =>
      match a, b, o with
      | none, none, _ => by
        -- Porting note: These 2 theorems should be excluded.
        simp [-liftRel_pure_left, -liftRel_pure_right]
      | some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop (n + 1)).destruct (t.drop (n + 1)).destruct

Tactic:
simp only [LiftRelO, drop, Nat.add_eq, Nat.add_zero, destruct_tail, tail.aux]

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)

Tactic:
apply liftRel_bind

Result:
case h1
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel ?R (s.drop n).destruct (t.drop n).destruct

case h2
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    ?R a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)

case R
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Option (α × WSeq α) → Option (β × WSeq β) → Prop

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux (some (a, s))) (tail.aux (some (b, t)))

Tactic:
simpa [tail.aux] using liftRel_destruct h2

Result:
no goals

Proof state:
case h1
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel ?R (s.drop n).destruct (t.drop n).destruct

Tactic:
apply liftRel_dropn_destruct H n

Result:
no goals

Proof state:
case h2
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)

Tactic:
exact fun {a b} o =>
  match a, b, o with
  | none, none, _ => by
    simp [-liftRel_pure_left, -liftRel_pure_right]
  | some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
a : Option (α × WSeq α)
b : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a b
x✝ : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux none) (tail.aux none)

Tactic:
simp [-liftRel_pure_left, -liftRel_pure_right]

Result:
no goals