Theorem: var_resolution_step (Saturn/Resolution.lean)

State before:
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
⊢ VarSat left valuationVal ∨ VarSat right valuationVal → VarSat top valuationVal
Tactic:
intro hyp
State after:
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
hyp : VarSat left valuationVal ∨ VarSat right valuationVal
⊢ VarSat top valuationVal

State before:
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
hyp : VarSat left valuationVal ∨ VarSat right valuationVal
⊢ VarSat top valuationVal
Tactic:
cases hyp with
| inl heq =>
  induction join with
  | noneNone =>
    assumption
  | noneSome b =>
    injection heq
  | someNone b =>
    assumption
  | someSome b =>
    assumption
| inr heq =>
  induction join with
  | noneNone =>
    assumption
  | noneSome b =>
    assumption
  | someNone b =>
    injection heq
  | someSome b =>
    assumption
State after:
no goals

State before:
case inl
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
heq : VarSat left valuationVal
⊢ VarSat top valuationVal
Tactic:
induction join with
| noneNone =>
  assumption
| noneSome b =>
  injection heq
| someNone b =>
  assumption
| someSome b =>
  assumption
State after:
no goals

State before:
case inl.noneNone
left right top : Option Bool
valuationVal : Bool
heq : VarSat none valuationVal
⊢ VarSat none valuationVal
Tactic:
assumption
State after:
no goals

State before:
case inl.noneSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat none valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
injection heq
State after:
no goals

State before:
case inl.someNone
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
State after:
no goals

State before:
case inl.someSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
State after:
no goals

State before:
case inr
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
heq : VarSat right valuationVal
⊢ VarSat top valuationVal
Tactic:
induction join with
| noneNone =>
  assumption
| noneSome b =>
  assumption
| someNone b =>
  injection heq
| someSome b =>
  assumption
State after:
no goals

State before:
case inr.noneNone
left right top : Option Bool
valuationVal : Bool
heq : VarSat none valuationVal
⊢ VarSat none valuationVal
Tactic:
assumption
State after:
no goals

State before:
case inr.noneSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
State after:
no goals

State before:
case inr.someNone
left right top : Option Bool
valuationVal b : Bool
heq : VarSat none valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
injection heq
State after:
no goals

State before:
case inr.someSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
State after:
no goals