-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap α Nat)
    (hidx : idx < upper) (a : α) (hinv : Inv2 decls upper map)
    (heq : decls[idx]'(by have := upper_lt_size hinv; omega) = .atom a) :
    ∃ n, map[a]? = some n

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
b✝ : Bool
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.const b✝
ih4 : ∀ (hidx : idx < idx'), decls[idx] = Decl.atom a → ∃ n, map✝[a]? = some n
hidx : idx < idx' + 1
heq : decls[idx] = Decl.atom a
⊢ ∃ n, map✝[a]? = some n

Tactic:
replace hidx : idx ≤ idx' := by omega

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
b✝ : Bool
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.const b✝
ih4 : ∀ (hidx : idx < idx'), decls[idx] = Decl.atom a → ∃ n, map✝[a]? = some n
hidx✝ : idx < idx' + 1
heq : decls[idx] = Decl.atom a
hidx : idx ≤ idx'
⊢ ∃ n, map✝[a]? = some n

Proof state:
case const
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx✝ : Nat
map✝ : HashMap α Nat
b✝ : Bool
ih1 : Inv2 decls idx✝ map✝
ih2 : idx✝ < decls.size
ih3 : decls[idx✝] = Decl.const b✝
ih4 : ∀ (hidx : idx < idx✝), decls[idx] = Decl.atom a → ∃ n, map✝[a]? = some n
hidx : idx < idx✝ + 1
heq : decls[idx] = Decl.atom a
⊢ ∃ n, map✝[a]? = some n

Tactic:
next idx' _ _ =>
replace hidx : idx ≤ idx' := by omega
cases Nat.eq_or_lt_of_le hidx with
| inl hidxeq => simp [hidxeq, ih3] at heq
| inr hlt => apply ih4 <;> assumption

Result:
no goals

Proof state:
case inl
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a✝ : α
n✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a✝
ih4 : map✝[a✝]? = some n✝
hidx✝ : idx < idx' + 1
ih5 : idx < idx' → ∃ n, map✝[a]? = some n
hidx : idx ≤ idx'
hidxeq : idx = idx'
heq : a✝ = a
⊢ ∃ n, map✝[a✝]? = some n

Tactic:
apply Exists.intro

Result:
case inl.h
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a✝ : α
n✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a✝
ih4 : map✝[a✝]? = some n✝
hidx✝ : idx < idx' + 1
ih5 : idx < idx' → ∃ n, map✝[a]? = some n
hidx : idx ≤ idx'
hidxeq : idx = idx'
heq : a✝ = a
⊢ map✝[a✝]? = some ?inl.w

case inl.w
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a✝ : α
n✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a✝
ih4 : map✝[a✝]? = some n✝
hidx✝ : idx < idx' + 1
ih5 : idx < idx' → ∃ n, map✝[a]? = some n
hidx : idx ≤ idx'
hidxeq : idx = idx'
heq : a✝ = a
⊢ Nat

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
l✝ r✝ : Nat
li✝ ri✝ : Bool
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.gate l✝ r✝ li✝ ri✝
ih4 : ∀ (hidx : idx < idx'), decls[idx] = Decl.atom a → ∃ n, map✝[a]? = some n
hidx : idx < idx' + 1
heq : decls[idx] = Decl.atom a
⊢ idx ≤ idx'

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
hidx : idx < upper
a : α
hinv : Inv2 decls upper map
⊢ idx < decls.size

Tactic:
have := upper_lt_size hinv

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
hidx : idx < upper
a : α
hinv : Inv2 decls upper map
this : upper ≤ decls.size
⊢ idx < decls.size

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a✝ : α
n✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a✝
ih4 : map✝[a✝]? = some n✝
hidx : idx < idx' + 1
ih5 : idx < idx' → ∃ n, map✝[a]? = some n
heq : decls[idx] = Decl.atom a
⊢ ∃ n, map✝[a]? = some n

Tactic:
replace hidx : idx ≤ idx' := by omega

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a✝ : α
n✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a✝
ih4 : map✝[a✝]? = some n✝
hidx✝ : idx < idx' + 1
ih5 : idx < idx' → ∃ n, map✝[a]? = some n
heq : decls[idx] = Decl.atom a
hidx : idx ≤ idx'
⊢ ∃ n, map✝[a]? = some n

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
b✝ : Bool
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.const b✝
ih4 : ∀ (hidx : idx < idx'), decls[idx] = Decl.atom a → ∃ n, map✝[a]? = some n
hidx✝ : idx < idx' + 1
heq : decls[idx] = Decl.atom a
hidx : idx ≤ idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
cases Nat.eq_or_lt_of_le hidx with
| inl hidxeq => simp [hidxeq, ih3] at heq
| inr hlt => apply ih4 <;> assumption

Result:
no goals

Proof state:
case empty
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
hidx : idx < 0
heq : decls[idx] = Decl.atom a
⊢ ∃ n, ∅[a]? = some n

Tactic:
omega

Result:
no goals

Proof state:
case inr
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a✝ : α
n✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a✝
ih4 : map✝[a✝]? = some n✝
hidx✝ : idx < idx' + 1
ih5 : idx < idx' → ∃ n, map✝[a]? = some n
heq : decls[idx] = Decl.atom a
hidx : idx ≤ idx'
hlt : idx < idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
apply ih5 <;> assumption

Result:
no goals