-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) :
    ⟦(fold aig (FoldTarget.mkAnd s)), assign⟧
      ↔
    (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (∀ (idx : Nat) (hidx1 : idx < len),
      ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true) ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
constructor

Result:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (∀ (idx : Nat) (hidx1 : idx < len),
      ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true) →
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true) →
    ∀ (idx : Nat) (hidx1 : idx < len),
      ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (⟦assign, { aig := (aig.mkConstCached true).aig, ref := (aig.mkConstCached true).ref }⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        0 ≤ idx → ⟦assign, { aig := (aig.mkConstCached true).aig, ref := (s.cast ⋯).get idx hidx1 }⟧ = true) ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst,
Nat.zero_le, get_cast, Ref.cast_eq, true_implies, true_and]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (∀ (idx : Nat) (hidx1 : idx < len),
      ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true) ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ ⟦assign, fold aig (FoldTarget.mkAnd s)⟧ = true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
unfold fold

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ ⟦assign,
        let res := aig.mkConstCached true;
        let aig_1 := res.aig;
        let acc := res.ref;
        let input := (FoldTarget.mkAnd s).vec.cast ⋯;
        fold.go aig_1 acc 0 (FoldTarget.mkAnd s).len input (FoldTarget.mkAnd s).func⟧ =
      true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Proof state:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (∀ (idx : Nat) (hidx1 : idx < len),
      ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true) →
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
intro h idx hidx

Result:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
h :
  ∀ (idx : Nat) (hidx1 : idx < len),
    ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true
idx : Nat
hidx : idx < len
⊢ ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Proof state:
case mpr.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ idx < len

Tactic:
simp [FoldTarget.mkAnd, hidx]

Result:
no goals

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true

Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)]

Result:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ ⟦assign, { aig := aig, ref := { gate := (s.get idx hidx).gate, hgate := ?mpr } }⟧ = true

case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ (s.get idx hidx).gate < aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ ⟦assign,
        let res := aig.mkConstCached true;
        let aig_1 := res.aig;
        let acc := res.ref;
        let input := (FoldTarget.mkAnd s).vec.cast ⋯;
        fold.go aig_1 acc 0 (FoldTarget.mkAnd s).len input (FoldTarget.mkAnd s).func⟧ =
      true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
simp only [FoldTarget.mkAnd]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ ⟦assign, fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 len (s.cast ⋯) mkAndCached⟧ = true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true) →
    ∀ (idx : Nat) (hidx1 : idx < len),
      ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true

Tactic:
intro h idx hidx

Result:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
h : ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
idx : Nat
hidx : idx < len
⊢ ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true

Proof state:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
h :
  ∀ (idx : Nat) (hidx1 : idx < len),
    ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx1).gate, hgate := ⋯ } }⟧ = true
idx : Nat
hidx : idx < len
⊢ ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
specialize h idx hidx

Result:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true
⊢ ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true