-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/If.lean
theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} :
    ⟦aig.mkIfCached input, assign⟧
      =
    if ⟦aig, input.discr, assign⟧ then ⟦aig, input.lhs, assign⟧ else ⟦aig, input.rhs, assign⟧

Proof state:
case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      {
        aig :=
          (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                    { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).ref,
                rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } }⟧ =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧)

Tactic:
rw [LawfulOperator.denote_mem_prefix]

Result:
case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } }⟧ =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧)

case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
            { gate := input.discr.gate, hgate := ⋯ }).aig.decls.size

Proof state:
case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } }⟧ =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧)

case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
            { gate := input.discr.gate, hgate := ⋯ }).aig.decls.size

Tactic:
rw [LawfulOperator.denote_mem_prefix]

Result:
case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      { aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } }⟧ =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧)

case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign, aig.mkIfCached input⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs }⟧
    else ⟦assign, { aig := aig, ref := input.rhs }⟧

Tactic:
rw [if_as_bool]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign, aig.mkIfCached input⟧ =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧ ||
      !⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Proof state:
case e_y.e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (!⟦assign,
        { aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
          ref := { gate := input.discr.gate, hgate := ⋯ } }⟧) =
    !⟦assign, { aig := aig, ref := input.discr }⟧

Tactic:
rw [LawfulOperator.denote_mem_prefix]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (⟦assign,
        {
          aig :=
            (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
                {
                  lhs :=
                    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                        { gate := input.discr.gate, hgate := ⋯ }).ref,
                  rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
          ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } }⟧ ||
      !⟦assign,
            { aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
              ref := { gate := input.discr.gate, hgate := ⋯ } }⟧ &&
        ⟦assign,
          {
            aig :=
              ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                  { gate := input.discr.gate, hgate := ⋯ }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧) =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧ ||
      !⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
congr 2

Result:
case e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      {
        aig :=
          (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                    { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).ref,
                rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } }⟧ =
    (⟦assign, { aig := aig, ref := input.discr }⟧ && ⟦assign, { aig := aig, ref := input.lhs }⟧)

case e_y.e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (!⟦assign,
        { aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
          ref := { gate := input.discr.gate, hgate := ⋯ } }⟧) =
    !⟦assign, { aig := aig, ref := input.discr }⟧

case e_y.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.rhs }⟧