-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF.inj_is_injection {aig : AIG Nat} (a b : CNFVar aig) :
    toCNF.inj a = toCNF.inj b → a = b

Proof state:
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 only [inj] at h
  congr
  omega
| inr rhs =>
  exfalso
  dsimp only [inj] at h
  have := rhs.isLt
  omega

Result:
no goals

Proof state:
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 only [inj] at h

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

Proof state:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ Sum.inr lhs = Sum.inl val✝

Tactic:
omega

Result:
no goals

Proof state:
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 only [inj] at h

Result:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ Sum.inr lhs = Sum.inr val✝

Proof state:
aig : AIG Nat
a b : aig.CNFVar
⊢ inj a = inj b → a = b

Tactic:
intro h

Result:
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b

Proof state:
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 only [inj] at h

Result:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
⊢ False

Proof state:
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b

Tactic:
cases a with
| inl =>
  cases b with
  | inl =>
    dsimp only [inj] at h
    congr
    omega
  | inr rhs =>
    exfalso
    dsimp only [inj] at h
    have := rhs.isLt
    omega
| inr lhs =>
  cases b with
  | inl =>
    dsimp only [inj] at h
    omega
  | inr =>
    dsimp only [inj] at h
    congr
    omega

Result:
no goals

Proof state:
case inr.inr.e_val
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝

Tactic:
omega

Result:
no goals

Proof state:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ Sum.inr lhs = Sum.inr val✝

Tactic:
congr

Result:
case inr.inr.e_val
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝

Proof state:
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

Result:
no goals

Proof state:
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

Result:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ False

Proof state:
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 =>
  dsimp only [inj] at h
  omega
| inr =>
  dsimp only [inj] at h
  congr
  omega

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
⊢ False

Tactic:
have := rhs.isLt

Result:
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

Proof state:
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:
dsimp only [inj] at h

Result:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ Sum.inr lhs = Sum.inl val✝

Proof state:
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:
congr

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