-- 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:
case oldAtom
α : 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:
next idx' _ _ _ =>
replace hidx : idx ≤ idx' := by omega
cases Nat.eq_or_lt_of_le hidx with
| inl hidxeq =>
  simp only [hidxeq, ih3, Decl.atom.injEq] at heq
  rw [← heq]
  apply Exists.intro
  assumption
| inr hlt => apply ih5 <;> assumption

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a' : α
val✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a'
ih4 : map✝[a']? = none
ih5 : ∀ (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✝.insert a' val✝)[a]? = some n

Tactic:
rw [HashMap.getElem?_insert]

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx' : Nat
map✝ : HashMap α Nat
a' : α
val✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a'
ih4 : map✝[a']? = none
ih5 : ∀ (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, (if (a' == a) = true then some val✝ else map✝[a]?) = some n

Proof state:
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

Tactic:
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' : α
val✝ : Nat
ih1 : Inv2 decls idx' map✝
ih2 : idx' < decls.size
ih3 : decls[idx'] = Decl.atom a'
ih4 : map✝[a']? = none
ih5 : ∀ (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'
heq2 : (a' == a) = false
hidxeq : idx = idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
subst hidxeq

Result:
case inl
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
map✝ : HashMap α Nat
a' : α
val✝ : Nat
ih4 : map✝[a']? = none
heq2 : (a' == a) = false
ih1 : Inv2 decls idx map✝
ih2 : idx < decls.size
ih3 : decls[idx] = Decl.atom a'
ih5 : ∀ (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 inr
α : 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'
hlt : idx < idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
apply ih4 <;> assumption

Result:
no goals

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
⊢ idx ≤ idx'

Tactic:
omega

Result:
no goals

Proof state:
case newAtom
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
decls : Array (Decl α)
idx upper : Nat
map : HashMap α Nat
a : α
idx✝ : Nat
map✝ : HashMap α Nat
a✝ : α
val✝ : Nat
ih1 : Inv2 decls idx✝ map✝
ih2 : idx✝ < decls.size
ih3 : decls[idx✝] = Decl.atom a✝
ih4 : map✝[a✝]? = none
ih5 : ∀ (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✝.insert a✝ val✝)[a]? = some n

Tactic:
next idx' _ a' _ =>
replace hidx : idx ≤ idx' := by omega
rw [HashMap.getElem?_insert]
match heq2 : a' == a with
| false =>
  simp only [Bool.false_eq_true, ↓reduceIte]
  cases Nat.eq_or_lt_of_le hidx with
  | inl hidxeq =>
    subst hidxeq
    simp_all only [beq_eq_false_iff_ne, Decl.atom.injEq]
  | inr hlt =>
    exact ih5 hlt heq
| true =>
  exact Option.isSome_iff_exists.mp rfl

Result:
no goals

Proof state:
case oldAtom
α : 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✝
ih5 : ∀ (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:
simp_all only [true_implies]

Result:
case oldAtom
α : 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

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
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