-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/If.lean
theorem denote_ite {aig : AIG α} {input : IfInput aig w} :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦(ite aig input).aig, (ite aig input).vec.get idx hidx, assign⟧
      =
    if ⟦aig, input.discr, assign⟧ then
      ⟦aig, input.lhs.get idx hidx, assign⟧
    else
      ⟦aig, input.rhs.get idx hidx, assign⟧

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (ite aig input).aig, ref := (ite aig input).vec.get idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧

Tactic:
unfold ite

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (match input with
            | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).aig,
        ref :=
          (match input with
                | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).vec.get
            idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (match input with
            | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).aig,
        ref :=
          (match input with
                | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).vec.get
            idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).aig,
        ref := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).vec.get idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).aig,
        ref := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).vec.get idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧

Tactic:
rw [ite.denote_go]

Result:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (ite aig input).aig, ref := (ite aig input).vec.get idx hidx }⟧ =
      if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then
        ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
      else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (ite aig input).aig, ref := (ite aig input).vec.get idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧