Theorem: CNF.nonempty_or_impossible (LeanSAT/Reflect/CNF/Relabel.lean)

State before:
α : Type
x : CNF α
⊢ Nonempty α ∨ ∃ n, x = List.replicate n []
Tactic:
induction x with
| nil => exact Or.inr ⟨0, rfl⟩
| cons c x ih => match c with
  | [] => cases ih with
    | inl h => left; exact h
    | inr h =>
      obtain ⟨n, rfl⟩ := h
      right
      exact ⟨n + 1, rfl⟩
  | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩
State after:
no goals

State before:
case nil
α : Type
⊢ Nonempty α ∨ ∃ n, [] = List.replicate n []
Tactic:
exact Or.inr ⟨0, rfl⟩
State after:
no goals

State before:
case cons
α : Type
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, c :: x = List.replicate n []
Tactic:
match c with
| [] => cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩
| ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩
State after:
no goals

State before:
α : Type
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []
Tactic:
cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩
State after:
no goals

State before:
case inl
α : Type
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []
Tactic:
left
State after:
case inl.h
α : Type
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α

State before:
case inl.h
α : Type
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α
Tactic:
exact h
State after:
no goals

State before:
case inr
α : Type
c : Clause α
x : List (Clause α)
h : ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []
Tactic:
obtain ⟨n, rfl⟩ := h
State after:
case inr.intro
α : Type
c : Clause α
n : Nat
⊢ Nonempty α ∨ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

State before:
case inr.intro
α : Type
c : Clause α
n : Nat
⊢ Nonempty α ∨ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []
Tactic:
right
State after:
case inr.intro.h
α : Type
c : Clause α
n : Nat
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

State before:
case inr.intro.h
α : Type
c : Clause α
n : Nat
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []
Tactic:
exact ⟨n + 1, rfl⟩
State after:
no goals

State before:
α : Type
c✝ : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
a : α
b : Bool
c : List (α × Bool)
⊢ Nonempty α ∨ ∃ n, ((a, b) :: c) :: x = List.replicate n []
Tactic:
exact Or.inl ⟨a⟩
State after:
no goals