awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
inl :
  Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inl₁ : ∀ (x : α) (s : Seq α),
  cons x s = nil ∧ cons x s = nil ∨
    ∃ (x_1 : α),
      ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), cons x s = cons x_1 s₁' ∧ cons x s = cons x_1 s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: cases s₁
Cleared hypotheses: s₁
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inr : ∀ (ih : motive s₁ s₁),
  s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: rcases step s₁ s₂ ih with (rfl | ⟨hd, s₁', s₂', _⟩)
Cleared hypotheses: s₂, ih
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
inr :
  ∀ (ih : motive s₁ s₁),
    s₁ = nil ∧ s₁ = nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inr₁ : ∀ (hd : α) (s₁' s₂' : Seq α),
  s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂' →
    s₁ = nil ∧ s₂ = nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: rcases step s₁ s₂ ih with (rfl | ⟨hd, s₁', s₂', _⟩)
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
⊢ s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inr : ∀ (ih : motive nil nil),
  Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: cases s₁
Cleared hypotheses: s₁, ih
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s₁_1 s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
inr :
  ∀ (ih : motive nil nil),
    Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
have inr₁ : ∀ (x : α) (s : Seq α) (ih : motive (cons x s) (cons x s)),
  cons x s = nil ∧ cons x s = nil ∨
    ∃ (x_1 : α),
      ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), cons x s = cons x_1 s₁' ∧ cons x s = cons x_1 s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Tactic: cases s₁
Cleared hypotheses: s₁, ih
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ f s = g s
have refine : IsBisimulation.{v} (α := β) fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s
Tactic: refine eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) ?_ ⟨s, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ (s : Seq α), s1 = f s ∧ s2 = g s
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
have rcases : ∀ (s : Seq α) (h1 : s1 = f s) (h2 : s2 = g s),
  BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
Tactic: rcases h with ⟨s, h1, h2⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
s_1 : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
have rw : BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
Tactic: rw [h1, h2]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ s.get? n = none ↔ (s.get? n).isNone = true
have none : Eq.{u + 1} (α := Option α) none none ↔ Option.isNone.{u} (α := α) none = true
Tactic: cases s.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
none : Eq.{u + 1} (α := Option α) Option.none Option.none ↔ Option.isNone.{u} (α := α) Option.none = true
⊢ s.get? n = Option.none ↔ (s.get? n).isNone = true
have some : ∀ (val : α), some val = Option.none ↔ (some val).isNone = true
Tactic: cases s.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates ↔ s.Terminates
have mp : (cons x s).Terminates → s.Terminates
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x : α
s : Seq α
mp : (cons x s).Terminates → s.Terminates
⊢ (cons x s).Terminates ↔ s.Terminates
have mpr : s.Terminates → (cons x s).Terminates
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 ↔ s = nil
have refine_1 : s.TerminatedAt 0 → s = nil
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
refine_1 : s.TerminatedAt 0 → s = nil
⊢ s.TerminatedAt 0 ↔ s = nil
have refine_2 : s = nil → s.TerminatedAt 0
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
h : s.TerminatedAt 0
⊢ s = nil
have refine_1 : ∀ (n : ℕ) (a : α), s.get? n = some a ↔ get? nil n = some a
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a : α
⊢ s.get? n = some a ↔ get? nil n = some a
have refine_1 : none = some a ↔ get? nil n = some a
Tactic: rw [le_stable _ (Nat.zero_le _) h]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
s : Seq α
x : α
h : x ∈ s
⊢ ∃ (i : ℕ), some x = s.get? i
have h₁ : some x ∈ (↑s : Stream' (Option α))
Tactic: change (some x ∈ s.1) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
x : α
h : some x ∈ (↑s : Stream' (Option α))
⊢ ∃ (i : ℕ), some x = s.get? i
have rwa : ∀ (h : ∃ (n : ℕ), some x = (↑s : Stream' (Option α)).get n), ∃ (i : ℕ), some x = s.get? i
Tactic: rwa [Stream'.mem_iff_exists_get_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
⊢ C s
have obtain : ∀ (k : ℕ) (e : some a = (↑s : Stream' (Option α)).get k), C s
Tactic: obtain ⟨k, e⟩ := M
Cleared hypotheses: M
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
⊢ s = cons a s.tail
have a₁ : s.destruct = some (a, s.tail)
Tactic: apply destruct_eq_cons
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
⊢ instFunctorOption.1 (fun (a' : α) ↦ (a', s.tail)) ((↑s : Stream' (Option α)) 0) = some (a, s.tail)
have a₁ : instFunctorOption.1 (fun (a' : α) ↦ (a', s.tail)) (some a) = some (a, s.tail)
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
⊢ C s
have zero : ∀ (TH : s = cons a s.tail), C s
Tactic: have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
TH : s = cons a s.tail
⊢ C s
have zero : C (cons a s.tail)
Tactic: rw [TH]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
⊢ (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k
have mk : ∀ (val : Stream' (Option α)) (property : val.IsSeq)
  (e :
    some a =
      (↑(cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) (k + 1)),
  (↑(cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) k.succ =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)) k
Tactic: cases s' using Subtype.recOn
Cleared hypotheses: s', e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
⊢ C (cons b s')
have succ : ∀ (h_eq : (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k), C (cons b s')
Tactic: have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
h_eq : (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k
⊢ C (cons b s')
have e₁ : some a = (↑s' : Stream' (Option α)) k
Tactic: rw [h_eq] at e
Cleared hypotheses: e, h_eq
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
s : Seq α
e : some a = (↑s : Stream' (Option α)) (k + 1)
⊢ C s
have succ : ∀ (e : some a = (↑nil : Stream' (Option α)) (k + 1)), C nil
Tactic: cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))
Cleared hypotheses: s, e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
s : Seq α
e : some a = (↑s : Stream' (Option α)) (k + 1)
succ : ∀ (e : some a = (↑nil : Stream' (Option α)) (k + 1)), C nil
⊢ C s
have succ₁ : ∀ (b : α) (s' : Seq α) (e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)), C (cons b s')
Tactic: cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))
Cleared hypotheses: s, e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s : Stream' (Option α)) k
⊢ C s
have zero : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) 0), C s
Tactic: induction k generalizing s with
  | zero =>
    have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
    rw [TH]
    apply h1 _ _ (Or.inl rfl)
  | succ k IH =>
    cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))
Cleared hypotheses: s, k, e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s : Stream' (Option α)) k
zero : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) 0), C s
⊢ C s
have succ : ∀ (k : ℕ) (IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s) {s : Seq α}
  (e : some a = (↑s : Stream' (Option α)) (k + 1)), C s
Tactic: induction k generalizing s with
  | zero =>
    have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
    rw [TH]
    apply h1 _ _ (Or.inl rfl)
  | succ k IH =>
    cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))
Cleared hypotheses: s, k, e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h :
  Eq.{u + 1} (α := Option α) ((fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) n) none
⊢ Eq.{u + 1} (α := Option α) ((fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) (n + 1))
    none
have rw : ∀ (h : l.length ≤ n), l.length ≤ n + 1
Tactic: rw [List.getElem?_eq_none_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
l : List α
⊢ (↑(a :: l) : Seq α) = cons a (↑l : Seq α)
have h : (↑(a :: l) : Seq α).get? 0 = (cons a (↑l : Seq α)).get? 0
Tactic: ext1 (_ | n)
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
l : List α
h : (↑(a :: l) : Seq α).get? 0 = (cons a (↑l : Seq α)).get? 0
⊢ (↑(a :: l) : Seq α) = cons a (↑l : Seq α)
have h₁ : ∀ (n : ℕ), (↑(a :: l) : Seq α).get? (n + 1) = (cons a (↑l : Seq α)).get? (n + 1)
Tactic: ext1 (_ | n)
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
⊢ Stream'.map (Option.map f) s n = none → Stream'.map (Option.map f) s (n + 1) = none
have dsimp : Option.map f (s n) = none → Option.map f (s (n + 1)) = none
Tactic: dsimp [Stream'.map, Stream'.get]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
⊢ Option.map f (s n) = none → Option.map f (s (n + 1)) = none
have none : ∀ (e : s n = none), Option.map f none = none → Option.map f (s (n + 1)) = none
Tactic: rcases e : s n with - | e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
none : ∀ (e : s n = Option.none), Option.map f Option.none = Option.none → Option.map f (s (n + 1)) = Option.none
⊢ Option.map f (s n) = Option.none → Option.map f (s (n + 1)) = Option.none
have some : ∀ (e : α) (e_1 : s n = some e), Option.map f (some e) = Option.none → Option.map f (s (n + 1)) = Option.none
Tactic: rcases e : s n with - | e
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
⊢ Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none
have pos : ∀ (hi : i = n),
  Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none
Tactic: by_cases hi : i = n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
pos :
  ∀ (hi : i = n),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
⊢ Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none
have neg : ∀ (hi : ¬i = n),
  Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none
Tactic: by_cases hi : i = n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
⊢ IsSeq
    (Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n
      (Option.map f ((↑s : Stream' (Option α)) n)))
have this : ∀ (i : ℕ),
  Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none
Tactic: have (i : ℕ) : Function.update s.val n ((s.get? n).map f) i = none ↔ s.get? i = none := by
      by_cases hi : i = n <;> simp [Function.update, hi]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
this :
  ∀ (i : ℕ),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
⊢ IsSeq
    (Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n
      (Option.map f ((↑s : Stream' (Option α)) n)))
have simp : ∀ {n : ℕ}, s.get? n = none → s.get? (n + 1) = none
Tactic: simp only [IsSeq, val_eq_get, this]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ (a : α), parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
have obtain : ∀ (a : α) (e : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
Tactic: obtain ⟨a, e⟩ := e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = Pure.pure a
have a₁ : (corec parallel.aux1 (l, S)).destruct = Sum.inl a
Tactic: apply destruct_eq_pure
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inl a
have a₁ : Eq.{u + 1} (α := α ⊕ Computation α)
  (match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
      match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) :
    α ⊕ Computation α)
  (Sum.inl a : α ⊕ Computation α)
Tactic: simp only [parallel.aux1, rmap, corec_eq]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α))
          parallel.aux2 l with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct S with
            | none => (b, Seq.nil)
            | some (none, S') => (b, S')
            | some (some c, S') => (c :: b, S')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (corec parallel.aux1 b) :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
have a₁ : Eq.{u + 1} (α := α ⊕ Computation α)
  (match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
      match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) Sum.inl a with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) :
    α ⊕ Computation α)
  (Sum.inl a : α ⊕ Computation α)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
have this : corec parallel.aux1 (l, S) = Pure.pure a
Tactic: have : corec parallel.aux1 (l, S) = return a := by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ (corec parallel.aux1 (l, S)).Terminates
have rw : Terminates (Pure.pure a)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
have lem1 : ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
  (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
Tactic: have lem1 :
    ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := by
    intro l S e
    obtain ⟨a, e⟩ := e
    have : corec parallel.aux1 (l, S) = return a := by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
    rw [this]
    exact ret_terminates a