Theorem: List.Index.unsublist_neg_tail (GMLInit/Data/Index/Sublist.lean)

State before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ unsublist p (⋯ ▸ i) = (unsublist p i).tail
Tactic:
simp only [unsublist]
State after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i)).tail) =
    (unsublist p i).tail

State before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i)).tail) =
    (unsublist p i).tail
Tactic:
rw [dif_neg h]
State after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (unsublist p (⋯ ▸ ⋯ ▸ i)).tail = (unsublist p i).tail

State before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (unsublist p (⋯ ▸ ⋯ ▸ i)).tail = (unsublist p i).tail
Tactic:
congr
State after:
case e_a.e_i
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ ⋯ ▸ ⋯ ▸ i = i

State before:
case e_a.e_i
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ ⋯ ▸ ⋯ ▸ i = i
Tactic:
elim_casts
State after:
no goals