-- 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
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
have heq2 := relabel_gate 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
heq2 : 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:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
start : Nat
hidx : start < (relabel r aig).decls.size
assign : β → Bool
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
apply denote_idx_trichotomy

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),
    (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 := ⋯ } }⟧

case hatom
α : 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 : β),
    (relabel r aig).decls[start] = Decl.atom a →
      ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
        ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

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 := ⋯ } }⟧

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
heq1 : (relabel r aig).decls[start] = Decl.const b
heq2 : 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:
rw [denote_idx_const 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
heq2 : aig.decls[start] = Decl.const b
⊢ b = ⟦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 := start, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
rw [denote_idx_gate 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
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 := ⋯ } }⟧

Proof state:
case hatom
α : 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 : β
heq1 : (relabel r aig).decls[start] = Decl.atom a
⊢ assign a = ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
rcases relabel_atom heq1 with ⟨x, ⟨hlx, hrx⟩⟩

Result:
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 : β
heq1 : (relabel r aig).decls[start] = Decl.atom a
x : α
hlx : aig.decls[start] = Decl.atom x
hrx : a = r x
⊢ assign a = ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Proof state:
case hatom
α : 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 : β
heq1 : (relabel r aig).decls[start] = Decl.atom a
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := start, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
rw [denote_idx_atom heq1]

Result:
case hatom
α : 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 : β
heq1 : (relabel r aig).decls[start] = Decl.atom a
⊢ assign a = ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

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
heq1 : (relabel r aig).decls[start] = Decl.const b
heq2 : aig.decls[start] = Decl.const b
⊢ b = ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

Tactic:
rw [denote_idx_const heq2]

Result:
no goals