Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.data → l' ∈ l ∨ l' ∈ units.data := by
  intro h
  exact Or.inr h
State after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
  (h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.data → l' ∈ l ∨ l' ∈ units.data) (l'' : Literal (PosFin n))
  (l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.data → l' ∈ l ∨ l' ∈ units.data := by
  intro l' l'_in_res
  rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
  . rw [l'_eq_l'']
    exact Or.inl l''_in_l
  . exact h l' l'_in_acc
State after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data) →
      ∀ (l'' : Literal (PosFin n)),
        l'' ∈ l → ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data) →
      ∀ (l'' : Literal (PosFin n)),
        l'' ∈ l → ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
exact List.foldlRecOn l insertUnit (units, assignments, foundContradiction) hb hl
State after:
no goals

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
l' : Literal (PosFin n)
⊢ l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
intro h
State after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
l' : Literal (PosFin n)
h : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' ∈ l ∨ l' ∈ units.data

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
l' : Literal (PosFin n)
h : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
exact Or.inr h
State after:
no goals

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
⊢ ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
intro l' l'_in_res
State after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
⊢ l' ∈ l ∨ l' ∈ units.data

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
State after:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data

case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data

State before:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data

case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
. rw [l'_eq_l'']
  exact Or.inl l''_in_l
State after:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data

State before:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
. exact h l' l'_in_acc
State after:
no goals

State before:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
rw [l'_eq_l'']
State after:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.data

State before:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.data
Tactic:
exact Or.inl l''_in_l
State after:
no goals

State before:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
exact h l' l'_in_acc
State after:
no goals