Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl (LeanSAT/AIG/CNF.lean)

State before:
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.IsExtensionBy cache idx ⋯
Tactic:
apply IsExtensionBy.mk
State after:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true

State before:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Tactic:
. intros
  assumption
State after:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true

State before:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Tactic:
. exact hmarked
State after:
no goals

State before:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true
Tactic:
intros
State after:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
idx✝ : Nat
hidx✝ : idx✝ < aig.decls.size
a✝ : cache.marks[idx✝] = true
⊢ cache.marks[idx✝] = true

State before:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
idx✝ : Nat
hidx✝ : idx✝ < aig.decls.size
a✝ : cache.marks[idx✝] = true
⊢ cache.marks[idx✝] = true
Tactic:
assumption
State after:
no goals

State before:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Tactic:
exact hmarked
State after:
no goals