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

Tactic:
omega

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

Tactic:
omega

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, (if (a' == a) = true then some val✝ else map✝[a]?) = some n

Tactic:
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:
α : 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
⊢ ∃ 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
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

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
hidx : idx ≤ idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
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
⊢ ∃ n, (map✝.insert a' val✝)[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' : α
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

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
heq : decls[idx] = Decl.atom a
hidx : idx ≤ idx'
hidxeq : idx = idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
simp only [hidxeq, ih3, Decl.atom.injEq] at heq

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

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'
heq2 : (a' == a) = true
⊢ ∃ n, (if true = true then some val✝ else map✝[a]?) = some n

Tactic:
exact Option.isSome_iff_exists.mp rfl

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' : α
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
hlt : idx < idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
exact ih5 hlt heq

Result:
no goals