-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lhs rhs linv rinv) :
    ⟦aig, ⟨start, hstart⟩, assign⟧
      =
    (
      (⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv)
        &&
      (⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv)
    )

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

Tactic:
split

Result:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
b✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.const b✝
⊢ b✝ =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
idx✝ : α
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.atom idx✝
⊢ assign idx✝ =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

case h_3
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ lhs < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.gate lhs rhs linv rinv = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

Tactic:
simp_all

Result:
no goals

Proof state:
case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
idx✝ : α
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.atom idx✝
⊢ assign idx✝ =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ rhs < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ lhs < aig.decls.size

Tactic:
have := aig.invariant hstart h

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ lhs < aig.decls.size