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

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : xs.Index
hi : p i.val
⊢ unsublist p (sublist p i hi) = i
Tactic:
induction i with
| head =>
  rw [sublist_pos_head]
  rw [unsublist_pos_head]
| @tail xs x i ih =>
  by_cases p x with
  | isTrue hh =>
    rw [sublist_pos_tail hh]
    rw [unsublist_pos_tail hh]
    rw [ih]
  | isFalse hh =>
    rw [sublist_neg_tail hh]
    rw [unsublist_neg_tail hh]
    rw [ih]
State after:
no goals

State before:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (sublist p head hi) = head
Tactic:
rw [sublist_pos_head]
State after:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (⋯ ▸ head) = head

State before:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (⋯ ▸ head) = head
Tactic:
rw [unsublist_pos_head]
State after:
no goals

State before:
case tail
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
⊢ unsublist p (sublist p i.tail hi) = i.tail
Tactic:
by_cases p x with
| isTrue hh =>
  rw [sublist_pos_tail hh]
  rw [unsublist_pos_tail hh]
  rw [ih]
| isFalse hh =>
  rw [sublist_neg_tail hh]
  rw [unsublist_neg_tail hh]
  rw [ih]
State after:
no goals

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ unsublist p (sublist p i.tail hi) = i.tail
Tactic:
rw [sublist_pos_tail hh]
State after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ unsublist p (⋯ ▸ (sublist p i hi).tail) = i.tail

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ unsublist p (⋯ ▸ (sublist p i hi).tail) = i.tail
Tactic:
rw [unsublist_pos_tail hh]
State after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ (unsublist p (sublist p i hi)).tail = i.tail

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ (unsublist p (sublist p i hi)).tail = i.tail
Tactic:
rw [ih]
State after:
no goals

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ unsublist p (sublist p i.tail hi) = i.tail
Tactic:
rw [sublist_neg_tail hh]
State after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ unsublist p (⋯ ▸ sublist p i hi) = i.tail

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ unsublist p (⋯ ▸ sublist p i hi) = i.tail
Tactic:
rw [unsublist_neg_tail hh]
State after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ (unsublist p (sublist p i hi)).tail = i.tail

State before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ (unsublist p (sublist p i hi)).tail = i.tail
Tactic:
rw [ih]
State after:
no goals