Theorem: LRAT.DefaultClause.isUnit_iff (LeanSAT/LRAT/Clause.lean)

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.isUnit = some l ↔ c.toList = [l]
Tactic:
simp only [isUnit, Prod.forall, toList]
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]
Tactic:
split
State after:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]

State before:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
. next l' heq => simp [heq]
State after:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]

State before:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
. next hne =>
  simp only [false_iff]
  intro heq
  exact hne l heq
State after:
no goals

State before:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]
Tactic:
next l' heq => simp [heq]
State after:
no goals

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l' : Literal (PosFin n)
heq : c.clause = [l']
⊢ some l' = some l ↔ c.clause = [l]
Tactic:
simp [heq]
State after:
no goals

State before:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
next hne =>
simp only [false_iff]
intro heq
exact hne l heq
State after:
no goals

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
simp only [false_iff]
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]
Tactic:
intro heq
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
heq : c.clause = [l]
⊢ False

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
heq : c.clause = [l]
⊢ False
Tactic:
exact hne l heq
State after:
no goals