awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
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
⊢ LiftRelAux R C ca'.think.destruct cb.destruct

Tactic:
have h := H Hc
-- Module: Mathlib.Data.Seq.Computation
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
⊢ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
simp only [destruct_pure, LiftRelAux.ret_left] at h

Premises used: Computation.destruct_pure, Computation.LiftRelAux.ret_left
-- Module: Mathlib.Data.Seq.Computation
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 : ∃ (b : β), b ∈ cb ∧ R a b
⊢ LiftRel R (pure a) cb

Tactic:
simp [h]
-- Module: Mathlib.Data.Seq.Computation
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 : LiftRel R ca' cb
⊢ LiftRel R ca'.think cb

Tactic:
simp only [liftRel_think_left]

Premises used: Computation.liftRel_think_left
-- Module: Mathlib.Data.Seq.Computation
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'
b : β
Hc : C ca'.think (pure b)
h : LiftRelAux R C ca'.think.destruct (pure b).destruct
⊢ LiftRel R ca' (pure b)

Tactic:
simpa using h
-- Module: Mathlib.Data.Seq.Computation
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.think
h : LiftRelAux R C ca'.think.destruct cb.think.destruct
⊢ LiftRel R ca' cb.think

Tactic:
simpa [h] using IH _ h
-- Module: Mathlib.Data.Seq.Computation
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)
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
⊢ LiftRel R ca' cb

Tactic:
induction cb using recOn with
    | pure b => simpa using h
    | think cb => simpa [h] using IH _ h

Premises used: Computation.think, Computation.pure
-- Module: Mathlib.Data.Seq.Computation
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
⊢ LiftRel R ca cb

Tactic:
liftRel_mem_cases (LiftRelRec.lem C (@H) ca cb Hc) fun b hb =>
    (LiftRel.swap _ _ _).2 <|
      LiftRelRec.lem (swap C) (fun {_ _} h => cast (LiftRelAux.swap _ _ _ _).symm <| H h) cb ca Hc b
        hb

Premises used: Iff.mpr, Computation.LiftRelAux.swap, Function.swap, cast, Computation.liftRel_mem_cases, Computation.destruct, Computation.LiftRel.swap, Computation.LiftRelRec.lem, Eq.symm
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (↑s : Stream' (Option α)) n = s.get? n

Tactic:
rfl

Premises used: rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
f : Stream' (Option α)
hf : f.IsSeq
⊢ get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f hf) = f

Tactic:
rfl

Premises used: rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
m n : ℕ
h : m ≤ n
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
⊢ s.get? m = none → s.get? n = none

Tactic:
obtain ⟨f, al⟩ := s
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
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) m = none

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
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) m = none

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
m n : ℕ
f : Stream' (Option α)
al : f.IsSeq
m_1 : ℕ
h : 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:
fun h2 ↦ al (IH h2)

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
m n : ℕ
f : Stream' (Option α)
al : f.IsSeq
m_1 : ℕ
h : 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:
exact fun h2 ↦ al (IH h2)
-- Module: Mathlib.Data.Seq.Defs
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
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
⊢ 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:
induction h with | refl => exact id | step _ IH => exact fun h2 ↦ al (IH h2)

Premises used: id, refl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
aₙ : α
n m : ℕ
m_le_n : m ≤ n
s_nth_eq_some : s.get? n = some aₙ
⊢ s.get? n ≠ none

Tactic:
simp [s_nth_eq_some]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s t : Seq α
h : ∀ (n : ℕ), s.get? n = t.get? n
⊢ s = t

Tactic:
Subtype.ext <| funext h

Premises used: Stream'.Seq, funext, Subtype.ext
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
h : (some a :: (↑s : Stream' (Option α))) 0 = none
⊢ (some a :: (↑s : Stream' (Option α))) (HAdd.hAdd (α := ℕ) 0 1) = none

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n : ℕ
h : (some a :: (↑s : Stream' (Option α))) (n + 1) = none
⊢ (some a :: (↑s : Stream' (Option α))) (n + 1 + 1) = none

Tactic:
s.2 h

Premises used: Stream'.cons, Subtype.property
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n : ℕ
h : (some a :: (↑s : Stream' (Option α))) (n + 1) = none
⊢ (some a :: (↑s : Stream' (Option α))) (n + 1 + 1) = none

Tactic:
exact s.2 h

Premises used: Subtype.property
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
⊢ (↑(cons x s) : Stream' (Option α)) = some x :: (↑s : Stream' (Option α))

Tactic:
rfl

Premises used: Stream'.cons, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := Option α) (get? nil n) none

Tactic:
rfl

Premises used: Stream'.const, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
⊢ s.get? 0 = none ↔ s = nil

Tactic:
⟨fun h => ?_, fun h => h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
refine : ∀ (h : s.get? 0 = none), s = nil
⊢ s.get? 0 = none ↔ s = nil

Tactic:
refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.get? 0 = none
h₁ : ∀ (n : ℕ), s.get? n = get? nil n
⊢ s = nil

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.get? 0 = none
n : ℕ
⊢ s.get? n = get? nil n

Tactic:
le_stable s (Nat.zero_le _) h

Premises used: Nat.zero_le, Stream'.Seq.le_stable, Stream'.const, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.get? 0 = none
n : ℕ
⊢ s.get? n = get? nil n

Tactic:
exact le_stable s (Nat.zero_le _) h

Premises used: Nat.zero_le, Stream'.Seq.le_stable
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s : Seq α
⊢ (cons a s).get? 0 = some a

Tactic:
rfl

Premises used: Stream'.cons, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s : Seq α
n : ℕ
⊢ (cons a s).get? (n + 1) = s.get? n

Tactic:
rfl

Premises used: Stream'.Seq, Stream'.Seq.cons, Stream'.cons, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
h : cons x s = nil
⊢ False

Tactic:
simpa using congrArg (·.get? 0) h

Premises used: congrArg
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
⊢ nil ≠ cons x s

Tactic:
cons_ne_nil.symm

Premises used: Stream'.Seq.cons_ne_nil, Ne.symm
-- Module: Mathlib.Data.Seq.Defs
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
rw₃ rw₄ : some y = some y
⊢ x = y

Tactic:
rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]

Premises used: Stream'.Seq.get?_cons_zero, Option.some_inj
-- Module: Mathlib.Data.Seq.Defs
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
simp_rw₁ : (cons y t).get? (n + 1) = t.get? n
⊢ s.get? n = t.get? n

Tactic:
simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]

Premises used: Stream'.Seq.get?_cons_succ
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
⊢ Function.Injective (β := Seq α) fun (x : α) ↦ cons x s

Tactic:
cons_injective2.left _

Premises used: Stream'.Seq.cons_injective2, Function.Injective2.left
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
⊢ Function.Injective (cons x)

Tactic:
cons_injective2.right _

Premises used: Stream'.Seq.cons_injective2, Function.Injective2.right
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x x' : α
s s' : Seq α
mp : cons x s = cons x' s' → x = x' ∧ s = s'
mpr : x = x' ∧ s = s' → cons x s = cons x' s'
⊢ cons x s = cons x' s' ↔ x = x' ∧ s = s'

Tactic:
constructor
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x x' : α
s s' : Seq α
⊢ cons x s = cons x' s' → x = x' ∧ s = s'

Tactic:
apply cons_injective2

Premises used: Stream'.Seq.cons_injective2
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x x' : α
s s' : Seq α
left : x = x'
right : s = s'
⊢ cons x s = cons x' s'

Tactic:
congr
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
n' : (↑s : Stream' (Option α)).tail n = none
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
⊢ (↑s : Stream' (Option α)).tail (n + 1) = none

Tactic:
obtain ⟨f, al⟩ := s
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
n : ℕ
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:
al n'

Premises used: Stream'.get, Stream'.tail
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
n : ℕ
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:
exact al n'
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
none :
  Eq.{u + 1} (α := Option α) Option.none
    (Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> Option.none))
some :
  ∀ (val : α),
    Option.some val = Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> Option.some val)
⊢ s.get? 0 = Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0)

Tactic:
cases get? s 0

Premises used: OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
⊢ Eq.{u + 1} (α := Option α) none (Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> none))

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
val : α
⊢ some val = Functor.map (α := α × Seq α) Prod.fst ((fun (a' : α) ↦ (a', s.tail)) <$> some val)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.get? n = s.get? (n + 1)

Tactic:
rfl

Premises used: Stream'.Seq, Stream'.Seq.tail, Stream'.get, Stream'.tail, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Option (Seq1 α)) (destruct nil) none

Tactic:
rfl

Premises used: Stream'.Seq.destruct, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
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 α))) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al
⊢ 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)

Tactic:
apply congr_arg fun s => some (a, s)

Premises used: Option.some, Prod.mk, congr_arg
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
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 α))) ⋯)) :
      Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))
⊢ 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

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Defs
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 α))) ⋯)) :
      Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α))

Tactic:
dsimp [tail]

Premises used: Stream'.Seq.tail
-- Module: Mathlib.Data.Seq.Defs
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
some :
  ∀ (val : α) (f0 : s.get? 0 = Option.some val),
    Eq (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) (Option.some val)) Option.none → s = nil
⊢ Eq (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) (s.get? 0)) Option.none → s = nil

Tactic:
rcases f0 : get? s 0

Premises used: OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Eq.{u + 1} (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) none) none
⊢ s = nil

Tactic:
get?_zero_eq_none.mp f0

Premises used: Stream'.Seq.get?_zero_eq_none, Iff.mp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Eq.{u + 1} (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) none) none
⊢ s = nil

Tactic:
exact get?_zero_eq_none.mp f0

Premises used: Stream'.Seq.get?_zero_eq_none, Iff.mp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
val : α
f0 : s.get? 0 = some val
h : Eq (α := Option (Seq1 α)) (Option.map (fun (a' : α) ↦ (a', s.tail)) (some val)) none
⊢ s = nil

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
a : α
s' : Seq α
none :
  ∀ (f0 : s.get? 0 = Option.none),
    Option.map (fun (a' : α) ↦ (a', s.tail)) Option.none = Option.some (a, s') → s = cons a s'
some :
  ∀ (a' : α) (f0 : s.get? 0 = Option.some a'),
    Option.map (fun (a' : α) ↦ (a', s.tail)) (Option.some a') = Option.some (a, s') → s = cons a s'
⊢ Option.map (fun (a' : α) ↦ (a', s.tail)) (s.get? 0) = Option.some (a, s') → s = cons a s'

Tactic:
rcases f0 : get? s 0 with - | a'

Premises used: OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : Option.map (fun (a' : α) ↦ (a', s.tail)) none = some (a, s')
⊢ s = cons a s'

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = Option.some a'
h : Option.map (fun (a' : α) ↦ (a', s.tail)) (Option.some a') = Option.some (a, s')
some :
  ∀ (f : Stream' (Option α)) (al : f.IsSeq)
    (f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = Option.some a')
    (h :
      Option.map (fun (a' : α) ↦ (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al)))
          (Option.some a') =
        Option.some (a, s')),
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al = cons a s'
⊢ s = cons a s'

Tactic:
obtain ⟨f, al⟩ := s
-- Module: Mathlib.Data.Seq.Defs
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')
⊢ a' = a

Tactic:
injections _ h1 h2
-- Module: Mathlib.Data.Seq.Defs
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
⊢ tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'

Tactic:
injections _ h1 h2
-- Module: Mathlib.Data.Seq.Defs
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 = Option.some a'
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
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))
⊢ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al = cons a s'

Tactic:
rw [← h2]
-- Module: Mathlib.Data.Seq.Defs
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 = Option.some a'
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
some :
  (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α)) =
    (↑(cons a (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) : Stream' (Option α))
⊢ 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:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Defs
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 = Option.some a'
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
some : f = Option.some a :: f.tail
⊢ (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α)) =
    (↑(cons a (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) : Stream' (Option α))

Tactic:
dsimp [tail, cons]

Premises used: Stream'.Seq.tail, Stream'.Seq.cons
-- Module: Mathlib.Data.Seq.Defs
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'
⊢ get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a

Tactic:
rw [h1] at f0
-- Module: Mathlib.Data.Seq.Defs
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'
f0₁ : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a
⊢ a' = a

Tactic:
rw [h1] at f0
-- Module: Mathlib.Data.Seq.Defs
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'
f0₁ : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a
h1₁ : a' = a
⊢ tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'

Tactic:
rw [h1] at f0
-- Module: Mathlib.Data.Seq.Defs
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 = Option.some a
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
some : f = get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 :: f.tail
⊢ f = Option.some a :: f.tail

Tactic:
rw [← f0]