awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s t u s1 s2 : Seq α
h : ∃ (s : Seq α) (t : Seq α) (u : Seq α), s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (t : Seq α) (u : Seq α), s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    s1.destruct s2.destruct

Tactic:
exact
      match s1, s2, h with
      | _, _, ⟨s, t, u, rfl, rfl⟩ => by
        cases s <;> simp
        case nil =>
          cases t <;> simp
          case nil =>
            cases u <;> simp
            case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
          case cons _ t => refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
        case cons _ s => exact ⟨s, t, u, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s t u : Seq α
⊢ ∃ (s_1 : Seq α) (t_1 : Seq α) (u_1 : Seq α),
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
⟨s, t, u, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s t u : Seq α
⊢ ∃ (s_1 : Seq α) (t_1 : Seq α) (u_1 : Seq α),
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
exact ⟨s, t, u, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
⊢ a ∈ s₁.append s₂

Tactic:
have := h
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h this : a ∈ s₁.append s₂
revert : ∀ (this : a ∈ s₁.append s₂), a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
revert this
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
generalize : ∀ (ss : Seq α) (e : s₁.append s₂ = ss) (this : a ∈ ss), a ∈ s₁ ∨ a ∈ s₂
⊢ ∀ (this : a ∈ s₁.append s₂), a ∈ s₁ ∨ a ∈ s₂

Tactic:
generalize e : append s₁ s₂ = ss

Premises used: Stream'.Seq.append
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h_1 : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
revert : ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = ss), a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
revert s₁
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
apply :
  ∀ (b : α) (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = cons b s'), a ∈ s₁ ∨ a ∈ s₂
⊢ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = ss), a ∈ s₁ ∨ a ∈ s₂

Tactic:
apply mem_rec_on h _

Premises used: Stream'.Seq.mem_rec_on
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
m : a ∈ append Seq.nil s₂
nil : append Seq.nil s₂ = cons b s' → Membership.mem (γ := Seq α) Seq.nil a ∨ a ∈ s₂
⊢ ∀ (e : append Seq.nil s₂ = cons b s'), Membership.mem (γ := Seq α) Seq.nil a ∨ a ∈ s₂

Tactic:
_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
m : a ∈ append Seq.nil s₂
e : append Seq.nil s₂ = cons b s'
nil : a ∈ s₂
⊢ Membership.mem (γ := Seq α) Seq.nil a ∨ a ∈ s₂

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
m : a ∈ append nil s₂
e : append nil s₂ = cons b s'
⊢ a ∈ s₂

Tactic:
simpa using m
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
⊢ ((cons c t₁).append s₂).destruct = (cons b s').destruct

Tactic:
have this := congr_arg destruct e
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a = c ∨ a ∈ t₁.append s₂

Tactic:
simpa using m
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (Seq.cons c t₁).append s₂
e : (Seq.cons c t₁).append s₂ = Seq.cons b s'
this : ((Seq.cons c t₁).append s₂).destruct = (Seq.cons b s').destruct
cons : ∀ (e' : a = c), a ∈ Seq.cons c t₁ ∨ a ∈ s₂
cons₁ : ∀ (m : a ∈ t₁.append s₂), a ∈ Seq.cons c t₁ ∨ a ∈ s₂
⊢ a ∈ Seq.cons c t₁ ∨ a ∈ s₂

Tactic:
rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (Seq.cons c t₁).append s₂
e : (Seq.cons c t₁).append s₂ = Seq.cons b s'
this : ((Seq.cons c t₁).append s₂).destruct = (Seq.cons b s').destruct
e' : a = c
cons : c ∈ Seq.cons c t₁ ∨ c ∈ s₂
⊢ a ∈ Seq.cons c t₁ ∨ a ∈ s₂

Tactic:
rw [e']
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂

Tactic:
Or.inl (mem_cons _ _)

Premises used: Stream'.Seq.mem_cons, Or.inl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂

Tactic:
exact Or.inl (mem_cons _ _)

Premises used: Stream'.Seq.mem_cons, Or.inl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m_1 : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ c = b ∧ t₁.append s₂ = s'

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m_1 : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ c = b

Tactic:
obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m_1 : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
⊢ t₁.append s₂ = s'

Tactic:
obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m_1 : a ∈ (Seq.cons c t₁).append s₂
e : (Seq.cons c t₁).append s₂ = Seq.cons b s'
this : ((Seq.cons c t₁).append s₂).destruct = (Seq.cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
cons : ∀ (e' : a = b), a ∈ Seq.cons c t₁ ∨ a ∈ s₂
cons₁ :
  ∀ (IH : ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂), a ∈ Seq.cons c t₁ ∨ a ∈ s₂
⊢ a ∈ Seq.cons c t₁ ∨ a ∈ s₂

Tactic:
rcases o with e' | IH
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m_1 : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
simp [i1, e']
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m_1 : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
Or.imp_left (mem_cons_of_mem _) (IH m i2)

Premises used: Or.imp_left, Stream'.Seq.mem_cons_of_mem
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m_1 : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
exact Or.imp_left (mem_cons_of_mem _) (IH m i2)

Premises used: Or.imp_left, Stream'.Seq.mem_cons_of_mem
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = s'), a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
nil :
  ∀ (h : a ∈ append Seq.nil s₂) (e : append Seq.nil s₂ = Seq.cons b s'), Membership.mem (γ := Seq α) Seq.nil a ∨ a ∈ s₂
cons :
  ∀ (c : α) (t₁ : Seq α) (h : a ∈ (Seq.cons c t₁).append s₂) (e : (Seq.cons c t₁).append s₂ = Seq.cons b s'),
    a ∈ Seq.cons c t₁ ∨ a ∈ s₂
⊢ ∀ (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = Seq.cons b s'), a ∈ s₁ ∨ a ∈ s₂

Tactic:
cases s₁ with
  | nil =>
    intro m _
    apply Or.inr
    simpa using m
  | cons c t₁ =>
    intro m e
    have this := congr_arg destruct e
    rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
    · rw [e']
      exact Or.inl (mem_cons _ _)
    · obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
      rcases o with e' | IH
      · simp [i1, e']
      · exact Or.imp_left (mem_cons_of_mem _) (IH m i2)

Premises used: Stream'.Seq.nil, Stream'.Seq.cons, Stream'.Seq.mem_cons, Or.inl, Or.inr
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
apply : ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂
⊢ a ∈ s₁.append s₂

Tactic:
apply mem_rec_on h

Premises used: Stream'.Seq.mem_rec_on
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b : α
s' : Seq α
h_1 : a = b ∨ a ∈ s'.append s₂
⊢ a ∈ (cons b s').append s₂

Tactic:
simp [*]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l l' : List α
nil : (↑([] ++ l') : Seq α) = append (↑[] : Seq α) (↑l' : Seq α)
cons :
  ∀ (head : α) (tail : List α),
    (↑(tail ++ l') : Seq α) = (↑tail : Seq α).append (↑l' : Seq α) →
      (↑(head :: tail ++ l') : Seq α) = (↑(head :: tail) : Seq α).append (↑l' : Seq α)
⊢ (↑(l ++ l') : Seq α) = (↑l : Seq α).append (↑l' : Seq α)

Tactic:
induction l
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l' : List α
⊢ (↑([] ++ l') : Seq α) = append (↑[] : Seq α) (↑l' : Seq α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l' : List α
head : α
tail : List α
tail_ih : (↑(tail ++ l') : Seq α) = (↑tail : Seq α).append (↑l' : Seq α)
⊢ (↑(head :: tail ++ l') : Seq α) = (↑(head :: tail) : Seq α).append (↑l' : Seq α)

Tactic:
simp [*]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l : List α
s : Stream' α
nil : (↑([] ++ₛ s) : Seq α) = append (↑[] : Seq α) (↑s : Seq α)
cons :
  ∀ (head : α) (tail : List α),
    (↑(tail ++ₛ s) : Seq α) = (↑tail : Seq α).append (↑s : Seq α) →
      (↑(head :: tail ++ₛ s) : Seq α) = (↑(head :: tail) : Seq α).append (↑s : Seq α)
⊢ (↑(l ++ₛ s) : Seq α) = (↑l : Seq α).append (↑s : Seq α)

Tactic:
induction l
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Stream' α
⊢ (↑([] ++ₛ s) : Seq α) = append (↑[] : Seq α) (↑s : Seq α)

Tactic:
simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

Premises used: Stream'.cons_append_stream, Stream'.nil_append_stream
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Stream' α
head : α
tail : List α
tail_ih : (↑(tail ++ₛ s) : Seq α) = (↑tail : Seq α).append (↑s : Seq α)
⊢ (↑(head :: tail ++ₛ s) : Seq α) = (↑(head :: tail) : Seq α).append (↑s : Seq α)

Tactic:
simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

Premises used: Stream'.cons_append_stream, Stream'.nil_append_stream
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
⊢ map f nil = nil

Tactic:
rfl

Premises used: Stream'.Seq.map, Stream'.Seq.nil, Stream'.map, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
a₁ :
  (↑(map f (cons a (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option β)) =
    (↑(cons (f a) (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option β))
⊢ map f (cons a (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)) =
    cons (f a) (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
a₁ : Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
⊢ (↑(map f (cons a (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option β)) =
    (↑(cons (f a) (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option β))

Tactic:
dsimp [cons, map]

Premises used: Stream'.Seq.map, Stream'.Seq.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
a₁ : Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s

Tactic:
rw [Stream'.map_cons]

Premises used: Stream'.map_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
a :
  (↑(map id (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)) : Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al) : Stream' (Option α))
⊢ map id (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
a : Stream'.map (Option.map id) s = s
⊢ (↑(map id (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)) : Stream' (Option α)) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al) : Stream' (Option α))

Tactic:
dsimp [map]

Premises used: Stream'.Seq.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
a : Stream'.map id s = s
a₁ a₂ : s = s
⊢ Stream'.map (Option.map id) s = s

Tactic:
rw [Option.map_id, Stream'.map_id]

Premises used: Stream'.map_id, Option.map_id
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
a :
  (↑(map f (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option β)) =
    (↑(map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)).tail : Stream' (Option β))
⊢ map f (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)) =
    (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)).tail

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
⊢ (↑(map f (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option β)) =
    (↑(map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)).tail : Stream' (Option β))

Tactic:
dsimp [tail, map]

Premises used: Stream'.Seq.map, Stream'.Seq.tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a :
  (↑(map (g ∘ f) (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)) : Stream' (Option γ)) =
    (↑(map g (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option γ))
⊢ map (g ∘ f) (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al) =
    map g (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a : Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s
⊢ (↑(map (g ∘ f) (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)) : Stream' (Option γ)) =
    (↑(map g (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al))) : Stream' (Option γ))

Tactic:
dsimp [map]

Premises used: Stream'.Seq.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a : Option.map (g ∘ f) = Option.map g ∘ Option.map f
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s

Tactic:
apply congr_arg fun f : _ → Option γ => Stream'.map f s

Premises used: congr_arg, Stream'.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a : ∀ (a : γ), Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a
a₁ : ∀ (val : α) (a : γ), Option.map (g ∘ f) (some val) = some a ↔ (Option.map g ∘ Option.map f) (some val) = some a
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Tactic:
ext ⟨⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a : γ
⊢ Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
val : α
a : γ
⊢ Option.map (g ∘ f) (some val) = some a ↔ (Option.map g ∘ Option.map f) (some val) = some a

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Seq α
n : ℕ
⊢ (map f s).TerminatedAt n ↔ s.TerminatedAt n

Tactic:
simp [TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Seq α
⊢ (map f s).Terminates ↔ s.Terminates

Tactic:
simp [Terminates]

Premises used: Stream'.Seq.Terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
e_p : (map f s).TerminatedAt = s.TerminatedAt
⊢ Nat.find (p := (map f s).TerminatedAt) h = s.length ⋯

Tactic:
congr
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
e_p : ∀ (x : ℕ), (map f s).TerminatedAt x ↔ s.TerminatedAt x
⊢ (map f s).TerminatedAt = s.TerminatedAt

Tactic:
ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
x : ℕ
⊢ (map f s).TerminatedAt x ↔ s.TerminatedAt x

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
pos : ∀ (h : (map f s).Terminates), (map f s).length' = s.length'
neg : ∀ (h : ¬(map f s).Terminates), (map f s).length' = s.length'
⊢ (map f s).length' = s.length'

Tactic:
by_cases h : (s.map f).Terminates

Premises used: Stream'.Seq.Terminates, Stream'.Seq.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).Terminates

Tactic:
have h' := h
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
⊢ ¬(map f s).Terminates

Tactic:
have h' := h
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h h' : (map f s).Terminates
⊢ s.Terminates

Tactic:
rw [terminates_map_iff] at h'

Premises used: Stream'.Seq.terminates_map_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h h' : ¬(map f s).Terminates
⊢ ¬s.Terminates

Tactic:
rw [terminates_map_iff] at h'

Premises used: Stream'.Seq.terminates_map_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
pos : (↑((map f s).length h) : ℕ∞) = s.length'
pos₁ : Eq (α := ℕ∞) (↑((map f s).length h) : ℕ∞) (↑(s.length h') : ℕ∞)
pos₂ pos₃ : Eq (α := ℕ∞) (↑(s.length ⋯) : ℕ∞) (↑(s.length h') : ℕ∞)
⊢ (map f s).length' = s.length'

Tactic:
rw [length'_of_terminates h, length'_of_terminates h', length_map h]

Premises used: Stream'.Seq.length'_of_terminates, Stream'.Seq.length_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
neg : ⊤ = s.length'
neg₁ neg₂ : Eq (α := ℕ∞) ⊤ ⊤
⊢ (map f s).length' = s.length'

Tactic:
rw [length'_of_not_terminates h, length'_of_not_terminates h']

Premises used: Stream'.Seq.length'_of_not_terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al)
let :
  ∀ (o : Option α) (om : o ∈ g) (oe : Option.map f o = some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b

Tactic:
let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al)
o : Option α
om : o ∈ g
oe : Option.map f o = Option.some b
none :
  ∀ (om : Option.none ∈ g) (oe : Option.map f Option.none = Option.some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
some :
  ∀ (a : α) (om : Option.some a ∈ g) (oe : Option.map f (Option.some a) = Option.some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b

Tactic:
rcases o with - | a
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al)
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b

Tactic:
injection oe
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al)
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ f a = b

Tactic:
injection oe with h'