internlm/Lean-Github huggingface dataset:
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls ?intro.mk.upper (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < ?intro.mk.upper
Tactic:
. exact aig.decls.size
Proof state after:
case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Tactic:
. apply ofAIG.Inv2
Proof state after:
case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Tactic:
. omega
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat
Tactic:
exact aig.decls.size
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)
Tactic:
apply ofAIG.Inv2
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.relabelNat'_fst_eq_relabelNat
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ aig.relabelNat'.fst = aig.relabelNat
Tactic:
rfl
Proof state after:
no goals
Theorem: AIG.relabelNat_size_eq_size
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ aig.relabelNat.decls.size = aig.decls.size
Tactic:
simp [relabelNat, relabelNat']
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ aig.relabelNat.unsatAt idx hidx1 ↔ aig.unsatAt idx hidx2
Tactic:
dsimp [relabelNat, relabelNat']
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ (relabel
          (fun x =>
            match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0)
          aig).unsatAt
      idx hidx1 ↔
    aig.unsatAt idx hidx2
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ (relabel
          (fun x =>
            match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0)
          aig).unsatAt
      idx hidx1 ↔
    aig.unsatAt idx hidx2
Tactic:
rw [relabel_unsat_iff]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ ∀ (x y : α),
    x ∈ aig →
      y ∈ aig →
        ((match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0) =
            match (RelabelNat.State.ofAIG aig).find? y with
            | some var => var
            | none => 0) →
          x = y
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ ∀ (x y : α),
    x ∈ aig →
      y ∈ aig →
        ((match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0) =
            match (RelabelNat.State.ofAIG aig).find? y with
            | some var => var
            | none => 0) →
          x = y
Tactic:
intro x y hx hy heq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
heq :
  (match (RelabelNat.State.ofAIG aig).find? x with
    | some var => var
    | none => 0) =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
heq :
  (match (RelabelNat.State.ofAIG aig).find? x with
    | some var => var
    | none => 0) =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
split at heq
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
. next hcase1 =>
  split at heq
  . next hcase2 =>
    apply RelabelNat.State.ofAIG_find_unique
    . assumption
    . rw [heq]
      assumption
  . next hcase2 =>
    exfalso
    rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
    simp[hcase2] at hn
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
. next hcase =>
  exfalso
  rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
  simp[hcase] at hn
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
next hcase1 =>
split at heq
. next hcase2 =>
  apply RelabelNat.State.ofAIG_find_unique
  . assumption
  . rw [heq]
    assumption
. next hcase2 =>
  exfalso
  rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
  simp[hcase2] at hn
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
split at heq
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
. next hcase2 =>
  apply RelabelNat.State.ofAIG_find_unique
  . assumption
  . rw [heq]
    assumption
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
. next hcase2 =>
  exfalso
  rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
  simp[hcase2] at hn
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y
Tactic:
next hcase2 =>
apply RelabelNat.State.ofAIG_find_unique
. assumption
. rw [heq]
  assumption
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y
Tactic:
apply RelabelNat.State.ofAIG_find_unique
Proof state after:
case ha
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? x = some ?n

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? y = some ?n

case n
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ Nat

case aig
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ AIG α
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case ha
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? x = some ?n

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? y = some ?n

case n
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ Nat

case aig
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ AIG α
Tactic:
. assumption
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝¹
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝¹
Tactic:
. rw [heq]
  assumption
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case ha
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? x = some ?n
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝¹
Tactic:
rw [heq]
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
next hcase2 =>
exfalso
rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
simp[hcase2] at hn
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
exfalso
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ False
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ False
Tactic:
rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
Proof state after:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? y = some n
⊢ False
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? y = some n
⊢ False
Tactic:
simp[hcase2] at hn
Proof state after:
no goals