-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem Inv1.lt_of_get?_eq_some [EquivBEq α] {n m : Nat} (map : HashMap α Nat) (x : α)
    (hinv : Inv1 n map) :
    map[x]? = some m → m < n

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : (x == y) = false
⊢ (if (y == x) = true then some n✝ else map✝[x]?) = some m → m < n✝ + 1

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

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : (x == y) = false
⊢ map✝[x]? = some m → m < n✝ + 1

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : (x == y) = true
⊢ (if (y == x) = true then some n✝ else map✝[x]?) = some m → m < n✝ + 1

Tactic:
simp only [beq_iff_eq] at hx

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : x = y
⊢ (if (y == x) = true then some n✝ else map✝[x]?) = some m → m < n✝ + 1

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : (x == y) = false
h : map✝[x]? = some m
⊢ m < n✝ + 1

Tactic:
specialize ih3 h

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
hx : (x == y) = false
h : map✝[x]? = some m
ih3 : m < n✝
⊢ m < n✝ + 1

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
hx : (x == y) = false
h : map✝[x]? = some m
ih3 : m < n✝
⊢ m < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
hinv : Inv1 n map
⊢ map[x]? = some m → m < n

Tactic:
induction hinv with
| empty => simp
| insert ih1 ih2 ih3 =>
  rename_i y
  rw [Std.HashMap.getElem?_insert]
  match hx : x == y with
  | true =>
    simp only [beq_iff_eq] at hx
    simp only [hx, beq_self_eq_true, ↓reduceIte, Option.some.injEq]
    omega
  | false =>
    simp only [BEq.symm_false hx, Bool.false_eq_true, ↓reduceIte]
    intro h
    specialize ih3 h
    omega

Result:
no goals

Proof state:
case empty
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
⊢ ∅[x]? = some m → m < 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : (x == y) = false
⊢ map✝[x]? = some m → m < n✝ + 1

Tactic:
intro h

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : (x == y) = false
h : map✝[x]? = some m
⊢ m < n✝ + 1

Proof state:
case insert
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
x✝ : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[x✝]? = none
ih3 : map✝[x]? = some m → m < n✝
⊢ (map✝.insert x✝ n✝)[x]? = some m → m < n✝ + 1

Tactic:
rename_i y

Result:
case insert
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
⊢ (map✝.insert y n✝)[x]? = some m → m < n✝ + 1

Proof state:
case insert
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
⊢ (if (y == x) = true then some n✝ else map✝[x]?) = some m → m < n✝ + 1

Tactic:
match hx : x == y with
| true =>
  simp only [beq_iff_eq] at hx
  simp only [hx, beq_self_eq_true, ↓reduceIte, Option.some.injEq]
  omega
| false =>
  simp only [BEq.symm_false hx, Bool.false_eq_true, ↓reduceIte]
  intro h
  specialize ih3 h
  omega

Result:
no goals

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : x = y
⊢ (if (y == x) = true then some n✝ else map✝[x]?) = some m → m < n✝ + 1

Tactic:
simp only [hx, beq_self_eq_true, ↓reduceIte, Option.some.injEq]

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : x = y
⊢ n✝ = m → m < n✝ + 1

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
hx : x = y
⊢ n✝ = m → m < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
case insert
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
⊢ (map✝.insert y n✝)[x]? = some m → m < n✝ + 1

Tactic:
rw [Std.HashMap.getElem?_insert]

Result:
case insert
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
map : HashMap α Nat
x : α
n✝ : Nat
map✝ : HashMap α Nat
y : α
ih1 : Inv1 n✝ map✝
ih2 : map✝[y]? = none
ih3 : map✝[x]? = some m → m < n✝
⊢ (if (y == x) = true then some n✝ else map✝[x]?) = some m → m < n✝ + 1