. simp [Ref.mk.injEq]
  rw [Array.get_append_left]
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }