-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx}
    (assign : β → Bool) :
    ⟦aig.relabel r, ⟨start, hidx⟩, assign⟧
      =
    ⟦aig, ⟨start, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧

Proof state:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ ((⟦assign, { aig := relabel r aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign, { aig := relabel r aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
rw [denote_idx_gate heq2]

Result:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ ((⟦assign, { aig := relabel r aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign, { aig := relabel r aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign ∘ r, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign ∘ r, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Proof state:
case hatom.intro.intro
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
a : β
x : α
heq1 : (relabel r aig).decls[start] = Decl.atom (r x)
hlx : aig.decls[start] = Decl.atom x
hrx : a = r x
⊢ assign a = (assign ∘ r) x

Tactic:
simp [hrx]

Result:
no goals

Proof state:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
        ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
intro lhs rhs linv rinv heq1

Result:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Proof state:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ ((⟦assign, { aig := relabel r aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign, { aig := relabel r aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign ∘ r, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign ∘ r, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Tactic:
have := aig.invariant (by rw [← relabel_size_eq_size (r := r)]; omega) heq2

Result:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ ((⟦assign, { aig := relabel r aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign, { aig := relabel r aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign ∘ r, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign ∘ r, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Proof state:
case hconst
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
⊢ ∀ (b : Bool),
    (relabel r aig).decls[start] = Decl.const b →
      ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
        ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
intro b heq1

Result:
case hconst
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel r aig).decls[start] = Decl.const b
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ start < aig.decls.size

Tactic:
rw [← relabel_size_eq_size (r := r)]

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ start < (relabel r aig).decls.size

Proof state:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ ((⟦assign, { aig := relabel r aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign, { aig := relabel r aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign ∘ r, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign ∘ r, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Tactic:
rw [denote_relabel aig r lhs assign]

Result:
case hgate
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel r aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ ((⟦assign ∘ r, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign, { aig := relabel r aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign ∘ r, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign ∘ r, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))