Theorem: AIG.toCNF.inj_is_injection (LeanSAT/AIG/CNF.lean)

State before:
aig : AIG Nat
a b : aig.CNFVar
⊢ inj a = inj b → a = b
Tactic:
intro h
State after:
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b

State before:
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b
Tactic:
cases a with
| inl =>
  cases b with
  | inl =>
    dsimp [inj] at h
    apply congrArg
    apply Nat.add_left_cancel
    exact h
  | inr rhs =>
    exfalso
    dsimp [inj] at h
    have := rhs.isLt
    omega
| inr lhs =>
  cases b with
  | inl =>
    exfalso
    dsimp [inj] at h
    have := lhs.isLt
    omega
  | inr =>
    dsimp [inj] at h
    apply congrArg
    apply Fin.eq_of_val_eq
    exact h
State after:
no goals

State before:
case inl
aig : AIG Nat
b : aig.CNFVar
val✝ : Nat
h : inj (Sum.inl val✝) = inj b
⊢ Sum.inl val✝ = b
Tactic:
cases b with
| inl =>
  dsimp [inj] at h
  apply congrArg
  apply Nat.add_left_cancel
  exact h
| inr rhs =>
  exfalso
  dsimp [inj] at h
  have := rhs.isLt
  omega
State after:
no goals

State before:
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : inj (Sum.inl val✝¹) = inj (Sum.inl val✝)
⊢ Sum.inl val✝¹ = Sum.inl val✝
Tactic:
dsimp [inj] at h
State after:
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝

State before:
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝
Tactic:
apply congrArg
State after:
case inl.inl.h
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ val✝¹ = val✝

State before:
case inl.inl.h
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ val✝¹ = val✝
Tactic:
apply Nat.add_left_cancel
State after:
case inl.inl.h.a
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ ?inl.inl.h.n + val✝¹ = ?inl.inl.h.n + val✝

case inl.inl.h.n
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Nat

State before:
case inl.inl.h.a
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ ?inl.inl.h.n + val✝¹ = ?inl.inl.h.n + val✝

case inl.inl.h.n
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Nat
Tactic:
exact h
State after:
no goals

State before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ Sum.inl val✝ = Sum.inr rhs
Tactic:
exfalso
State after:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ False

State before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ False
Tactic:
dsimp [inj] at h
State after:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
⊢ False

State before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
⊢ False
Tactic:
have := rhs.isLt
State after:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
this : ↑rhs < aig.decls.size
⊢ False

State before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
this : ↑rhs < aig.decls.size
⊢ False
Tactic:
omega
State after:
no goals

State before:
case inr
aig : AIG Nat
b : aig.CNFVar
lhs : Fin aig.decls.size
h : inj (Sum.inr lhs) = inj b
⊢ Sum.inr lhs = b
Tactic:
cases b with
| inl =>
  exfalso
  dsimp [inj] at h
  have := lhs.isLt
  omega
| inr =>
  dsimp [inj] at h
  apply congrArg
  apply Fin.eq_of_val_eq
  exact h
State after:
no goals

State before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ Sum.inr lhs = Sum.inl val✝
Tactic:
exfalso
State after:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ False

State before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ False
Tactic:
dsimp [inj] at h
State after:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ False

State before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ False
Tactic:
have := lhs.isLt
State after:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
this : ↑lhs < aig.decls.size
⊢ False

State before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
this : ↑lhs < aig.decls.size
⊢ False
Tactic:
omega
State after:
no goals

State before:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : inj (Sum.inr lhs) = inj (Sum.inr val✝)
⊢ Sum.inr lhs = Sum.inr val✝
Tactic:
dsimp [inj] at h
State after:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ Sum.inr lhs = Sum.inr val✝

State before:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ Sum.inr lhs = Sum.inr val✝
Tactic:
apply congrArg
State after:
case inr.inr.h
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝

State before:
case inr.inr.h
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝
Tactic:
apply Fin.eq_of_val_eq
State after:
case inr.inr.h.a
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ ↑lhs = ↑val✝

State before:
case inr.inr.h.a
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ ↑lhs = ↑val✝
Tactic:
exact h
State after:
no goals