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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 0 ≤ 1
H : Multiset.card ((evalMultiset s q) i) = 0
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
rw [Multiset.card_eq_zero] at H
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 0 ≤ 1
H : (evalMultiset s q) i = 0
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 0 ≤ 1
H : (evalMultiset s q) i = 0
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
simp [H, evalOption]
State after:
no goals

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
H : Multiset.card ((evalMultiset s q) i) = 1
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
rw [Multiset.card_eq_one] at H
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
H : ∃ a, (evalMultiset s q) i = {a}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
H : ∃ a, (evalMultiset s q) i = {a}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
rcases H with ⟨a', ha'⟩
State after:
case intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
a' : α
ha' : (evalMultiset s q) i = {a'}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)

State before:
case intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
a' : α
ha' : (evalMultiset s q) i = {a'}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
simp [evalOption, ha']
State after:
no goals