Theorem: differsIsCorect (Advent/List/Indexing.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true ↔ DifferentList xs
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true → DifferentList xs

case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true → DifferentList xs

case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true
Tactic:
apply correctLeft
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true
Tactic:
apply correctRight
State after:
no goals