-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
    ∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres : aig.mkGateCached input = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
unfold mkGateCached at hres

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres :
  (let lhs := input.lhs.ref.gate;
    let rhs := input.rhs.ref.gate;
    if lhs < rhs then mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
    else mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ ∀ (idx : Nat) (h1 : idx < (aig.mkGateCached input).aig.decls.size) (h2 : idx < aig.decls.size),
    (aig.mkGateCached input).aig.decls[idx] = aig.decls[idx]

Tactic:
generalize hres : mkGateCached aig input = res

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres : aig.mkGateCached input = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
all_goals
  rw [← hres]
  intros
  rw [mkGateCached.go_decl_eq]

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
rw [← hres]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size)
    (h2 : idx < aig.decls.size),
    (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls[idx] = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres :
  (let lhs := input.lhs.ref.gate;
    let rhs := input.rhs.ref.gate;
    if lhs < rhs then mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
    else mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
dsimp only at hres

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres :
  (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 }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size)
    (h2 : idx < aig.decls.size),
    (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls[idx] = aig.decls[idx]

Tactic:
intros

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
idx✝ : Nat
h1✝ : idx✝ < (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size
h2✝ : idx✝ < aig.decls.size
⊢ (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls[idx✝] = aig.decls[idx✝]

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
idx✝ : Nat
h1✝ : idx✝ < (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size
h2✝ : idx✝ < aig.decls.size
⊢ (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls[idx✝] = aig.decls[idx✝]

Tactic:
rw [mkGateCached.go_decl_eq]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres :
  (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 }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
split at hres

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
hres : mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]