-- 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
hfound2 : (if (z == y) = true then some n✝ else map✝[y]?) = some m
hx : ¬z = x
hfound1 : map✝[x]? = some m
⊢ x = y

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

Result:
no goals

Proof state:
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 : (if (z == x) = true then some n✝ else map✝[x]?) = some m
hfound2 : (map✝.insert z n✝)[y]? = some m
⊢ x = y

Tactic:
rw [HashMap.getElem?_insert] at hfound2

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 : (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
⊢ 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✝
hy : ¬z = y
hfound2 : map✝[y]? = some m
⊢ x = y

Tactic:
have := Inv1.lt_of_get?_eq_some _ _ ih1 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
this : m < 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
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

Tactic:
simp only [←hx, hy]

Result:
no goals

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) = 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 : 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

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

Tactic:
simp at hfound1

Result:
no goals

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

Tactic:
rw [HashMap.getElem?_insert] at hfound1

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 : (if (z == x) = true then some n✝ else map✝[x]?) = some m
hfound2 : (map✝.insert z n✝)[y]? = some m
⊢ x = y

Proof state:
case refl
α : 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
⊢ x = y

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

Tactic:
rcases hfound1 with ⟨rfl⟩

Result:
case refl
α : 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
⊢ 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) = false
⊢ x = y

Tactic:
simp only [beq_eq_false_iff_ne, ne_eq] at hx

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

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
⊢ x = y

Tactic:
have := Inv1.lt_of_get?_eq_some _ _ ih1 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
hx : ¬z = x
hfound1 : map✝[x]? = some m
hy : (z == y) = true
hfound2 : n✝ = m
this : m < n✝
⊢ 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
hfound2 : map✝[y]? = some m
⊢ x = y

Tactic:
exact ih3 hfound1 hfound2

Result:
no goals