Theorem: LRAT.DefaultFormula.insert_iff (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
⊢ c2 ∈ (f.insert c1).toList ↔ c2 = c1 ∨ c2 ∈ f.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
  List.mem_map, Misc.Prod.exists, Misc.Bool.exists_bool]
State after:
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
by_cases c2 = c1
State after:
case pos
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case neg
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case pos
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case neg
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
. next c2_eq_c1 =>
  constructor
  . intro _
    exact Or.inl c2_eq_c1
  . intro _
    apply Or.inl
    simp only [c2_eq_c1, insert]
    split <;> simp
State after:
case neg
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case neg
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
. next c2_ne_c1 =>
  constructor
  . intro h
    apply Or.inr
    rcases h with h | h | h
    . apply Or.inl
      simp only [insert] at h
      split at h
      all_goals
        simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
        rcases h with h | h
        . exact h
        . exact False.elim $ c2_ne_c1 h
    . rw [insert_preserves_rupUnits] at h
      exact Or.inr $ Or.inl h
    . rw [insert_preserves_ratUnits] at h
      exact Or.inr $ Or.inr h
  . intro h
    rcases h with h | h | h | h
    . exact False.elim $ c2_ne_c1 h
    . apply Or.inl
      simp only [insert]
      split
      all_goals
        simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
        exact Or.inl h
    . rw [insert_preserves_rupUnits]
      exact Or.inr $ Or.inl h
    . rw [insert_preserves_ratUnits]
      exact Or.inr $ Or.inr h
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
next c2_eq_c1 =>
constructor
. intro _
  exact Or.inl c2_eq_c1
. intro _
  apply Or.inl
  simp only [c2_eq_c1, insert]
  split <;> simp
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
constructor
State after:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) →
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) →
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. intro _
  exact Or.inl c2_eq_c1
State after:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. intro _
  apply Or.inl
  simp only [c2_eq_c1, insert]
  split <;> simp
State after:
no goals

State before:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) →
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
intro _
State after:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inl c2_eq_c1
State after:
no goals

State before:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
intro _
State after:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
apply Or.inl
State after:
case mpr.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data

State before:
case mpr.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data
Tactic:
simp only [c2_eq_c1, insert]
State after:
case mpr.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c1 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data

State before:
case mpr.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
a✝ :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c1 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data
Tactic:
split <;> simp
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
next c2_ne_c1 =>
constructor
. intro h
  apply Or.inr
  rcases h with h | h | h
  . apply Or.inl
    simp only [insert] at h
    split at h
    all_goals
      simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
      rcases h with h | h
      . exact h
      . exact False.elim $ c2_ne_c1 h
  . rw [insert_preserves_rupUnits] at h
    exact Or.inr $ Or.inl h
  . rw [insert_preserves_ratUnits] at h
    exact Or.inr $ Or.inr h
. intro h
  rcases h with h | h | h | h
  . exact False.elim $ c2_ne_c1 h
  . apply Or.inl
    simp only [insert]
    split
    all_goals
      simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
      exact Or.inl h
  . rw [insert_preserves_rupUnits]
    exact Or.inr $ Or.inl h
  . rw [insert_preserves_ratUnits]
    exact Or.inr $ Or.inr h
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
constructor
State after:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) →
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) →
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. intro h
  apply Or.inr
  rcases h with h | h | h
  . apply Or.inl
    simp only [insert] at h
    split at h
    all_goals
      simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
      rcases h with h | h
      . exact h
      . exact False.elim $ c2_ne_c1 h
  . rw [insert_preserves_rupUnits] at h
    exact Or.inr $ Or.inl h
  . rw [insert_preserves_ratUnits] at h
    exact Or.inr $ Or.inr h
State after:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. intro h
  rcases h with h | h | h | h
  . exact False.elim $ c2_ne_c1 h
  . apply Or.inl
    simp only [insert]
    split
    all_goals
      simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
      exact Or.inl h
  . rw [insert_preserves_rupUnits]
    exact Or.inr $ Or.inl h
  . rw [insert_preserves_ratUnits]
    exact Or.inr $ Or.inr h
State after:
no goals

State before:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) →
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
intro h
State after:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
apply Or.inr
State after:
case mp.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
rcases h with h | h | h
State after:
case mp.h.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ (f.insert c1).clauses.data
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp.h.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ (f.insert c1).clauses.data
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
. apply Or.inl
  simp only [insert] at h
  split at h
  all_goals
    simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
    rcases h with h | h
    . exact h
    . exact False.elim $ c2_ne_c1 h
State after:
case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
. rw [insert_preserves_rupUnits] at h
  exact Or.inr $ Or.inl h
State after:
case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
. rw [insert_preserves_ratUnits] at h
  exact Or.inr $ Or.inr h
State after:
no goals

State before:
case mp.h.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ (f.insert c1).clauses.data
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
apply Or.inl
State after:
case mp.h.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ (f.insert c1).clauses.data
⊢ some c2 ∈ f.clauses.data

State before:
case mp.h.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ (f.insert c1).clauses.data
⊢ some c2 ∈ f.clauses.data
Tactic:
simp only [insert] at h
State after:
case mp.h.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  some c2 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data
⊢ some c2 ∈ f.clauses.data

State before:
case mp.h.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  some c2 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data
⊢ some c2 ∈ f.clauses.data
Tactic:
split at h
State after:
case mp.h.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data
⊢ some c2 ∈ f.clauses.data

case mp.h.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data
⊢ some c2 ∈ f.clauses.data

case mp.h.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
⊢ some c2 ∈ f.clauses.data

State before:
case mp.h.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data
⊢ some c2 ∈ f.clauses.data

case mp.h.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data
⊢ some c2 ∈ f.clauses.data

case mp.h.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
⊢ some c2 ∈ f.clauses.data
Tactic:
all_goals
  simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
  rcases h with h | h
  . exact h
  . exact False.elim $ c2_ne_c1 h
State after:
no goals

State before:
case mp.h.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h :
  some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
⊢ some c2 ∈ f.clauses.data
Tactic:
simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
State after:
case mp.h.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : some c2 ∈ f.clauses.data ∨ c2 = c1
⊢ some c2 ∈ f.clauses.data

State before:
case mp.h.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : some c2 ∈ f.clauses.data ∨ c2 = c1
⊢ some c2 ∈ f.clauses.data
Tactic:
rcases h with h | h
State after:
case mp.h.inl.h.h_3.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ f.clauses.data

case mp.h.inl.h.h_3.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : c2 = c1
⊢ some c2 ∈ f.clauses.data

State before:
case mp.h.inl.h.h_3.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ f.clauses.data

case mp.h.inl.h.h_3.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : c2 = c1
⊢ some c2 ∈ f.clauses.data
Tactic:
. exact h
State after:
case mp.h.inl.h.h_3.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : c2 = c1
⊢ some c2 ∈ f.clauses.data

State before:
case mp.h.inl.h.h_3.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : c2 = c1
⊢ some c2 ∈ f.clauses.data
Tactic:
. exact False.elim $ c2_ne_c1 h
State after:
no goals

State before:
case mp.h.inl.h.h_3.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ f.clauses.data
Tactic:
exact h
State after:
no goals

State before:
case mp.h.inl.h.h_3.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
h : c2 = c1
⊢ some c2 ∈ f.clauses.data
Tactic:
exact False.elim $ c2_ne_c1 h
State after:
no goals

State before:
case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
rw [insert_preserves_rupUnits] at h
State after:
case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp.h.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inr $ Or.inl h
State after:
no goals

State before:
case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  ∃ a,
    (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
rw [insert_preserves_ratUnits] at h
State after:
case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mp.h.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inr $ Or.inr h
State after:
no goals

State before:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
⊢ (c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2) →
    some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
intro h
State after:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h :
  c2 = c1 ∨
    some c2 ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
rcases h with h | h | h | h
State after:
case mpr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : c2 = c1
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : c2 = c1
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. exact False.elim $ c2_ne_c1 h
State after:
case mpr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. apply Or.inl
  simp only [insert]
  split
  all_goals
    simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
    exact Or.inl h
State after:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. rw [insert_preserves_rupUnits]
  exact Or.inr $ Or.inl h
State after:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. rw [insert_preserves_ratUnits]
  exact Or.inr $ Or.inr h
State after:
no goals

State before:
case mpr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : c2 = c1
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact False.elim $ c2_ne_c1 h
State after:
no goals

State before:
case mpr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
apply Or.inl
State after:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data

State before:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data
Tactic:
simp only [insert]
State after:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data

State before:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data
Tactic:
split
State after:
case mpr.inr.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data

case mpr.inr.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data

case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data

State before:
case mpr.inr.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data

case mpr.inr.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data

case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
Tactic:
all_goals
  simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
  exact Or.inl h
State after:
no goals

State before:
case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
Tactic:
simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
State after:
case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈ f.clauses.data ∨ c2 = c1

State before:
case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈ f.clauses.data ∨ c2 = c1
Tactic:
exact Or.inl h
State after:
no goals

State before:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
rw [insert_preserves_rupUnits]
State after:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inr $ Or.inl h
State after:
no goals

State before:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
rw [insert_preserves_ratUnits]
State after:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2

State before:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inr $ Or.inr h
State after:
no goals