awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
nil :
  match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f (join WSeq.nil)),
    Seq.destruct (map (map f) WSeq.nil).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
⊢ match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f S.join),
    Seq.destruct (map (map f) S).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
have nil₁ : ∀ (x : WSeq α) (s : WSeq (WSeq α)),
  match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f (cons x s).join),
    Seq.destruct (map (map f) (cons x s)).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
nil :
  match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f (join WSeq.nil)),
    Seq.destruct (map (map f) WSeq.nil).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
nil₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f (cons x s).join),
      Seq.destruct (map (map f) (cons x s)).join with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
    | x, x_1 => False
⊢ match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f S.join),
    Seq.destruct (map (map f) S).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
have nil₂ : ∀ (s : WSeq (WSeq α)),
  match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f s.think.join),
    Seq.destruct (map (map f) s.think).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
x : WSeq α
s : WSeq (WSeq α)
⊢ match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f (cons x s).join),
    Seq.destruct (map (map f) (cons x s)).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
have nil : ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)),
  (map f x).append (map f s.join) = s_1.append (map f S.join) ∧
    (map f x).append (map (map f) s).join = s_1.append (map (map f) S).join
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
s : WSeq (WSeq α)
⊢ match (motive := Option (Seq1 (Option β)) → Option (Seq1 (Option β)) → Prop) Seq.destruct (map f s.think.join),
    Seq.destruct (map (map f) s.think).join with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)), s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False
have nil : ∃ (s_1 : WSeq β) (S : WSeq (WSeq α)),
  map f s.join = s_1.append (map f S.join) ∧ (map (map f) s).join = s_1.append (map (map f) S).join
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
⊢ ∃ (s : WSeq β) (S_2 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_2.join) ∧ (map (map f) S).join = s.append (map (map f) S_2).join
have refine_1 : map f S.join = append nil (map f S.join)
Tactic: refine ⟨nil, S, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ (s : WSeq β) (S : WSeq (WSeq α)), s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
refine_1 : map f S.join = append nil (map f S.join)
⊢ ∃ (s : WSeq β) (S_2 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_2.join) ∧ (map (map f) S).join = s.append (map (map f) S_2).join
have refine_2 : (map (map f) S).join = append nil (map (map f) S).join
Tactic: refine ⟨nil, S, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ (s : WSeq β) (S_1 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join
have r : map f S.join = append nil (map f S.join)
Tactic: refine ⟨nil, S, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
r : map f S.join = append nil (map f S.join)
⊢ ∃ (s : WSeq β) (S_1 : WSeq (WSeq α)),
    map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join
have r₁ : (map (map f) S).join = append nil (map (map f) S).join
Tactic: refine ⟨nil, S, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Defs (goal)
Goal:
α : Type u
s : WSeq α
⊢ s.length = Computation.map List.length s.toList
have c1 : Computation.IsBisimulation (α := ℕ) fun (c1 c2 : Computation ℕ) ↦
  ∃ (l : List α) (s : WSeq α),
    c1 =
        Computation.corec
          (fun (x : ℕ × WSeq α) ↦
            match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
            | (n, s) =>
              match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
              | none => Sum.inl n
              | some (none, s') => Sum.inr (n, s')
              | some (some val, s') => Sum.inr (n + 1, s'))
          (l.length, s) ∧
      c2 =
        Computation.map (α := List α) List.length
          (Computation.corec
            (fun (x : List α × WSeq α) ↦
              match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
              | (l, s) =>
                match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l, s))
Tactic: refine
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨n, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some _, s') => Sum.inr (n + 1, s')) (l.length, s) ∧
            c2 = Computation.map List.length (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l, s)))
      ?_ ⟨[], s, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
⊢ (s.tail.get? n).Terminates
have rw : (s.get? (n + 1)).Terminates
Tactic: rw [get?_tail]
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n m : ℕ
⊢ ((s.drop n).get? m).Terminates
have rw : (s.get? (n + m)).Terminates
Tactic: rw [← get?_add]
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s : WSeq α).get? n).Terminates
have rw : (Computation.pure (s.get? n)).Terminates
Tactic: rw [get?_ofSeq]
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.Productive ↔ t.Productive
have simp : (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates
Tactic: simp only [productive_iff]
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) n) none
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
have none : ∀ (e : (s.get? (n + 1)).get = none), Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
Tactic: cases e : Computation.get (get? s (n + 1))
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) n) Option.none
none :
  ∀ (e : (s.get? (n + 1)).get = Option.none),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) Option.none
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) Option.none
have some : ∀ (val : α) (e : (s.get? (n + 1)).get = some val),
  Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) Option.none
Tactic: cases e : Computation.get (get? s (n + 1))
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (hypothesis)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) n) none
val : α
e : (s.get? (n + 1)).get = some val
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
have this : some val ∈ s.get? (n + 1)
Tactic: have := Computation.mem_of_get_eq _ e
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val : α
e : (s.get? (n + 1)).get = some val
this : some val ∈ (s.drop (n + 1)).head
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
have some : ∀ (a' : α) (h' : some a' ∈ (s.drop n).head), Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
Tactic: obtain ⟨a', h'⟩ := head_some_of_head_tail_some this
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (hypothesis)
Goal:
α : Type u
s : WSeq α
inst : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val : α
e : (s.get? (n + 1)).get = some val
this : some val ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
⊢ Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ (s.get? n).get) (n + 1)) none
have this₁ : some a' = none
Tactic: have := mem_unique h' (@Computation.mem_of_get_eq _ _ _ _ h)
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : Seq α
⊢ (↑s : WSeq α).toSeq = s
have a : (↑(↑s : WSeq α).toSeq : Stream' (Option α)) = (↑s : Stream' (Option α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : Seq α
⊢ (↑(↑s : WSeq α).toSeq : Stream' (Option α)) = (↑s : Stream' (Option α))
have a : ∀ (n : ℕ), (↑(↑s : WSeq α).toSeq : Stream' (Option α)) n = (↑s : Stream' (Option α)) n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s : WSeq α).get? n).get = s.get? n
have a : s.get? n ∈ (↑s : WSeq α).get? n
Tactic: apply get_eq_of_mem
-- Lean 4 proof step from Mathlib.Data.WSeq.Productive (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n ∈ (↑s : WSeq α).get? n
have a : s.get? n ∈ Computation.pure (s.get? n)
Tactic: rw [get?_ofSeq]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C)
have h : ∀ (x : Option (β × WSeq β)) (y : Option (α × WSeq α)),
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) x y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) x y
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) x y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) x y
have h : Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none y =
  LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
    (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none y
Tactic: rcases x with ⟨⟩ | ⟨hx, jx⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
h :
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none y
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) x y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) x y
have h₁ : ∀ (hx : β) (jx : WSeq β),
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx)) y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) y
Tactic: rcases x with ⟨⟩ | ⟨hx, jx⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none y
have h : Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none none =
  LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
    (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none none
Tactic: rcases y with ⟨⟩ | ⟨hy, jy⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
h :
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none none =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none none
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none y
have h₁ : ∀ (hy : α) (jy : WSeq α),
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none
      (some (hy, jy)) =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none (some (hy, jy))
Tactic: rcases y with ⟨⟩ | ⟨hy, jy⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx)) y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) y
have h : Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
    none =
  LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
    (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) none
Tactic: rcases y with ⟨⟩ | ⟨hy, jy⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
h :
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
      none =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) none
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx)) y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) y
have h₁ : ∀ (hy : α) (jy : WSeq α),
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
      (some (hy, jy)) =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) (some (hy, jy))
Tactic: rcases y with ⟨⟩ | ⟨hy, jy⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R_1 : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R_1 R) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R_1 (LiftRel R_1)) s.destruct t.destruct
have refine : ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R_1 R a b → LiftRelO R_1 (LiftRel R_1) a b
Tactic: refine Computation.LiftRel.imp ?_ _ _ (h2 h1)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R_1 : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R_1 R) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R_1 R a b → LiftRelO R_1 (LiftRel R_1) a b
have H : ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R_1 s t
Tactic: apply LiftRelO.imp_right
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
have inl : ∀ (h : LiftRel R s t), Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
inl : ∀ (h : LiftRel R s t), Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
have inr : ∀ (h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct),
  Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
    s.destruct t.destruct
have h₁ : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Tactic: have h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t) := by
        obtain h | h := h
        · exact liftRel_destruct h
        · assumption
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h_2 :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
    s.destruct t.destruct
have apply : ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
  LiftRelO R (LiftRel R) a b →
    LiftRelO R
      (fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
      a b
Tactic: apply Computation.LiftRel.imp _ _ _ h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h_2 :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R
        (fun (s : WSeq α) (t : WSeq β) ↦
          LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
        a b
have H : ∀ (s : WSeq α) (t : WSeq β),
  LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Tactic: apply LiftRelO.imp_right
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) s2 s1
have refine : ∀ {s : WSeq β} {t : WSeq α} (h : LiftRel R t s),
  Computation.LiftRel
    (LiftRelO (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) (LiftRel R)))
    s.destruct t.destruct
Tactic: refine ⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => ?_⟩