-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : DefaultClause n) :
    c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f

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

Tactic:
rcases h with h | h | h | h

Result:
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.toList ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.toList ∧ 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.toList
⊢ some c2 ∈ (f.insert c1).clauses.toList ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.toList ∧ 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.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.toList ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.toList ∧ 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.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.toList ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.toList ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.toList ∧ unit (a, true) = c2

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

Tactic:
intro _

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

Proof state:
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.toList ∧ unit (a, false) = c2 ∨
      (a, true) ∈ (f.insert c1).ratUnits.toList ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.toList ∨
    (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c2

Tactic:
rw [ratUnits_insert] at h

Result:
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.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.toList ∨
    (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c2

Proof state:
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.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c2
⊢ some c2 ∈ f.clauses.toList ∨
    (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c2

Tactic:
exact Or.inr <| Or.inr h

Result:
no goals

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

Tactic:
intro h

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