Theorem: List.Index.unsublist_pos_head (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
⊢ unsublist p (⋯ ▸ head) = head
Tactic:
unfold 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
⊢ (if hh : p x then
      let_fun this := ⋯;
      match ⋯ ▸ ⋯ ▸ head with
      | head => head
      | i.tail => (unsublist p i).tail
    else
      let_fun this := ⋯;
      (unsublist p (this ▸ ⋯ ▸ head)).tail) =
    head

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
⊢ (if hh : p x then
      let_fun this := ⋯;
      match ⋯ ▸ ⋯ ▸ head with
      | head => head
      | i.tail => (unsublist p i).tail
    else
      let_fun this := ⋯;
      (unsublist p (this ▸ ⋯ ▸ head)).tail) =
    head
Tactic:
rw [dif_pos 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
⊢ (let_fun this := ⋯;
    match ⋯ ▸ ⋯ ▸ head with
    | head => head
    | i.tail => (unsublist p i).tail) =
    head

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
⊢ (let_fun this := ⋯;
    match ⋯ ▸ ⋯ ▸ head with
    | head => head
    | i.tail => (unsublist p i).tail) =
    head
Tactic:
split
State after:
case h_1
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = head
⊢ (let_fun this := ⋯;
    head) =
    head

case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head

State before:
case h_1
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = head
⊢ (let_fun this := ⋯;
    head) =
    head

case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head
Tactic:
next => rfl
State after:
case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head

State before:
case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head
Tactic:
next i hh => elim_casts at hh; contradiction
State after:
no goals

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
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = head
⊢ (let_fun this := ⋯;
    head) =
    head
Tactic:
rfl
State after:
no goals

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
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : ⋯ ▸ ⋯ ▸ head = i.tail
⊢ (let_fun this := ⋯;
    (unsublist p i).tail) =
    head
Tactic:
elim_casts at hh
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
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : head = i.tail
⊢ (let_fun this := ⋯;
    (unsublist p i).tail) =
    head

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
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : head = i.tail
⊢ (let_fun this := ⋯;
    (unsublist p i).tail) =
    head
Tactic:
contradiction
State after:
no goals