-- 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:
α : 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 }⟧)

Tactic:
unfold mkIfCached

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      let res := aig.mkAndCached { lhs := input.discr, rhs := input.lhs };
      let aig_1 := res.aig;
      let lhsRef := res.ref;
      let input_1 := input.cast ⋯;
      let res_1 := aig_1.mkNotCached input_1.discr;
      let aig_2 := res_1.aig;
      let notDiscr := res_1.ref;
      let input_2 := input_1.cast ⋯;
      let res_2 := aig_2.mkAndCached { lhs := notDiscr, rhs := input_2.rhs };
      let aig_3 := res_2.aig;
      let rhsRef := res_2.ref;
      let lhsRef := lhsRef.cast ⋯;
      aig_3.mkOrCached { lhs := lhsRef, rhs := rhsRef }⟧ =
    (⟦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_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 }⟧)

Tactic:
simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      let res := aig.mkAndCached { lhs := input.discr, rhs := input.lhs };
      let aig_1 := res.aig;
      let lhsRef := res.ref;
      let input_1 := input.cast ⋯;
      let res_1 := aig_1.mkNotCached input_1.discr;
      let aig_2 := res_1.aig;
      let notDiscr := res_1.ref;
      let input_2 := input_1.cast ⋯;
      let res_2 := aig_2.mkAndCached { lhs := notDiscr, rhs := input_2.rhs };
      let aig_3 := res_2.aig;
      let rhsRef := res_2.ref;
      let lhsRef := lhsRef.cast ⋯;
      aig_3.mkOrCached { lhs := lhsRef, rhs := rhsRef }⟧ =
    (⟦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:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).ref,
                rhs := ((input.cast ⋯).cast ⋯).rhs }).aig.mkOrCached
        { lhs := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.cast ⋯,
          rhs :=
            (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      (input.cast ⋯).discr).aig.mkAndCached
                {
                  lhs :=
                    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                        (input.cast ⋯).discr).ref,
                  rhs := ((input.cast ⋯).cast ⋯).rhs }).ref }⟧ =
    (⟦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_y
α : 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.rhs.gate, hgate := ?e_y.e_y } }⟧ =
    ⟦assign, { aig := aig, ref := input.rhs }⟧

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

Tactic:
rw [LawfulOperator.denote_mem_prefix]

Result:
no goals

Proof state:
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

Tactic:
simp [Ref.hgate]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).ref,
                rhs := ((input.cast ⋯).cast ⋯).rhs }).aig.mkOrCached
        { lhs := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.cast ⋯,
          rhs :=
            (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      (input.cast ⋯).discr).aig.mkAndCached
                {
                  lhs :=
                    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                        (input.cast ⋯).discr).ref,
                  rhs := ((input.cast ⋯).cast ⋯).rhs }).ref }⟧ =
    (⟦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:
simp only [TernaryInput.cast, Ref.cast_eq, id_eq, Int.reduceNeg, denote_mkOrCached,
  denote_projected_entry, denote_mkAndCached, denote_mkNotCached]

Result:
α : 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 }⟧)