Theorem: cantorSurjection_surjective (GroupComp/CantorTree.lean)

State before:
⊢ ∀ (f : CantorTree' → Bool), ∃ t, cantorSurjection t = f
Tactic:
intro f
State after:
f : CantorTree' → Bool
⊢ ∃ t, cantorSurjection t = f

State before:
f : CantorTree' → Bool
⊢ ∃ t, cantorSurjection t = f
Tactic:
use CantorTree.node f
State after:
case h
f : CantorTree' → Bool
⊢ cantorSurjection (CantorTree.node f) = f

State before:
case h
f : CantorTree' → Bool
⊢ cantorSurjection (CantorTree.node f) = f
Tactic:
rfl
State after:
no goals