Theorem: AIG.Ref_cast' (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
⊢ ref.gate < aig2.decls.size
Tactic:
have := ref.hgate
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
this : ref.gate < aig1.decls.size
⊢ ref.gate < aig2.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
this : ref.gate < aig1.decls.size
⊢ ref.gate < aig2.decls.size
Tactic:
omega
State after:
no goals