-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem denote.go_eq_of_isPrefix (decls1 decls2 : Array (Decl α)) (start : Nat) {hdag1} {hdag2}
    {hbounds1} {hbounds2} (hprefix : IsPrefix decls1 decls2) :
    denote.go start decls2 assign hbounds2 hdag2
      =
    denote.go start decls1 assign hbounds1 hdag1

Proof state:
case h_3.e_x.e_a
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go lhs decls2 assign ⋯ ⋯ = go lhs decls1 assign ⋯ ⋯

Tactic:
apply denote.go_eq_of_isPrefix

Result:
case h_3.e_x.e_a.hprefix
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ IsPrefix decls1 decls2

Proof state:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
⊢ rhs < decls1.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq : decls2[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)

Tactic:
rw [hidx1] at heq

Result:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq : decls1[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)

Proof state:
case h_2
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)

Tactic:
next heq =>
rw [hidx1] at heq
split <;> simp_all

Result:
no goals

Proof state:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
⊢ (match elem : decls2[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls2 assign ⋯ ⋯;
      let rval := go rhs decls2 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)

Tactic:
have hidx1 := hprefix.idx_eq start hbounds1

Result:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
⊢ (match elem : decls2[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls2 assign ⋯ ⋯;
      let rval := go rhs decls2 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)

Proof state:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ ⋯;
    let rval := go rhs decls2 assign ⋯ ⋯;
    (lval ^^ linv) && (rval ^^ rinv)) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)

Tactic:
have hidx2 := hprefix.idx_eq lhs (by omega)

Result:
α : Type
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDAG α decls1
hdag2 : IsDAG α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ ⋯;
    let rval := go rhs decls2 assign ⋯ ⋯;
    (lval ^^ linv) && (rval ^^ rinv)) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ ⋯;
      let rval := go rhs decls1 assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)