Theorem: Section3sheet1.Yb_ne_Yc (FormalisingMathematics2024/Section03functions/Sheet3.lean)

State before:
⊢ Y.b ≠ Y.c
Tactic:
intro h
State after:
h : Y.b = Y.c
⊢ False

State before:
h : Y.b = Y.c
⊢ False
Tactic:
cases h
State after:
no goals