awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, s.append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
have nil : match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, append nil (S.join.append SS.join.join)),
  (Seq.cons (join ((x, nil), S)) (Seq.map join SS)).join.destruct with
| none, none => True
| some (a, s), some (a', s') =>
  a = a' ∧
    ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
| x, x_1 => False
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
s : Seq α
nil :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, append Seq.nil (S.join.append SS.join.join)),
    (Seq.cons (join ((x, Seq.nil), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, s.append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
have cons : ∀ (x_1 : α) (s : Seq α),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    some (x, (Seq.cons x_1 s).append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, Seq.cons x_1 s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_2 => False
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, append nil (S.join.append SS.join.join)),
    (Seq.cons (join ((x, nil), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
have simp : ∃ (s : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
  S.join.append SS.join.join = s.append SS_2.join.join ∧
    S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_2).join
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x x_1 : α
s : Seq α
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    some (x, (Seq.cons x_1 s).append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, Seq.cons x_1 s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_2 => False
have cons : ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
  Seq.cons x_1 (s.append (S.join.append SS.join.join)) = s_1.append SS_2.join.join ∧
    Seq.cons x_1 (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_2).join
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x_1 x : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    Seq.cons x (s.append (S.join.append SS.join.join)) = s_1.append SS_2.join.join ∧
      Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_2).join
have refine_1 : Seq.cons x (s.append (S.join.append SS.join.join)) = (Seq.cons x (s.append S.join)).append SS.join.join
Tactic: refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x_1 x : α
s : Seq α
refine_1 : Seq.cons x (s.append (S.join.append SS.join.join)) = (Seq.cons x (s.append S.join)).append SS.join.join
⊢ ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    Seq.cons x (s.append (S.join.append SS.join.join)) = s_1.append SS_2.join.join ∧
      Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_2).join
have refine_2 : Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) =
  (Seq.cons x (s.append S.join)).append (Seq.map join SS).join
Tactic: refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ (s : Seq α) (SS_1 : Seq (Seq1 (Seq1 α))),
    SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
have r : SS.join.join = append nil SS.join.join
Tactic: refine ⟨nil, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
r : SS.join.join = append nil SS.join.join
⊢ ∃ (s : Seq α) (SS_1 : Seq (Seq1 (Seq1 α))),
    SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
have r₁ : (Seq.map join SS).join = append nil (Seq.map join SS).join
Tactic: refine ⟨nil, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
⊢ (s.bind f).bind g = s.bind fun (x : α) ↦ (f x).bind g
have obtain : ∀ (a : α) (s : Seq α), (bind (a, s) f).bind g = bind (a, s) fun (x : α) ↦ (f x).bind g
Tactic: obtain ⟨a, s⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (bind (a, s) f).bind g = bind (a, s) fun (x : α) ↦ (f x).bind g
have simp : (join (map g (f a), Seq.map (map g) (Seq.map f s))).join =
  join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)
Tactic: simp only [bind, map_pair, map_join]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g) (Seq.map f s))).join =
    join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)
have rw : (join (map g (f a), Seq.map (map g ∘ f) s)).join =
  join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)
Tactic: rw [← map_comp]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join =
    join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)
have simp : (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)
Tactic: simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)
have rw : (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))
Tactic: rw [map_comp _ join]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))
have generalize : ∀ (SS : Seq (Seq1 (Seq1 γ))), (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)
Tactic: generalize Seq.map (map g ∘ f) s = SS
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)
have rcases : ∀ (S : Seq (Seq1 γ)) (a : γ) (s : Seq γ), (join (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)
Tactic: rcases map g (f a) with ⟨⟨a, s⟩, S⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s_1 : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
s : Seq γ
⊢ (join (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)
have nil : (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)
Tactic: induction s using recOn with | nil => ?_ | cons x s_1 => ?_
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s_1 : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
s : Seq γ
nil : (join (((a, Seq.nil), S), SS)).join = join (join ((a, Seq.nil), S), Seq.map join SS)
⊢ (join (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)
have cons : ∀ (x : γ) (s_1 : Seq γ),
  (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)
Tactic: induction s using recOn with | nil => ?_ | cons x s_1 => ?_
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
⊢ (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)
have nil : ∀ (x_1 : Seq1 γ) (s_2 : Seq (Seq1 γ)),
  (join (((a, nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, nil), Seq.cons x_1 s_2), Seq.map join SS)
Tactic: induction S using recOn with | nil => simp | cons x_1 s_2 => ?_
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)
have cons : ∀ (x_1 : Seq1 γ) (s_2 : Seq (Seq1 γ)),
  (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
Tactic: induction S using recOn with | nil => simp | cons x_1 s_2 => ?_
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, nil), Seq.cons x_1 s_2), Seq.map join SS)
have nil : ∀ (x : γ) (t : Seq γ),
  (join (((a, nil), Seq.cons (x, t) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, t) s_2), Seq.map join SS)
Tactic: obtain ⟨x, t⟩ := x_1
Cleared hypotheses: x_1
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
t : Seq γ
⊢ (join (((a, nil), Seq.cons (x, t) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, t) s_2), Seq.map join SS)
have nil : (join (((a, nil), Seq.cons (x, nil) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, nil) s_2), Seq.map join SS)
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
t : Seq γ
nil :
  (join (((a, Seq.nil), Seq.cons (x, Seq.nil) s_2), SS)).join =
    join (join ((a, Seq.nil), Seq.cons (x, Seq.nil) s_2), Seq.map join SS)
⊢ (join (((a, Seq.nil), Seq.cons (x, t) s_2), SS)).join =
    join (join ((a, Seq.nil), Seq.cons (x, t) s_2), Seq.map join SS)
have nil₁ : ∀ (x_1 : γ) (s : Seq γ),
  (join (((a, Seq.nil), Seq.cons (x, Seq.cons x_1 s) s_2), SS)).join =
    join (join ((a, Seq.nil), Seq.cons (x, Seq.cons x_1 s) s_2), Seq.map join SS)
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
have cons : ∀ (y : γ) (t : Seq γ),
  (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons (y, t) s_2), Seq.map join SS)
Tactic: obtain ⟨y, t⟩ := x_1
Cleared hypotheses: x_1
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
c : Computation α
n : ℕ
a : α
h :
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      n =
    some a
⊢ Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1) =
    some a
have zero : ∀
  (h :
    Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
        0 =
      some a),
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (HAdd.hAdd (α := ℕ) 0 1) =
    some a
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
c : Computation α
n : ℕ
a : α
h :
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      n =
    some a
zero :
  ∀
    (h :
      Stream'.cons none
          (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)) 0 =
        some a),
    Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
        (HAdd.hAdd (α := ℕ) 0 1) =
      some a
⊢ Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1) =
    some a
have succ : ∀ (n : ℕ)
  (h :
    Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
        (n + 1) =
      some a),
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1 + 1) =
    some a
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
⊢ s.destruct = Sum.inl a → s = pure a
have dsimp : Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α) →
  s = pure a
Tactic: dsimp [destruct]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
⊢ Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 with
        | none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inl a : α ⊕ Computation α) →
    s = pure a
have none : ∀ (f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = none),
  Eq.{u + 1} (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α) none with
        | none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inl a : α ⊕ Computation α) →
    s = pure a
Tactic: cases f0 : s.1 0
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a : α
none :
  ∀
    (f0 :
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = Option.none),
    Eq.{u + 1} (α := α ⊕ Computation α)
        (match (motive := Option α → α ⊕ Computation α) Option.none with
          | Option.none => Sum.inr s.tail
          | some a => Sum.inl a :
          α ⊕ Computation α)
        (Sum.inl a : α ⊕ Computation α) →
      s = pure a
⊢ Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 with
        | Option.none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inl a : α ⊕ Computation α) →
    s = pure a
have some : ∀ (val : α)
  (f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val),
  Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α) some val with
        | Option.none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inl a : α ⊕ Computation α) →
    s = pure a
Tactic: cases f0 : s.1 0
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
⊢ s = pure a
have some : s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
  (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
have some : ∀ (n : ℕ),
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0 =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0
have h' : val = a
Tactic: injection h with h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h' : val = a
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0 =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0
have some : ∀ (f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some a)
  (h' : val = a),
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0 =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0
Tactic: rwa [h'] at f0
Cleared hypotheses: f0, h'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
n : ℕ
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
have some : s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0 =
  (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) 0
Tactic: induction n with
    | zero => injection h with h'; rwa [h'] at f0
    | succ n IH => exact s.2 IH
Cleared hypotheses: n