-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
    ⟦aig.mkGateCached input, assign⟧ = ⟦aig.mkGate input, assign⟧

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ ((⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv) &&
      (⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
rw [Bool.and_comm]

Result:
no goals

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : input.lhs.ref.gate < input.rhs.ref.gate
⊢ ⟦assign, mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
rw [mkGateCached.go_eval_eq_mkGate_eval]

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ ⟦assign, aig.mkGate { lhs := input.rhs, rhs := input.lhs }⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
simp only [denote_mkGate]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ ((⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv) &&
      (⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ ⟦assign, aig.mkGateCached input⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
simp only [mkGateCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ ⟦assign,
      if input.lhs.ref.gate < input.rhs.ref.gate then mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
      else mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }⟧ =
    ⟦assign, aig.mkGate input⟧

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ ⟦assign, mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
rw [mkGateCached.go_eval_eq_mkGate_eval]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ ⟦assign, aig.mkGate { lhs := input.rhs, rhs := input.lhs }⟧ = ⟦assign, aig.mkGate input⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ ⟦assign,
      if input.lhs.ref.gate < input.rhs.ref.gate then mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
      else mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }⟧ =
    ⟦assign, aig.mkGate input⟧

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : input.lhs.ref.gate < input.rhs.ref.gate
⊢ ⟦assign, mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }⟧ = ⟦assign, aig.mkGate input⟧

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ ⟦assign, mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }⟧ = ⟦assign, aig.mkGate input⟧