-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
    (hidx : idx < lw + rw) :
    (lhs.append rhs).get idx hidx
      =
    if h : idx < lw then
      lhs.get idx h
    else
      rhs.get (idx - lw) (by omega)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
⊢ (lhs.append rhs).get idx hidx = if h : idx < lw then lhs.get idx h else rhs.get (idx - lw) ⋯

Tactic:
simp only [get, append]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lw ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h : ¬idx < lw
⊢ idx - lw < rw

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx

Tactic:
rw [lhs.hlen]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lw ≤ idx

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = rhs.refs[idx - lw]

Tactic:
rw [Array.getElem_append_right]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }

Tactic:
simp [Ref.mk.injEq]

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = lhs.refs[idx]

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]

Tactic:
simp [lhs.hlen]

Result:
no goals

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

Tactic:
simp only [Ref.mk.injEq]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = rhs.refs[idx - lw]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec 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✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefVec lw
rhs : aig.RefVec rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = lhs.refs[idx]

Tactic:
rw [Array.getElem_append_left]

Result:
no goals