Theorem: AIG.LawfulStreamOperator.IsPrefix_aig (LeanSAT/AIG/LawfulStreamOperator.lean)

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ IsPrefix aig.decls (f aig input).aig.decls
Tactic:
apply IsPrefix.of
State after:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

State before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. intro idx h
  apply decl_eq
State after:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

State before:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. apply le_size
State after:
no goals

State before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]
Tactic:
intro idx h
State after:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]

State before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]
Tactic:
apply decl_eq
State after:
no goals

State before:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
apply le_size
State after:
no goals