Theorem: List.Index.search_eq (Extra/Index/Basic.lean)

State before:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
ip : DecidablePred p
iq : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : p = q
⊢ search hp = search hq
Tactic:
cases h
State after:
case refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
iq : DecidablePred p
hq : ∃ j, p j
⊢ search hp = search hq

State before:
case refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
iq : DecidablePred p
hq : ∃ j, p j
⊢ search hp = search hq
Tactic:
cases Subsingleton.elim ip iq
State after:
case refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp hq : ∃ j, p j
⊢ search hp = search hq

State before:
case refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp hq : ∃ j, p j
⊢ search hp = search hq
Tactic:
cases Subsingleton.elim hp hq
State after:
case refl.refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
⊢ search hp = search hp

State before:
case refl.refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
⊢ search hp = search hp
Tactic:
rfl
State after:
no goals