-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem Cache.IsExtensionBy_set (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2) (idx : Nat)
    (hbound : idx < cache1.marks.size) (h : cache2.marks = cache1.marks.set idx true) :
    IsExtensionBy cache1 cache2 idx (by have := cache1.hmarks; omega)

Proof state:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
this : cache1.marks.size = aig.decls.size
⊢ idx < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
⊢ cache1.IsExtensionBy cache2 idx ⋯

Tactic:
apply IsExtensionBy.mk

Result:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache1.marks[idx_1] = true → cache2.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
⊢ cache2.marks[idx] = true

Proof state:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx✝ : Nat
hbound : idx✝ < cache1.marks.size
h : cache2.marks = cache1.marks.set idx✝ true hbound
idx : Nat
hidx : idx < aig.decls.size
hmark : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true

Tactic:
simp [Array.getElem_set, hmark, h]

Result:
no goals

Proof state:
case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
⊢ cache2.marks[idx] = true

Tactic:
simp [h]

Result:
no goals

Proof state:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
⊢ idx < aig.decls.size

Tactic:
have := cache1.hmarks

Result:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
this : cache1.marks.size = aig.decls.size
⊢ idx < aig.decls.size

Proof state:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set idx true hbound
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache1.marks[idx_1] = true → cache2.marks[idx_1] = true

Tactic:
intro idx hidx hmark

Result:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx✝ : Nat
hbound : idx✝ < cache1.marks.size
h : cache2.marks = cache1.marks.set idx✝ true hbound
idx : Nat
hidx : idx < aig.decls.size
hmark : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true