Theorem: Bool.majoritySelect_fin (Lib.lean)

State before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑0 = 1)) (decide (↑0 = 1)) = decide ((↑0 + ↑0 + ↑0) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑0 = 1)) (decide (↑1 = 1)) = decide ((↑0 + ↑0 + ↑1) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑1 = 1)) (decide (↑0 = 1)) = decide ((↑0 + ↑1 + ↑0) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑1 = 1)) (decide (↑1 = 1)) = decide ((↑0 + ↑1 + ↑1) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑0 = 1)) (decide (↑0 = 1)) = decide ((↑1 + ↑0 + ↑0) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑0 = 1)) (decide (↑1 = 1)) = decide ((↑1 + ↑0 + ↑1) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑1 = 1)) (decide (↑0 = 1)) = decide ((↑1 + ↑1 + ↑0) / 2 = 1)
Tactic:
decide
State after:
no goals

State before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑1 = 1)) (decide (↑1 = 1)) = decide ((↑1 + ↑1 + ↑1) / 2 = 1)
Tactic:
decide
State after:
no goals