internlm/Lean-Github huggingface dataset:
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
case h_2.h_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝³ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝³ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝² x✝¹ : Decl α
linv✝ rinv✝ : Bool
heq✝² : aig.decls[input.lhs.ref.gate] = Decl.const false
heq✝¹ : input.lhs.inv = true
heq✝ : input.rhs.inv = false
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → False
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := input.rhs.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
next heq _ _ _ =>
simp_all [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝³ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝² x✝¹ : Decl α
linv✝ rinv✝ : Bool
heq : aig.decls[input.lhs.ref.gate] = Decl.const false
heq✝¹ : input.lhs.inv = true
heq✝ : input.rhs.inv = false
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → False
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := input.rhs.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
simp_all [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
case h_2.h_7
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝⁴ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝³ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝³ x✝² : Decl α
linv✝ rinv✝ : Bool
heq✝² : aig.decls[input.rhs.ref.gate] = Decl.const true
heq✝¹ : input.lhs.inv = false
heq✝ : input.rhs.inv = false
x✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const false → False
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const true → False
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := input.lhs.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
next heq _ _ _ _ =>
simp_all [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝⁴ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝³ x✝² : Decl α
linv✝ rinv✝ : Bool
heq : aig.decls[input.rhs.ref.gate] = Decl.const true
heq✝¹ : input.lhs.inv = false
heq✝ : input.rhs.inv = false
x✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const false → False
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const true → False
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := input.lhs.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
simp_all [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
case h_2.h_8
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝³ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝³ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝² x✝¹ : Decl α
linv✝ rinv✝ : Bool
heq✝² : aig.decls[input.rhs.ref.gate] = Decl.const false
heq✝¹ : input.lhs.inv = false
heq✝ : input.rhs.inv = true
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const false → False
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := input.lhs.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
next heq _ _ _ =>
simp_all [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝³ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝² x✝¹ : Decl α
linv✝ rinv✝ : Bool
heq : aig.decls[input.rhs.ref.gate] = Decl.const false
heq✝¹ : input.lhs.inv = false
heq✝ : input.rhs.inv = true
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const false → False
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := input.lhs.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
simp_all [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.mkGateCached_eval_eq_mkGate_eval
Proof state before:
case h_2.h_9
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝¹⁰ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝⁹ x✝⁸ : Decl α
linv✝ rinv✝ : Bool
x✝⁷ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = true → False
x✝⁶ : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = false → False
x✝⁵ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.rhs.inv = true → False
x✝⁴ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.rhs.inv = false → False
x✝³ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝² : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = true → input.rhs.inv = false → False
x✝¹ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.lhs.inv = false → input.rhs.inv = true → False
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
            cache :=
              Cache.insert aig.decls aig.cache
                (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkGate input, assign⟧
Tactic:
simp [mkGate, denote]
Proof state after:
no goals
Theorem: Assignment.removePos_addPos_cancel
Proof state before:
assignment : Assignment
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Tactic:
rw [removePosAssignment, addPosAssignment]
Proof state after:
assignment : Assignment
h : ¬assignment.hasPosAssignment = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => unassigned
    | neg => neg
    | both => neg
    | unassigned => unassigned) =
    assignment
Theorem: Assignment.removePos_addPos_cancel
Proof state before:
assignment : Assignment
h : ¬assignment.hasPosAssignment = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => unassigned
    | neg => neg
    | both => neg
    | unassigned => unassigned) =
    assignment
Tactic:
rw [hasPosAssignment] at h
Proof state after:
assignment : Assignment
h :
  ¬(match assignment with
      | pos => true
      | neg => false
      | both => true
      | unassigned => false) =
      true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => unassigned
    | neg => neg
    | both => neg
    | unassigned => unassigned) =
    assignment
Theorem: Assignment.removePos_addPos_cancel
Proof state before:
assignment : Assignment
h :
  ¬(match assignment with
      | pos => true
      | neg => false
      | both => true
      | unassigned => false) =
      true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => unassigned
    | neg => neg
    | both => neg
    | unassigned => unassigned) =
    assignment
Tactic:
cases assignment <;> simp_all
Proof state after:
no goals
Theorem: Assignment.removeNeg_addNeg_cancel
Proof state before:
assignment : Assignment
h : ¬assignment.hasNegAssignment = true
⊢ assignment.addNegAssignment.removeNegAssignment = assignment
Tactic:
rw [removeNegAssignment, addNegAssignment]
Proof state after:
assignment : Assignment
h : ¬assignment.hasNegAssignment = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => unassigned
    | both => pos
    | unassigned => unassigned) =
    assignment
Theorem: Assignment.removeNeg_addNeg_cancel
Proof state before:
assignment : Assignment
h : ¬assignment.hasNegAssignment = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => unassigned
    | both => pos
    | unassigned => unassigned) =
    assignment
Tactic:
rw [hasNegAssignment] at h
Proof state after:
assignment : Assignment
h :
  ¬(match assignment with
      | pos => false
      | neg => true
      | both => true
      | unassigned => false) =
      true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => unassigned
    | both => pos
    | unassigned => unassigned) =
    assignment
Theorem: Assignment.removeNeg_addNeg_cancel
Proof state before:
assignment : Assignment
h :
  ¬(match assignment with
      | pos => false
      | neg => true
      | both => true
      | unassigned => false) =
      true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => unassigned
    | both => pos
    | unassigned => unassigned) =
    assignment
Tactic:
cases assignment <;> simp_all
Proof state after:
no goals
Theorem: Assignment.remove_add_cancel
Proof state before:
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
by_cases hb : b
Proof state after:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment

case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Theorem: Assignment.remove_add_cancel
Proof state before:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment

case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
. simp only [removeAssignment, hb, addAssignment, ite_true]
  simp only [hasAssignment, hb, ite_true] at h
  exact removePos_addPos_cancel h
Proof state after:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Theorem: Assignment.remove_add_cancel
Proof state before:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
. simp only [removeAssignment, hb, addAssignment, ite_true]
  simp only [hasAssignment, hb, ite_false] at h
  exact removeNeg_addNeg_cancel h
Proof state after:
no goals
Theorem: Assignment.remove_add_cancel
Proof state before:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
simp only [removeAssignment, hb, addAssignment, ite_true]
Proof state after:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Theorem: Assignment.remove_add_cancel
Proof state before:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Tactic:
simp only [hasAssignment, hb, ite_true] at h
Proof state after:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Theorem: Assignment.remove_add_cancel
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Tactic:
exact removePos_addPos_cancel h
Proof state after:
no goals
Theorem: Assignment.remove_add_cancel
Proof state before:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
simp only [removeAssignment, hb, addAssignment, ite_true]
Proof state after:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
Theorem: Assignment.remove_add_cancel
Proof state before:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
Tactic:
simp only [hasAssignment, hb, ite_false] at h
Proof state after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.hasNegAssignment = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
Theorem: Assignment.remove_add_cancel
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.hasNegAssignment = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
Tactic:
exact removeNeg_addNeg_cancel h
Proof state after:
no goals
Theorem: Assignment.add_of_both_eq_both
Proof state before:
b : Bool
⊢ addAssignment b both = both
Tactic:
rw [addAssignment]
Proof state after:
b : Bool
⊢ (if b = true then addPosAssignment else addNegAssignment) both = both
Theorem: Assignment.add_of_both_eq_both
Proof state before:
b : Bool
⊢ (if b = true then addPosAssignment else addNegAssignment) both = both
Tactic:
split <;> decide
Proof state after:
no goals
Theorem: Assignment.has_of_both
Proof state before:
b : Bool
⊢ hasAssignment b both = true
Tactic:
rw [hasAssignment]
Proof state after:
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment) both = true
Theorem: Assignment.has_of_both
Proof state before:
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment) both = true
Tactic:
split <;> decide
Proof state after:
no goals
Theorem: Assignment.has_of_add
Proof state before:
assignment : Assignment
b : Bool
⊢ hasAssignment b (addAssignment b assignment) = true
Tactic:
rw [addAssignment, hasAssignment]
Proof state after:
assignment : Assignment
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment)
      ((if b = true then addPosAssignment else addNegAssignment) assignment) =
    true
Theorem: Assignment.has_of_add
Proof state before:
assignment : Assignment
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment)
      ((if b = true then addPosAssignment else addNegAssignment) assignment) =
    true
Tactic:
split
Proof state after:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ assignment.addPosAssignment.hasPosAssignment = true

case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Theorem: Assignment.has_of_add
Proof state before:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ assignment.addPosAssignment.hasPosAssignment = true

case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Tactic:
. rw [hasPosAssignment, addPosAssignment]
  cases assignment <;> simp
Proof state after:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Theorem: Assignment.has_of_add
Proof state before:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Tactic:
. rw [hasNegAssignment, addNegAssignment]
  cases assignment <;> simp
Proof state after:
no goals
Theorem: Assignment.has_of_add
Proof state before:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ assignment.addPosAssignment.hasPosAssignment = true
Tactic:
rw [hasPosAssignment, addPosAssignment]
Proof state after:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    true
Theorem: Assignment.has_of_add
Proof state before:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    true
Tactic:
cases assignment <;> simp
Proof state after:
no goals
Theorem: Assignment.has_of_add
Proof state before:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Tactic:
rw [hasNegAssignment, addNegAssignment]
Proof state after:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    true
Theorem: Assignment.has_of_add
Proof state before:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    true
Tactic:
cases assignment <;> simp
Proof state after:
no goals
Theorem: Assignment.not_hasPos_of_removePos
Proof state before:
assignment : Assignment
⊢ ¬assignment.removePosAssignment.hasPosAssignment = true
Tactic:
simp only [removePosAssignment, hasPosAssignment, Bool.not_eq_true]
Proof state after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => unassigned
      | neg => neg
      | both => neg
      | unassigned => unassigned with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
Theorem: Assignment.not_hasPos_of_removePos
Proof state before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => unassigned
      | neg => neg
      | both => neg
      | unassigned => unassigned with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
Tactic:
cases assignment <;> simp
Proof state after:
no goals
Theorem: Assignment.not_hasNeg_of_removeNeg
Proof state before:
assignment : Assignment
⊢ ¬assignment.removeNegAssignment.hasNegAssignment = true
Tactic:
simp only [removeNegAssignment, hasNegAssignment, Bool.not_eq_true]
Proof state after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => unassigned
      | both => pos
      | unassigned => unassigned with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
Theorem: Assignment.not_hasNeg_of_removeNeg
Proof state before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => unassigned
      | both => pos
      | unassigned => unassigned with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
Tactic:
cases assignment <;> simp
Proof state after:
no goals
Theorem: Assignment.not_has_of_remove
Proof state before:
assignment : Assignment
b : Bool
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
by_cases hb : b
Proof state after:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Theorem: Assignment.not_has_of_remove
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
. have h := not_hasPos_of_removePos assignment
  simp [hb, h, removeAssignment, hasAssignment]
Proof state after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Theorem: Assignment.not_has_of_remove
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
. have h := not_hasNeg_of_removeNeg assignment
  simp [hb, h, removeAssignment, hasAssignment]
Proof state after:
no goals
Theorem: Assignment.not_has_of_remove
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
have h := not_hasPos_of_removePos assignment
Proof state after:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.removePosAssignment.hasPosAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Theorem: Assignment.not_has_of_remove
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.removePosAssignment.hasPosAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
simp [hb, h, removeAssignment, hasAssignment]
Proof state after:
no goals
Theorem: Assignment.not_has_of_remove
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
have h := not_hasNeg_of_removeNeg assignment
Proof state after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.removeNegAssignment.hasNegAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Theorem: Assignment.not_has_of_remove
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.removeNegAssignment.hasNegAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
simp [hb, h, removeAssignment, hasAssignment]
Proof state after:
no goals