Theorem: AIG.LawfulStreamOperator.le_size_of_le_aig_size (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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ (f aig input).aig.decls.size
Tactic:
apply Nat.le_trans
State after:
case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ Nat

State before:
case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ Nat
Tactic:
. exact h
State after:
case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

State before:
case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. exact le_size aig input
State after:
no goals

State before:
case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m
Tactic:
exact h
State after:
no goals

State before:
case a
α : 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 x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
exact le_size aig input
State after:
no goals