Theorem: IsDag.empty (LeanSAT/AIG/Basic.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ IsDag α #[]
Tactic:
intro i lhs rhs linv rinv h
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
Tactic:
simp only [Array.size_toArray, List.length_nil] at h
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
Tactic:
omega
State after:
no goals