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

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

Tactic:
simp only [beq_iff_eq, hx, ↓reduceIte] at hfound1

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

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map : HashMap α Nat
n✝ : Nat
map✝ : HashMap α Nat
z : α
ih1 : Inv1 n✝ map✝
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hfound2 : (if (z == y) = true then some n✝ else map✝[y]?) = some m
hx : ¬z = x
hfound1 : map✝[x]? = some m
hy : ¬z = y
⊢ x = y

Tactic:
simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map : HashMap α Nat
n✝ : Nat
map✝ : HashMap α Nat
z : α
ih1 : Inv1 n✝ map✝
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hx : ¬z = x
hfound1 : map✝[x]? = some m
hy : ¬z = y
hfound2 : map✝[y]? = some m
⊢ x = y

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

Tactic:
rename_i z

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

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

Tactic:
simp only [beq_eq_false_iff_ne, ne_eq] at hy

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

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

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

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

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

Tactic:
induction hinv with
| empty => simp at hfound1
| insert ih1 _ih2 ih3 =>
  rename_i z
  rw [HashMap.getElem?_insert] at hfound1
  rw [HashMap.getElem?_insert] at hfound2
  match hx : z == x with
  | false =>
    simp only [beq_eq_false_iff_ne, ne_eq] at hx
    simp only [beq_iff_eq, hx, ↓reduceIte] at hfound1
    match hy : z == y with
    | false =>
      simp only [beq_eq_false_iff_ne, ne_eq] at hy
      simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2
      exact ih3 hfound1 hfound2
    | true =>
      simp only [hy, ↓reduceIte, Option.some.injEq] at hfound2
      have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound1
      omega
  | true =>
    simp only [hx, ↓reduceIte, Option.some.injEq] at hfound1
    rcases hfound1 with ⟨rfl⟩
    match hy : z == y with
    | false =>
      simp only [beq_eq_false_iff_ne, ne_eq] at hy
      simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2
      have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound2
      omega
    | true =>
      simp only [beq_iff_eq] at hx hy
      simp only [←hx, hy]

Result:
no goals

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

Tactic:
simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map map✝ : HashMap α Nat
z : α
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hx : (z == x) = true
ih1 : Inv1 m map✝
hy : ¬z = y
hfound2 : map✝[y]? = some m
⊢ x = y

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map : HashMap α Nat
n✝ : Nat
map✝ : HashMap α Nat
z : α
ih1 : Inv1 n✝ map✝
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hfound2 : (if (z == y) = true then some n✝ else map✝[y]?) = some m
hx : ¬z = x
hfound1 : map✝[x]? = some m
hy : (z == y) = true
⊢ x = y

Tactic:
simp only [hy, ↓reduceIte, Option.some.injEq] at hfound2

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map : HashMap α Nat
n✝ : Nat
map✝ : HashMap α Nat
z : α
ih1 : Inv1 n✝ map✝
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hx : ¬z = x
hfound1 : map✝[x]? = some m
hy : (z == y) = true
hfound2 : n✝ = m
⊢ x = y

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

Tactic:
simp only [beq_iff_eq] at hx hy

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

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map : HashMap α Nat
n✝ : Nat
map✝ : HashMap α Nat
z : α
ih1 : Inv1 n✝ map✝
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hx : ¬z = x
hfound1 : map✝[x]? = some m
hy : (z == y) = true
hfound2 : n✝ = m
this : m < n✝
⊢ x = y

Tactic:
omega

Result:
no goals