Theorem: AIG.RefStream.getRef_push_ref_eq' (LeanSAT/AIG/RefStream.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
⊢ idx < len + 1
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
⊢ (s.pushRef ref).getRef idx ⋯ = ref
Tactic:
have := s.hlen
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
this : s.refs.size = len
⊢ (s.pushRef ref).getRef idx ⋯ = ref

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
this : s.refs.size = len
⊢ (s.pushRef ref).getRef idx ⋯ = ref
Tactic:
simp [getRef, pushRef, ← this, hidx]
State after:
no goals