Theorem: LRAT.DefaultFormula.insert_iff
Proof 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
Proof 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