awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ (b : β), b ∈ cb ∧ R a b
have pure : ∀ (b : β), LiftRelAux R C (Sum.inl a) (pure b).destruct ↔ ∃ (b_1 : β), b_1 ∈ pure b ∧ R a b_1
Tactic: induction cb using recOn with
  | pure b =>
    exact
      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
  | think cb =>
    rw [destruct_think]
    exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩
Cleared hypotheses: cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
pure :
  ∀ (b : β), LiftRelAux R C (Sum.inl a) (Computation.pure b).destruct ↔ ∃ (b_1 : β), b_1 ∈ Computation.pure b ∧ R a b_1
⊢ LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ (b : β), b ∈ cb ∧ R a b
have think : ∀ (cb : Computation β), LiftRelAux R C (Sum.inl a) cb.think.destruct ↔ ∃ (b : β), b ∈ cb.think ∧ R a b
Tactic: induction cb using recOn with
  | pure b =>
    exact
      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
  | think cb =>
    rw [destruct_think]
    exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩
Cleared hypotheses: cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b a =
    LiftRelAux R C a b
have inl : ∀ (a : α),
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) b
Tactic: rcases a with a | ca
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
inl :
  ∀ (a : α),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inl a) =
      LiftRelAux R C (Sum.inl a) b
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b a =
    LiftRelAux R C a b
have inr : ∀ (ca : Computation α),
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) b
Tactic: rcases a with a | ca
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
b : β ⊕ Computation β
a : α
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) b
have inl : ∀ (b : β),
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) (Sum.inl b)
Tactic: rcases b with b | cb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
b : β ⊕ Computation β
a : α
inl :
  ∀ (b : β),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inl a) =
      LiftRelAux R C (Sum.inl a) (Sum.inl b)
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) b
have inl₁ : ∀ (cb : Computation β),
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inr cb) (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) (Sum.inr cb)
Tactic: rcases b with b | cb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
b : β ⊕ Computation β
ca : Computation α
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) b
have inr : ∀ (b : β),
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) (Sum.inl b)
Tactic: rcases b with b | cb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
b : β ⊕ Computation β
ca : Computation α
inr :
  ∀ (b : β),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inr ca) =
      LiftRelAux R C (Sum.inr ca) (Sum.inl b)
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) b
have inr₁ : ∀ (cb : Computation β),
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inr cb) (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) (Sum.inr cb)
Tactic: rcases b with b | cb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ (a : α), a ∈ ca ∧ R a b
have rw : LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
    (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) ca.destruct ↔
  ∃ (a : α), a ∈ ca ∧ R a b
Tactic: rw [← LiftRelAux.swap, LiftRelAux.ret_left]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
rw :
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) ca.destruct ↔
    ∃ (a : α), a ∈ ca ∧ R a b
⊢ LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ (a : α), a ∈ ca ∧ R a b
have rw₁ : (∃ (b_1 : α), b_1 ∈ ca ∧ Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R b b_1) ↔ ∃ (a : α), a ∈ ca ∧ R a b
Tactic: rw [← LiftRelAux.swap, LiftRelAux.ret_left]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
cb : Computation β
Hc : C ca cb
a : α
ha : a ∈ ca
⊢ LiftRel R ca cb
have revert : ∀ (cb : Computation β) (Hc : C ca cb), LiftRel R ca cb
Tactic: revert cb
Cleared hypotheses: cb, Hc
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β) (Hc : C ca cb), LiftRel R ca cb
have refine_1 : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) (pure a)
Tactic: refine memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
    ha ?_ (fun ca' IH => ?_)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
refine_1 : ∀ (cb : Computation β), C (pure a) cb → LiftRel R (pure a) cb
⊢ ∀ (cb : Computation β) (Hc : C ca cb), LiftRel R ca cb
have refine_2 : ∀ (ca' : Computation α) (IH : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'),
  (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'.think
Tactic: refine memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
    ha ?_ (fun ca' IH => ?_)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
⊢ LiftRel R (pure a) cb
have h : LiftRelAux R C (pure a).destruct cb.destruct
Tactic: have h := H Hc
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C ca'.think cb
⊢ LiftRel R ca'.think cb
have h : LiftRelAux R C ca'.think.destruct cb.destruct
Tactic: have h := H Hc
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : LiftRelAux R C (pure a).destruct cb.destruct
⊢ LiftRel R (pure a) cb
have h₁ : ∃ (b : β), b ∈ cb ∧ R a b
Tactic: simp only [destruct_pure, LiftRelAux.ret_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C ca'.think cb
h : LiftRelAux R C ca'.think.destruct cb.destruct
⊢ LiftRel R ca'.think cb
have refine_2 : LiftRel R ca' cb
Tactic: simp only [liftRel_think_left]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C ca'.think cb
h : LiftRelAux R C ca'.think.destruct cb.destruct
⊢ LiftRel R ca' cb
have refine_2 : ∀ (b : β) (Hc : C ca'.think (pure b)) (h : LiftRelAux R C ca'.think.destruct (pure b).destruct), LiftRel R ca' (pure b)
Tactic: induction cb using recOn with
    | pure b => simpa using h
    | think cb => simpa [h] using IH _ h
Cleared hypotheses: cb, Hc, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C ca'.think cb
h : LiftRelAux R C ca'.think.destruct cb.destruct
refine_2 :
  ∀ (b : β) (Hc : C ca'.think (pure b)) (h : LiftRelAux R C ca'.think.destruct (pure b).destruct),
    LiftRel R ca' (pure b)
⊢ LiftRel R ca' cb
have refine_2₁ : ∀ (cb : Computation β) (Hc : C ca'.think cb.think) (h : LiftRelAux R C ca'.think.destruct cb.think.destruct),
  LiftRel R ca' cb.think
Tactic: induction cb using recOn with
    | pure b => simpa using h
    | think cb => simpa [h] using IH _ h
Cleared hypotheses: cb, Hc, h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
m n : ℕ
h : m ≤ n
⊢ s.get? m = none → s.get? n = none
have obtain : ∀ (f : Stream' (Option α)) (al : f.IsSeq),
  get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
    get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) n = none
Tactic: obtain ⟨f, al⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : f.IsSeq
⊢ get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
    get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) n = none
have refl : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
  get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none
Tactic: induction h with | refl => exact id | step _ IH => exact fun h2 ↦ al (IH h2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : f.IsSeq
refl :
  get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
    get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none
⊢ get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
    get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) n = none
have step : ∀ {m_1 : ℕ},
  m.le m_1 →
    ∀
      (IH :
        get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
          get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m_1 = none),
      get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m = none →
        get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) m_1.succ = none
Tactic: induction h with | refl => exact id | step _ IH => exact fun h2 ↦ al (IH h2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
⊢ s.get? 0 = none ↔ s = nil
have refine : ∀ (h : s.get? 0 = none), s = nil
Tactic: refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
h : s.get? 0 = none
⊢ s = nil
have h₁ : ∀ (n : ℕ), s.get? n = get? nil n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ x = y
have rw : some x = some y
Tactic: rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
rw : some x = some y
⊢ x = y
have rw₁ : (cons x s).get? 0 = some y
Tactic: rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
rw : some x = some y
rw₁ : (cons x s).get? 0 = some y
s₁ : Seq α
⊢ x = y
have rw₂ : (cons y t).get? 0 = some y
Tactic: rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
rw : some x = some y
rw₁ : (cons x s).get? 0 = some y
s₁ : Seq α
rw₂ : (cons y t).get? 0 = some y
⊢ x = y
have rw₃ : some y = some y
Tactic: rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
n : ℕ
⊢ s.get? n = t.get? n
have simp_rw : (cons x s).get? (n + 1) = t.get? n
Tactic: simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
n : ℕ
simp_rw : (cons x s).get? (n + 1) = t.get? n
⊢ s.get? n = t.get? n
have simp_rw₁ : (cons y t).get? (n + 1) = t.get? n
Tactic: simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x x' : α
s s' : Seq α
⊢ cons x s = cons x' s' ↔ x = x' ∧ s = s'
have mp : cons x s = cons x' s' → x = x' ∧ s = s'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
x x' : α
s s' : Seq α
mp : cons x s = cons x' s' → x = x' ∧ s = s'
⊢ cons x s = cons x' s' ↔ x = x' ∧ s = s'
have mpr : x = x' ∧ s = s' → cons x s = cons x' s'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
n' : (↑s : Stream' (Option α)).tail n = none
⊢ (↑s : Stream' (Option α)).tail (n + 1) = none
have obtain : ∀ (f : Stream' (Option α)) (al : f.IsSeq)
  (n' : (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α)).tail n = none),
  (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α)).tail (n + 1) = none
Tactic: obtain ⟨f, al⟩ := s
Cleared hypotheses: s, n'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
⊢ s.get? 0 = Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0)
have none : Eq.{u + 1} (α := Option α) none (Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> none))
Tactic: cases get? s 0
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
none :
  Eq.{u + 1} (α := Option α) Option.none
    (Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> Option.none))
⊢ s.get? 0 = Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0)
have some : ∀ (val : α), some val = Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> some val)
Tactic: cases get? s 0
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ instFunctorOption.1
      (fun (a' : α) ↦
        (a',
          tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq)
              (some a :: (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))) ⋯)))
      (get?
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq)
          (some a :: (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))) ⋯)
        0) =
    some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al)
have apply : tail
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq)
      (some a :: (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))) sorry) =
  Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al
Tactic: apply congr_arg fun s => some (a, s)
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ tail
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq)
        (some a :: (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al
have a₁ : (↑(tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq)
          (some a :: (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))) sorry)) :
    Stream' (Option α)) =
  (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
⊢ Eq (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) (s.get? 0)) none → s = nil
have none : ∀ (f0 : s.get? 0 = none),
  Eq.{u + 1} (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) none) none → s = nil
Tactic: rcases f0 : get? s 0
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
none :
  ∀ (f0 : s.get? 0 = Option.none),
    Eq.{u + 1} (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) Option.none) Option.none → s = nil
⊢ Eq (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) (s.get? 0)) Option.none → s = nil
have some : ∀ (val : α) (f0 : s.get? 0 = some val),
  Eq (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) (some val)) Option.none → s = nil
Tactic: rcases f0 : get? s 0
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
a : α
s' : Seq α
⊢ Option.map (fun (a' : α) ↦ (a', s.tail)) (s.get? 0) = some (a, s') → s = cons a s'
have none : ∀ (f0 : s.get? 0 = none), Option.map (fun (a' : α) ↦ (a', s.tail)) none = some (a, s') → s = cons a s'
Tactic: rcases f0 : get? s 0 with - | a'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
a : α
s' : Seq α
none :
  ∀ (f0 : s.get? 0 = Option.none), Option.map (fun (a' : α) ↦ (a', s.tail)) Option.none = some (a, s') → s = cons a s'
⊢ Option.map (fun (a' : α) ↦ (a', s.tail)) (s.get? 0) = some (a, s') → s = cons a s'
have some : ∀ (a' : α) (f0 : s.get? 0 = some a'), Option.map (fun (a' : α) ↦ (a', s.tail)) (some a') = some (a, s') → s = cons a s'
Tactic: rcases f0 : get? s 0 with - | a'
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : Option.map (fun (a' : α) ↦ (a', s.tail)) (some a') = some (a, s')
⊢ s = cons a s'
have some : ∀ (f : Stream' (Option α)) (al : f.IsSeq)
  (f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a')
  (h :
    Option.map (fun (a' : α) ↦ (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) (some a') =
      some (a, s')),
  Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al = cons a s'
Tactic: obtain ⟨f, al⟩ := s
Cleared hypotheses: s, f0, h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a'
h :
  Option.map (fun (a' : α) ↦ (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) (some a') =
    some (a, s')
⊢ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al = cons a s'
have h1 : a' = a
Tactic: injections _ h1 h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
Goal:
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a'
h :
  Option.map (fun (a' : α) ↦ (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) (some a') =
    some (a, s')
h1 : a' = a
⊢ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al = cons a s'
have h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
Tactic: injections _ h1 h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a'
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
⊢ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al = cons a s'
have some : Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al =
  cons a (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))
Tactic: rw [← h2]