awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this_1 this : s.Terminates
rw : s.length = n
rw₁ rw₂ : n = n
⊢ m = n

Tactic:
rw [← h1.length, h2.length]

Premises used: Computation.Results.length
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
h : a ∈ s
⊢ ∃ (n : ℕ), s.Results a n

Tactic:
haveI := terminates_of_mem h
  ⟨_, results_of_terminates' s h⟩

Premises used: Computation.length, Exists.intro, Computation.results_of_terminates'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ (pure a).get = a

Tactic:
get_eq_of_mem _ ⟨0, rfl⟩

Premises used: Computation.get_eq_of_mem, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ (pure a).length = 0

Tactic:
let h := Computation.ret_terminates a
  Nat.eq_zero_of_le_zero <| Nat.find_min' ((terminates_def (pure a)).1 h) rfl

Premises used: Nat.find_min', Computation.pure, Iff.mp, Computation.terminates_def, Computation.ret_terminates, rfl, Nat.eq_zero_of_le_zero
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ (pure a).Results a 0

Tactic:
⟨ret_mem a, length_pure _⟩

Premises used: Computation.length_pure, Computation.Results, Exists.intro, Computation.ret_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
a : s.think.length ≤ s.length + 1
a₁ : s.length + 1 ≤ s.think.length
⊢ s.think.length = s.length + 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

Tactic:
Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))

Premises used: Computation.length, Nat.find_min', Iff.mp, Computation.terminates_def, Nat.find_spec
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

Tactic:
exact Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))

Premises used: Nat.find_min'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        s.think.length).isSome =
    true

Tactic:
have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
      Nat.find_spec ((terminates_def _).1 s.think_terminates)
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        s.think.length).isSome =
    true
a :
  ∀
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            s.think.length).isSome =
        true),
    s.length + 1 ≤ s.think.length
⊢ s.length + 1 ≤ s.think.length

Tactic:
revert this
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
a :
  ∀
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            0).isSome =
        true),
    s.length + 1 ≤ 0
a₁ :
  ∀ (n : ℕ)
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (n + 1)).isSome =
        true),
    s.length + 1 ≤ n + 1
⊢ ∀
    (this :
      (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            s.think.length).isSome =
        true),
    s.length + 1 ≤ s.think.length

Tactic:
rcases length (think s) with - | n

Premises used: Computation.think, Computation.length
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0).isSome =
    true
⊢ s.length + 1 ≤ 0

Tactic:
simp [think, Stream'.cons] at this

Premises used: Computation.think, Stream'.cons
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (n + 1)).isSome =
    true
a : s.length ≤ n
⊢ s.length + 1 ≤ n + 1

Tactic:
apply Nat.succ_le_succ

Premises used: Nat.succ_le_succ
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (n + 1)).isSome =
    true
a : (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n).isSome = true
⊢ s.length ≤ n

Tactic:
apply Nat.find_min'

Premises used: Nat.find_min'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this :
  (s.think.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (n + 1)).isSome =
    true
⊢ (s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) n).isSome = true

Tactic:
apply this
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
rw : s.length + 1 = n + 1
rw₁ rw₂ : n + 1 = n + 1
⊢ s.think.length = n + 1

Tactic:
rw [length_think, h.length]

Premises used: Computation.Results.length, Computation.length_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
⊢ s.Terminates

Tactic:
haveI := of_think_terminates h.terminates
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this : s.Terminates
⊢ s.Results a s.length

Tactic:
have := results_of_terminates' _ (of_think_mem h.mem)
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this_1 : s.Terminates
this : s.Results a s.length
⊢ ∃ (m : ℕ), s.Results a m ∧ n = m + 1

Tactic:
⟨_, this, Results.len_unique h (results_think this)⟩

Premises used: Computation.Results.len_unique, Computation.results_think, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this_1 : s.Terminates
this : s.Results a s.length
⊢ ∃ (m : ℕ), s.Results a m ∧ n = m + 1

Tactic:
exact ⟨_, this, Results.len_unique h (results_think this)⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
let : ∀ (n' : ℕ) (r : s.Results a n') (e : n + 1 = n' + 1), s.Results a n
⊢ s.Results a n

Tactic:
let ⟨n', r, e⟩ := of_results_think h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
e : n + 1 = n' + 1
⊢ n = n'

Tactic:
injection e with h'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
rwa rwa₁ rwa₂ rwa₃ : s.Results a n'
⊢ s.Results a n

Tactic:
rwa [h']
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
⊢ ((pure a).thinkN n).Results a (0 + n)

Tactic:
have := results_thinkN n (results_pure a)
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : ((pure a).thinkN n).Results a n), ((pure a).thinkN n).Results a n
⊢ ((pure a).thinkN n).Results a n

Tactic:
rwa [Nat.zero_add] at this

Premises used: Nat.zero_add
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
_h : s.Terminates
n : ℕ
⊢ (s.thinkN n).length = s.length + n

Tactic:
(results_thinkN n (results_of_terminates _)).length

Premises used: Computation.Results.length, Computation.results_of_terminates, Computation.results_thinkN
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
zero : ∀ {s : Computation α} (h : s.Results a 0), s = (pure a).thinkN 0
succ :
  ∀ (n : ℕ) (IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n) {s : Computation α}
    (h : s.Results a (n + 1)), s = (pure a).thinkN (n + 1)
⊢ s = (pure a).thinkN n

Tactic:
induction n generalizing s with | zero | succ n IH
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
s : Computation α
h : s.Results a 0
zero : ∀ (a' : α) (h : (pure a').Results a 0), pure a' = (pure a).thinkN 0
zero₁ : ∀ (s : Computation α) (h : s.think.Results a 0), s.think = (pure a).thinkN 0
⊢ s = (pure a).thinkN 0

Tactic:
induction s using recOn with | pure a' | think s

Premises used: Computation.think, Computation.pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
s : Computation α
h : s.Results a (n + 1)
succ : ∀ (a' : α) (h : (pure a').Results a (n + 1)), pure a' = (pure a).thinkN (n + 1)
succ₁ : ∀ (s : Computation α) (h : s.think.Results a (n + 1)), s.think = (pure a).thinkN (n + 1)
⊢ s = (pure a).thinkN (n + 1)

Tactic:
induction s using recOn with | pure a' | think s

Premises used: Computation.think, Computation.pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a a' : α
h : (pure a').Results a 0
zero : pure a = (pure a).thinkN 0
⊢ pure a' = (pure a).thinkN 0

Tactic:
rw [← eq_of_pure_mem h.mem]

Premises used: Computation.Results.mem, Computation.eq_of_pure_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a = (pure a).thinkN 0

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
zero : ∀ (n : ℕ) (h : s.Results a n ∧ 0 = n + 1), s.think = (pure a).thinkN 0
⊢ s.think = (pure a).thinkN 0

Tactic:
obtain ⟨n, h⟩ := of_results_think h

Premises used: Computation.of_results_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
s : Computation α
h_1 : s.think.Results a 0
n : ℕ
h : s.Results a n ∧ 0 = n + 1
⊢ s.Results a n

Tactic:
cases h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
s : Computation α
h_1 : s.think.Results a 0
n : ℕ
h : s.Results a n ∧ 0 = n + 1
left : s.Results a n
⊢ 0 = n + 1

Tactic:
cases h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
n : ℕ
left : s.Results a n
right : 0 = n + 1
⊢ s.think = (pure a).thinkN 0

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
a' : α
h : (pure a').Results a (n + 1)
⊢ n + 1 = 0

Tactic:
have := h.len_unique (results_pure _)
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
a' : α
h : (pure a').Results a (n + 1)
this : n + 1 = 0
⊢ pure a' = (pure a).thinkN (n + 1)

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
succ : ((pure a).thinkN n).think = (pure a).thinkN (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)

Tactic:
rw [IH (results_think_iff.1 h)]

Premises used: Iff.mp, Computation.results_think_iff
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α} (h : s.Results a n), s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ ((pure a).thinkN n).think = (pure a).thinkN (n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
_h : s.Terminates
⊢ s = (pure s.get).thinkN s.length

Tactic:
eq_thinkN (results_of_terminates _)

Premises used: Computation.results_of_terminates, Computation.eq_thinkN
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
haveI : (T : s.Terminates) → C s
⊢ C s

Tactic:
haveI T := terminates_of_mem M
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
rw : C ((pure a).thinkN s.length)
⊢ C s

Tactic:
rw [eq_thinkN' s, get_eq_of_mem s M]

Premises used: Computation.eq_thinkN', Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
generalize : (n : ℕ) → C ((pure a).thinkN n)
⊢ C ((pure a).thinkN s.length)

Tactic:
generalize length s = n

Premises used: Computation.length
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure a).thinkN 0)

Tactic:
exact h1
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
n : ℕ
IH : C ((pure a).thinkN n)
⊢ C ((pure a).thinkN (n + 1))

Tactic:
exact h2 _ IH
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
n : ℕ
zero : C ((pure a).thinkN 0)
succ : (n : ℕ) → (IH : C ((pure a).thinkN n)) → C ((pure a).thinkN (n + 1))
⊢ C ((pure a).thinkN n)

Tactic:
induction n with | zero => exact h1 | succ n IH => exact h2 _ IH
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
dsimp :
  Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s n) = some b →
    Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b
⊢ Stream'.map (fun (o : Option α) ↦ Option.casesOn (motive := fun (x : Option α) ↦ Option β) o none (some ∘ f)) s n =
      some b →
    Stream'.map (fun (o : Option α) ↦ Option.casesOn (motive := fun (x : Option α) ↦ Option β) o none (some ∘ f)) s
        (n + 1) =
      some b

Tactic:
dsimp [Stream'.map, Stream'.get]

Premises used: Stream'.get, Stream'.map
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = Option.some a → s (n + 1) = Option.some a
n : ℕ
b : β
none :
  ∀ (e : s n = Option.none),
    Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ Option.some (f val)) Option.none =
        Option.some b →
      Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ Option.some (f val))
          (s (n + 1)) =
        Option.some b
some :
  ∀ (a : α) (e : s n = Option.some a),
    Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ Option.some (f val))
          (Option.some a) =
        Option.some b →
      Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ Option.some (f val))
          (s (n + 1)) =
        Option.some b
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ Option.some (f val)) (s n) =
      Option.some b →
    Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ Option.some (f val)) (s (n + 1)) =
      Option.some b

Tactic:
rcases e : s n with - | a
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
e : s n = none
h : Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) none = some b
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = Option.some a → s (n + 1) = Option.some a
n : ℕ
b : β
a : α
e : s n = Option.some a
h some :
  Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ Option.some (f val)) (Option.some a) =
    Option.some b
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ Option.some (f val)) (s (n + 1)) =
    Option.some b

Tactic:
rw [al e]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (some a) = some b
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (some a) = some b

Tactic:
h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (some a) = some b
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (some a) = some b

Tactic:
exact h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α β : Type u
c : Computation α
f : α → Computation β
⊢ c >>= f = c.bind f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ map f (pure a) = pure (f a)

Tactic:
rfl

Premises used: Computation.map, Stream'.map, Computation.pure, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a :
  (map f
          (think
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al))).val
      (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a) =
    (map f
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al)).think.val
      (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a)
⊢ map f
      (think
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s al)) =
    (map f
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
          al)).think

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a :
  Eq.{v + 1} (α := Stream' (Option β))
    (Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
      (Stream'.cons none s))
    (Stream'.cons none
      (Stream'.map
        (fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        s))
⊢ (map f
          (think
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al))).val
      (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a) =
    (map f
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al)).think.val
      (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a)

Tactic:
dsimp [think, map]

Premises used: Computation.think, Computation.map
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a a₁ :
  Eq.{v + 1} (α := Stream' (Option β))
    (Stream'.cons (Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) none)
        (Stream'.map
          (fun (o : Option α) ↦
            Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
          s) :
      Stream' (Option β))
    (Stream'.cons none
        (Stream'.map
          (fun (o : Option α) ↦
            Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
          s) :
      Stream' (Option β))
⊢ Eq.{v + 1} (α := Stream' (Option β))
    (Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
      (Stream'.cons none s))
    (Stream'.cons none
      (Stream'.map
        (fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        s))

Tactic:
rw [Stream'.map_cons]

Premises used: Stream'.map_cons
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
pure : ∀ (a : α), (map f (Computation.pure a)).destruct = lmap f (rmap (map f) (Computation.pure a).destruct)
think : ∀ (s : Computation α), (map f s.think).destruct = lmap f (rmap (map f) s.think.destruct)
⊢ (map f s).destruct = lmap f (rmap (map f) s.destruct)

Tactic:
induction s using recOn
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ (map f (pure a)).destruct = lmap f (rmap (map f) (pure a).destruct)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ (map f s.think).destruct = lmap f (rmap (map f) s.think.destruct)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
a :
  (map id
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
            al)).val
      (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al)
⊢ map id (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
a :
  Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option α) none (fun (val : α) ↦ some val) o) f =
    f
⊢ (map id
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
            al)).val
      (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al)

Tactic:
simp only [map, comp_apply, id_eq]

Premises used: Computation.map, Function.comp_apply, id_eq