Theorem: LoVe.neq_fin4_of_neq (LoVe/Homework/Homework7.lean)

State before:
a b : ℕ
ha : a < 4
hb : b < 4
⊢ a ≠ b → { val := a, isLt := ha } ≠ { val := b, isLt := hb }
Tactic:
intro _ h
State after:
a b : ℕ
ha : a < 4
hb : b < 4
a✝ : a ≠ b
h : { val := a, isLt := ha } = { val := b, isLt := hb }
⊢ False

State before:
a b : ℕ
ha : a < 4
hb : b < 4
a✝ : a ≠ b
h : { val := a, isLt := ha } = { val := b, isLt := hb }
⊢ False
Tactic:
cases h
State after:
case refl
a : ℕ
ha hb : a < 4
a✝ : a ≠ a
⊢ False

State before:
case refl
a : ℕ
ha hb : a < 4
a✝ : a ≠ a
⊢ False
Tactic:
contradiction
State after:
no goals