-- 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
hidx : idx < upper
a : α
hinv : Inv2 decls upper map
heq : decls[idx] = Decl.atom a
⊢ ∃ n, map[a]? = some n

Tactic:
induction hinv with
| empty => omega
| newAtom ih1 ih2 ih3 ih4 ih5 =>
  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
| oldAtom ih1 ih2 ih3 ih4 ih5 =>
  simp_all only [true_implies]
  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
| const ih1 ih2 ih3 ih4 =>
  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
| gate ih1 ih2 ih3 ih4 =>
  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:
rw [← 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:
case inl
α : 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'
hidxeq : idx = idx'
⊢ ∃ n, map✝[a]? = some n

Tactic:
simp [hidxeq, ih3] at heq

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

Tactic:
apply ih4 <;> assumption

Result:
no goals

Proof state:
case gate
α : 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:
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 : α
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

Tactic:
simp_all only [beq_eq_false_iff_ne, Decl.atom.injEq]

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

Tactic:
simp [hidxeq, ih3] at heq

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
this : upper ≤ decls.size
⊢ idx < decls.size

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

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

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

Tactic:
simp only [Bool.false_eq_true, ↓reduceIte]

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