-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat) (hcurr : curr ≤ len)
    (input : RefVec aig len) :
    ⟦
      (go aig acc curr len input mkAndCached).aig,
      (go aig acc curr len input mkAndCached).ref,
      assign
    ⟧
      =
    (
      ⟦aig, acc, assign⟧
        ∧
      (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦aig, input.get idx hidx1, assign⟧)
    )

Proof state:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h3 :
  ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦assign,
          { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
            ref := (input.get idx hidx1).cast ⋯ }⟧ =
        true
h1 : ⟦assign, { aig := aig, ref := acc }⟧ = true
h2 : ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
⊢ ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true

Tactic:
specialize h3 idx hidx1 (by omega)

Result:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦assign, { aig := aig, ref := acc }⟧ = true
h2 : ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦assign,
      { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig, ref := (input.get idx hidx1).cast ⋯ }⟧ =
    true
⊢ ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h3 :
  ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦assign,
          { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
            ref := (input.get idx hidx1).cast ⋯ }⟧ =
        true
h1 : ⟦assign, { aig := aig, ref := acc }⟧ = true
h2 : ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
⊢ curr + 1 ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.mpr.right
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦assign, { aig := aig, ref := acc }⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
⊢ ⟦assign,
      { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig, ref := (input.get idx hidx1).cast ⋯ }⟧ =
    true

Tactic:
specialize hrest idx hidx1 (by omega)

Result:
case isTrue.mpr.right
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦assign, { aig := aig, ref := acc }⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true
⊢ ⟦assign,
      { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig, ref := (input.get idx hidx1).cast ⋯ }⟧ =
    true

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ ((⟦assign, { aig := aig, ref := acc }⟧ = true ∧ ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦assign,
              { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
                ref := (input.get idx hidx1).cast ⋯ }⟧ =
            true) ↔
    ⟦assign, { aig := aig, ref := acc }⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true

Tactic:
constructor

Result:
case isTrue.mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ ((⟦assign, { aig := aig, ref := acc }⟧ = true ∧ ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦assign,
              { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
                ref := (input.get idx hidx1).cast ⋯ }⟧ =
            true) →
    ⟦assign, { aig := aig, ref := acc }⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true

case isTrue.mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ (⟦assign, { aig := aig, ref := acc }⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true) →
    (⟦assign, { aig := aig, ref := acc }⟧ = true ∧ ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦assign,
              { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
                ref := (input.get idx hidx1).cast ⋯ }⟧ =
            true