-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem of_isConstant {aig : AIG α} {assign : α → Bool} {ref : Ref aig} {b : Bool} :
    aig.isConstant ref b → ⟦aig, ref, assign⟧ = b

Proof state:
case mk.h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
decl✝ : Decl α
x✝ : ∀ (val : Bool), aig.decls[gate] = Decl.const val → False
h : false = true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Tactic:
contradiction

Result:
no goals

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
⊢ aig.isConstant { gate := gate, hgate := hgate } b = true →
    ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Tactic:
intro h

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
h : aig.isConstant { gate := gate, hgate := hgate } b = true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Proof state:
case mk.h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
decl✝ : Decl α
val✝ : Bool
heq✝ : aig.decls[gate] = Decl.const val✝
h : decide (b = val✝) = true
⊢ aig.decls[gate] = Decl.const b

Tactic:
simp_all

Result:
no goals

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
h :
  (match { gate := gate, hgate := hgate } with
    | { gate := gate, hgate := hgate } =>
      let decl := aig.decls[gate];
      match decl with
      | Decl.const val => decide (b = val)
      | x => false) =
    true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Tactic:
dsimp only at h

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
h :
  (match aig.decls[gate] with
    | Decl.const val => decide (b = val)
    | x => false) =
    true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
h : aig.isConstant { gate := gate, hgate := hgate } b = true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Tactic:
unfold isConstant at h

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
h :
  (match { gate := gate, hgate := hgate } with
    | { gate := gate, hgate := hgate } =>
      let decl := aig.decls[gate];
      match decl with
      | Decl.const val => decide (b = val)
      | x => false) =
    true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Proof state:
case mk.h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
decl✝ : Decl α
val✝ : Bool
heq✝ : aig.decls[gate] = Decl.const val✝
h : decide (b = val✝) = true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Tactic:
rw [denote_idx_const]

Result:
case mk.h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
decl✝ : Decl α
val✝ : Bool
heq✝ : aig.decls[gate] = Decl.const val✝
h : decide (b = val✝) = true
⊢ aig.decls[gate] = Decl.const b

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
h :
  (match aig.decls[gate] with
    | Decl.const val => decide (b = val)
    | x => false) =
    true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Tactic:
split at h

Result:
case mk.h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
decl✝ : Decl α
val✝ : Bool
heq✝ : aig.decls[gate] = Decl.const val✝
h : decide (b = val✝) = true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

case mk.h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
decl✝ : Decl α
x✝ : ∀ (val : Bool), aig.decls[gate] = Decl.const val → False
h : false = true
⊢ ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
ref : aig.Ref
b : Bool
⊢ aig.isConstant ref b = true → ⟦assign, { aig := aig, ref := ref }⟧ = b

Tactic:
rcases ref with ⟨gate, hgate⟩

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
b : Bool
gate : Nat
hgate : gate < aig.decls.size
⊢ aig.isConstant { gate := gate, hgate := hgate } b = true →
    ⟦assign, { aig := aig, ref := { gate := gate, hgate := hgate } }⟧ = b