Theorem: CNF.unsat_of_lift_unsat (LeanSAT/Reflect/Glue.lean)

State before:
cnf : CNF Nat
⊢ cnf.lift.unsat → cnf.unsat
Tactic:
intro h2
State after:
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ cnf.unsat

State before:
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ cnf.unsat
Tactic:
have h3 :=
  CNF.unsat_relabel_iff
    (by
      intro a b ha hb hab
      injections hab
      cases a; cases b; simp_all)
    |>.mp h2
State after:
cnf : CNF Nat
h2 : cnf.lift.unsat
h3 : cnf.relabelFin.unsat
⊢ cnf.unsat

State before:
cnf : CNF Nat
h2 : cnf.lift.unsat
h3 : cnf.relabelFin.unsat
⊢ cnf.unsat
Tactic:
exact CNF.unsat_relabelFin.mp h3
State after:
no goals

State before:
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ ∀ {a b : Fin cnf.numLiterals}, mem a cnf.relabelFin → mem b cnf.relabelFin → ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩ → a = b
Tactic:
intro a b ha hb hab
State after:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
hab : ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩
⊢ a = b

State before:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
hab : ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩
⊢ a = b
Tactic:
injections hab
State after:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
n_eq✝ : ↑a = ↑b
⊢ a = b

State before:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
n_eq✝ : ↑a = ↑b
⊢ a = b
Tactic:
cases a
State after:
case mk
cnf : CNF Nat
h2 : cnf.lift.unsat
b : Fin cnf.numLiterals
hb : mem b cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
ha : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝, isLt✝⟩ = ↑b
⊢ ⟨val✝, isLt✝⟩ = b

State before:
case mk
cnf : CNF Nat
h2 : cnf.lift.unsat
b : Fin cnf.numLiterals
hb : mem b cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
ha : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝, isLt✝⟩ = ↑b
⊢ ⟨val✝, isLt✝⟩ = b
Tactic:
cases b
State after:
case mk.mk
cnf : CNF Nat
h2 : cnf.lift.unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩

State before:
case mk.mk
cnf : CNF Nat
h2 : cnf.lift.unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩
Tactic:
simp_all
State after:
no goals