Theorem: Imo1989P5.lemma3 (Compfiles/Imo1989P5.lean)

State before:
α : Type
l : List α
hl : l.Nodup
i j : Fin l.length
hij : i ≠ j
⊢ l.get i ≠ l.get j
Tactic:
intro hij'
State after:
α : Type
l : List α
hl : l.Nodup
i j : Fin l.length
hij : i ≠ j
hij' : l.get i = l.get j
⊢ False

State before:
α : Type
l : List α
hl : l.Nodup
i j : Fin l.length
hij : i ≠ j
hij' : l.get i = l.get j
⊢ False
Tactic:
exact hij (List.nodup_iff_injective_get.mp hl hij')
State after:
no goals