Theorem: Etch.Verification.Stream.map_zero (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ map f 0 = 0
Tactic:
ext <;> try rfl
State after:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ HEq (map f 0).value 0.value

State before:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ HEq (map f 0).value 0.value
Tactic:
rw [heq_iff_eq]
State after:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ (map f 0).value = 0.value

State before:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ (map f 0).value = 0.value
Tactic:
funext ⟨q, h⟩
State after:
case value.h
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
q : { x // (map f 0).valid x = true }
h : (map f 0).ready q = true
⊢ (map f 0).value { val := q, property := h } = 0.value { val := q, property := h }

State before:
case value.h
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
q : { x // (map f 0).valid x = true }
h : (map f 0).ready q = true
⊢ (map f 0).value { val := q, property := h } = 0.value { val := q, property := h }
Tactic:
cases h
State after:
no goals

State before:
case ready
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ HEq (map f 0).ready 0.ready
Tactic:
rfl
State after:
no goals