awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s t_1 u_1 s1 s2 : Seq α
h : ∃ (s : Seq α) (t : Seq α) (u : Seq α), s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
x : α
t : Seq α
refine_1 : t.append u = (append nil t).append u
⊢ ∃ (s : Seq α) (t_2 : Seq α) (u_2 : Seq α),
    t.append u = (s.append t_2).append u_2 ∧ t.append u = s.append (t_2.append u_2)
have refine_2 : t.append u = append nil (t.append u)
Tactic: refine ⟨nil, t, u, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h this : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂
have revert : ∀ (this : a ∈ s₁.append s₂), a ∈ s₁ ∨ a ∈ s₂
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
⊢ ∀ (this : a ∈ s₁.append s₂), a ∈ s₁ ∨ a ∈ s₂
have generalize : ∀ (ss : Seq α) (e : s₁.append s₂ = ss) (this : a ∈ ss), a ∈ s₁ ∨ a ∈ s₂
Tactic: generalize e : append s₁ s₂ = ss
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h_1 : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂
have revert : ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = ss), a ∈ s₁ ∨ a ∈ s₂
Tactic: revert s₁
Cleared hypotheses: s₁, h_1, e
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α} (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = ss), a ∈ s₁ ∨ a ∈ s₂
have 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₂
Tactic: apply mem_rec_on h _
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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'
⊢ Membership.mem (γ := Seq α) nil a ∨ a ∈ s₂
have nil : a ∈ s₂
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
have this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
Tactic: have this := congr_arg destruct e
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 ∈ cons c t₁ ∨ a ∈ s₂
have cons : ∀ (e' : a = c), a ∈ cons c t₁ ∨ a ∈ s₂
Tactic: rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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₂
⊢ a ∈ Seq.cons c t₁ ∨ a ∈ s₂
have cons₁ : ∀ (m : a ∈ t₁.append s₂), a ∈ Seq.cons c t₁ ∨ a ∈ s₂
Tactic: rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
have cons : c ∈ cons c t₁ ∨ c ∈ s₂
Tactic: rw [e']
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
have i1 : c = b
Tactic: obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
have i2 : t₁.append s₂ = s'
Tactic: obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
i2 : t₁.append s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
have cons : ∀ (e' : a = b), a ∈ cons c t₁ ∨ a ∈ s₂
Tactic: rcases o with e' | IH
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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₂
⊢ a ∈ Seq.cons c t₁ ∨ a ∈ s₂
have 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₂
Tactic: rcases o with e' | IH
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 α
⊢ ∀ (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = cons b s'), a ∈ s₁ ∨ a ∈ s₂
have nil : ∀ (h : a ∈ append nil s₂) (e : append nil s₂ = cons b s'), Membership.mem (γ := Seq α) nil a ∨ 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)
Cleared hypotheses: s₁
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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₂ = cons b s'), Membership.mem (γ := Seq α) Seq.nil a ∨ a ∈ s₂
⊢ ∀ (h : a ∈ s₁.append s₂) (e : s₁.append s₂ = cons b s'), a ∈ s₁ ∨ a ∈ s₂
have cons : ∀ (c : α) (t₁ : Seq α) (h : a ∈ (cons c t₁).append s₂) (e : (cons c t₁).append s₂ = cons b s'), a ∈ cons c t₁ ∨ 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)
Cleared hypotheses: s₁
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ a ∈ s₁.append s₂
have apply : ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂
Tactic: apply mem_rec_on h
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
l l' : List α
⊢ (↑(l ++ l') : Seq α) = (↑l : Seq α).append (↑l' : Seq α)
have nil : (↑([] ++ l') : Seq α) = append (↑[] : Seq α) (↑l' : Seq α)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
l l' : List α
nil : (↑([] ++ l') : Seq α) = append (↑[] : Seq α) (↑l' : Seq α)
⊢ (↑(l ++ l') : Seq α) = (↑l : Seq α).append (↑l' : Seq α)
have cons : ∀ (head : α) (tail : List α),
  (↑(tail ++ l') : Seq α) = (↑tail : Seq α).append (↑l' : Seq α) →
    (↑(head :: tail ++ l') : Seq α) = (↑(head :: tail) : Seq α).append (↑l' : Seq α)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
l : List α
s : Stream' α
⊢ (↑(l ++ₛ s) : Seq α) = (↑l : Seq α).append (↑s : Seq α)
have nil : (↑([] ++ₛ s) : Seq α) = append (↑[] : Seq α) (↑s : Seq α)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
l : List α
s : Stream' α
nil : (↑([] ++ₛ s) : Seq α) = append (↑[] : Seq α) (↑s : Seq α)
⊢ (↑(l ++ₛ s) : Seq α) = (↑l : Seq α).append (↑s : Seq α)
have cons : ∀ (head : α) (tail : List α),
  (↑(tail ++ₛ s) : Seq α) = (↑tail : Seq α).append (↑s : Seq α) →
    (↑(head :: tail ++ₛ s) : Seq α) = (↑(head :: tail) : Seq α).append (↑s : Seq α)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ 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))
have 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 β))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ (↑(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 β))
have a₁ : Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
Tactic: dsimp [cons, map]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
have a₁ : Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
Tactic: rw [Stream'.map_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ map id (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al
have 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 α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ (↑(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 α))
have a : Stream'.map (Option.map id) s = s
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map id) s = s
have a : Stream'.map id s = s
Tactic: rw [Option.map_id, Stream'.map_id]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
a : Stream'.map id s = s
⊢ Stream'.map (Option.map id) s = s
have a₁ : s = s
Tactic: rw [Option.map_id, Stream'.map_id]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)) =
    (map f (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) s al)).tail
have 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 β))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ 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))
have 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 γ))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ (↑(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 γ))
have a : Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s
have a : Option.map (g ∘ f) = Option.map g ∘ Option.map f
Tactic: apply congr_arg fun f : _ → Option γ => Stream'.map f s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
have a : ∀ (a : γ), Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
have a₁ : ∀ (val : α) (a : γ), Option.map (g ∘ f) (some val) = some a ↔ (Option.map g ∘ Option.map f) (some val) = some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find (p := (map f s).TerminatedAt) h = s.length ⋯
have e_p : (map f s).TerminatedAt = s.TerminatedAt
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).TerminatedAt = s.TerminatedAt
have e_p : ∀ (x : ℕ), (map f s).TerminatedAt x ↔ s.TerminatedAt x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
⊢ (map f s).length' = s.length'
have pos : ∀ (h : (map f s).Terminates), (map f s).length' = s.length'
Tactic: by_cases h : (s.map f).Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
pos : ∀ (h : (map f s).Terminates), (map f s).length' = s.length'
⊢ (map f s).length' = s.length'
have neg : ∀ (h : ¬(map f s).Terminates), (map f s).length' = s.length'
Tactic: by_cases h : (s.map f).Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h h' : (map f s).Terminates
⊢ (map f s).length' = s.length'
have h'₁ : s.Terminates
Tactic: rw [terminates_map_iff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h h' : ¬(map f s).Terminates
⊢ (map f s).length' = s.length'
have h'₁ : ¬s.Terminates
Tactic: rw [terminates_map_iff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
⊢ (map f s).length' = s.length'
have pos : (↑((map f s).length h) : ℕ∞) = s.length'
Tactic: rw [length'_of_terminates h, length'_of_terminates h', length_map h]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
pos : (↑((map f s).length h) : ℕ∞) = s.length'
⊢ (map f s).length' = s.length'
have pos₁ : Eq (α := ℕ∞) (↑((map f s).length h) : ℕ∞) (↑(s.length h') : ℕ∞)
Tactic: rw [length'_of_terminates h, length'_of_terminates h', length_map h]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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') : ℕ∞)
⊢ (map f s).length' = s.length'
have pos₂ : Eq (α := ℕ∞) (↑(s.length sorry) : ℕ∞) (↑(s.length h') : ℕ∞)
Tactic: rw [length'_of_terminates h, length'_of_terminates h', length_map h]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ (map f s).length' = s.length'
have neg : ⊤ = s.length'
Tactic: rw [length'_of_not_terminates h, length'_of_not_terminates h']
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
neg : ⊤ = s.length'
⊢ (map f s).length' = s.length'
have neg₁ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [length'_of_not_terminates h, length'_of_not_terminates h']
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
have 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
Tactic: let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 = some b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
have none : ∀ (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: rcases o with - | a
Cleared hypotheses: o, om, oe
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 = some b
none :
  ∀ (om : Option.none ∈ g) (oe : Option.map f Option.none = 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
have some : ∀ (a : α) (om : some a ∈ g) (oe : Option.map f (some a) = some b),
  ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
Tactic: rcases o with - | a
Cleared hypotheses: o, om, oe
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) g al, f a = b
have h' : f a = b
Tactic: injection oe with h'
Cleared hypotheses: oe
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ map f (s.append t) = (map f s).append (map f t)
have eq_of_bisim : IsBisimulation.{v} (α := β) fun (s1 s2 : Seq β) ↦
  ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
Tactic: apply
    eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
      ⟨s, t, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
s t : Seq α
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (s.append t)).destruct ((map f s).append (map f t)).destruct
have nil : BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
  (map f (append nil t)).destruct ((map f nil).append (map f t)).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
s t : Seq α
nil :
  BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (append Seq.nil t)).destruct ((map f Seq.nil).append (map f t)).destruct
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (s.append t)).destruct ((map f s).append (map f t)).destruct
have cons : ∀ (x : α) (s : Seq α),
  BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f ((cons x s).append t)).destruct ((map f (cons x s)).append (map f t)).destruct
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (append nil t)).destruct ((map f nil).append (map f t)).destruct
have simp : match (motive := Option (Seq1 β) → Option (Seq1 β) → Prop) (map f t).destruct, (map f t).destruct with
| none, none => True
| some (a, s), some (a', s') =>
  a = a' ∧ ∃ (s_1 : Seq α) (t : Seq α), s = map f (s_1.append t) ∧ s' = (map f s_1).append (map f t)
| x, x_1 => False
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s t_1 : Seq α
s1 s2 : Seq β
h : ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
t : Seq α
x : α
s_1 : Seq α
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α) (t : Seq α), s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f ((cons x s_1).append t)).destruct ((map f (cons x s_1)).append (map f t)).destruct
have cons : ∃ (s : Seq α) (t_2 : Seq α),
  map f (s_1.append t) = map f (s.append t_2) ∧ (map f s_1).append (map f t) = (map f s).append (map f t_2)
Tactic: simp