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

State before:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
⊢ (∀ (i : xs.Index), p i ↔ q i) → search hp = search hq
Tactic:
intro h
State after:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ search hp = search hq

State before:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ search hp = search hq
Tactic:
apply search_eq
State after:
case h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ (fun i => p i) = fun i => q i

State before:
case h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ (fun i => p i) = fun i => q i
Tactic:
funext i
State after:
case h.h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
i : xs.Index
⊢ p i = q i

State before:
case h.h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
i : xs.Index
⊢ p i = q i
Tactic:
exact propext (h i)
State after:
no goals