Theorem: top_of_join_not_positive (Saturn/Resolution.lean)

State before:
bf : Bool
left right top : Option Bool
⊢ IsJoin left right top → ¬left = some bf → ¬right = some bf → ¬top = some bf
Tactic:
intro join
State after:
bf : Bool
left right top : Option Bool
join : IsJoin left right top
⊢ ¬left = some bf → ¬right = some bf → ¬top = some bf

State before:
bf : Bool
left right top : Option Bool
join : IsJoin left right top
⊢ ¬left = some bf → ¬right = some bf → ¬top = some bf
Tactic:
induction join with
| noneNone => intros; simp
| noneSome b =>
  intros
  assumption
| someNone b =>
  intros
  assumption
| someSome b =>
  intros
  assumption
State after:
no goals

State before:
case noneNone
bf : Bool
left right top : Option Bool
⊢ ¬none = some bf → ¬none = some bf → ¬none = some bf
Tactic:
intros
State after:
case noneNone
bf : Bool
left right top : Option Bool
a✝¹ a✝ : ¬none = some bf
⊢ ¬none = some bf

State before:
case noneNone
bf : Bool
left right top : Option Bool
a✝¹ a✝ : ¬none = some bf
⊢ ¬none = some bf
Tactic:
simp
State after:
no goals

State before:
case noneSome
bf : Bool
left right top : Option Bool
b : Bool
⊢ ¬none = some bf → ¬some b = some bf → ¬some b = some bf
Tactic:
intros
State after:
case noneSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬none = some bf
a✝ : ¬some b = some bf
⊢ ¬some b = some bf

State before:
case noneSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬none = some bf
a✝ : ¬some b = some bf
⊢ ¬some b = some bf
Tactic:
assumption
State after:
no goals

State before:
case someNone
bf : Bool
left right top : Option Bool
b : Bool
⊢ ¬some b = some bf → ¬none = some bf → ¬some b = some bf
Tactic:
intros
State after:
case someNone
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬some b = some bf
a✝ : ¬none = some bf
⊢ ¬some b = some bf

State before:
case someNone
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬some b = some bf
a✝ : ¬none = some bf
⊢ ¬some b = some bf
Tactic:
assumption
State after:
no goals

State before:
case someSome
bf : Bool
left right top : Option Bool
b : Bool
⊢ ¬some b = some bf → ¬some b = some bf → ¬some b = some bf
Tactic:
intros
State after:
case someSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ a✝ : ¬some b = some bf
⊢ ¬some b = some bf

State before:
case someSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ a✝ : ¬some b = some bf
⊢ ¬some b = some bf
Tactic:
assumption
State after:
no goals