case mk
α : Type u
β : Type v
γ : Type w
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } n = some a
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ ↑s m = some a → ↑s n = some a
cases' s with f al
case mk.refl
α : Type u
β : Type v
γ : Type w
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } m = some a

case mk.step
α : Type u
β : Type v
γ : Type w
a : α
m n✝ : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
n : ℕ
a✝ : Nat.le m n
IH : ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } n = some a
⊢ ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } (Nat.succ n) = some a
case mk
α : Type u
β : Type v
γ : Type w
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } n = some a
induction' h with n _ IH
no goals
case mk.refl
α : Type u
β : Type v
γ : Type w
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } m = some a

case mk.step
α : Type u
β : Type v
γ : Type w
a : α
m n✝ : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
n : ℕ
a✝ : Nat.le m n
IH : ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } n = some a
⊢ ↑{ val := f, property := al } m = some a → ↑{ val := f, property := al } (Nat.succ n) = some a
exacts [id, fun h2 => al (IH h2)]