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

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ f.readyForRatAdd → (f.insert c).readyForRatAdd
Tactic:
intro h
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRatAdd

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRatAdd
Tactic:
constructor
State after:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd

State before:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd
Tactic:
. simp only [insert, h.1] <;> split <;> rfl
State after:
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd

State before:
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd
Tactic:
. exact insert_readyForRupAdd f c h.2
State after:
no goals

State before:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).ratUnits = #[]
Tactic:
simp only [insert, h.1] <;> split <;> rfl
State after:
no goals

State before:
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd
Tactic:
exact insert_readyForRupAdd f c h.2
State after:
no goals