internlm/Lean-Github huggingface dataset:
Theorem: List.modifyLast_eq_modifyNth
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : [] ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = f x✝ :: xs✝

α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
simp_all only [tsub_le_iff_right, ge_iff_le, ne_eq, nil_append, cons.injEq]
Proof state after:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Theorem: List.modifyLast_eq_modifyNth
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
simp only [length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
  nonpos_iff_eq_zero, le_refl]
Proof state after:
no goals
Theorem: Array.modifyLast_data
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modifyLast f a).data = List.modifyLast f a.data
Tactic:
unfold modifyLast
Proof state after:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyLast f a.data
Theorem: Array.modifyLast_data
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyLast f a.data
Tactic:
rw [List.modifyLast_eq_modifyNth]
Proof state after:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyNth f (List.length a.data - 1) a.data
Theorem: Array.modifyLast_data
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyNth f (List.length a.data - 1) a.data
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, modify_data]
Proof state after:
no goals
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
a b c : ℕ
h : c ≤ b
⊢ a - (b - c) = a + c - b
Tactic:
induction a generalizing b c with
| zero => simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, tsub_le_iff_right, Nat.zero_sub,
  tsub_eq_zero_of_le, zero_add, h]
| succ a ih =>
  cases hle: decide (a ≥ (b-c)) with
  | true => 
    simp only [ decide_eq_true_eq] at hle
    rw [Nat.succ_sub hle]
    simp only [tsub_le_iff_right, ge_iff_le] at hle
    rw [Nat.succ_add, Nat.succ_sub hle, ih h]
  | false =>
    simp only [ decide_eq_false_iff_not, not_le] at hle
    have hle₂ := Nat.succ_le_of_lt hle
    rw [Nat.sub_eq_zero_of_le hle₂]
    have hle₃ := Nat.add_le_of_le_sub h hle₂
    rw [Nat.sub_eq_zero_of_le hle₃]
Proof state after:
no goals
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case zero
b c : ℕ
h : c ≤ b
⊢ zero - (b - c) = zero + c - b
Tactic:
simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, tsub_le_iff_right, Nat.zero_sub,
tsub_eq_zero_of_le, zero_add, h]
Proof state after:
no goals
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
⊢ succ a - (b - c) = succ a + c - b
Tactic:
cases hle: decide (a ≥ (b-c)) with
| true => 
  simp only [ decide_eq_true_eq] at hle
  rw [Nat.succ_sub hle]
  simp only [tsub_le_iff_right, ge_iff_le] at hle
  rw [Nat.succ_add, Nat.succ_sub hle, ih h]
| false =>
  simp only [ decide_eq_false_iff_not, not_le] at hle
  have hle₂ := Nat.succ_le_of_lt hle
  rw [Nat.sub_eq_zero_of_le hle₂]
  have hle₃ := Nat.add_le_of_le_sub h hle₂
  rw [Nat.sub_eq_zero_of_le hle₃]
Proof state after:
no goals
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : decide (a ≥ b - c) = true
⊢ succ a - (b - c) = succ a + c - b
Tactic:
simp only [ decide_eq_true_eq] at hle
Proof state after:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ a - (b - c) = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ a - (b - c) = succ a + c - b
Tactic:
rw [Nat.succ_sub hle]
Proof state after:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ (a - (b - c)) = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ (a - (b - c)) = succ a + c - b
Tactic:
simp only [tsub_le_iff_right, ge_iff_le] at hle
Proof state after:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : b ≤ a + c
⊢ succ (a - (b - c)) = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : b ≤ a + c
⊢ succ (a - (b - c)) = succ a + c - b
Tactic:
rw [Nat.succ_add, Nat.succ_sub hle, ih h]
Proof state after:
no goals
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : decide (a ≥ b - c) = false
⊢ succ a - (b - c) = succ a + c - b
Tactic:
simp only [ decide_eq_false_iff_not, not_le] at hle
Proof state after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
⊢ succ a - (b - c) = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
⊢ succ a - (b - c) = succ a + c - b
Tactic:
have hle₂ := Nat.succ_le_of_lt hle
Proof state after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ succ a - (b - c) = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ succ a - (b - c) = succ a + c - b
Tactic:
rw [Nat.sub_eq_zero_of_le hle₂]
Proof state after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ 0 = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ 0 = succ a + c - b
Tactic:
have hle₃ := Nat.add_le_of_le_sub h hle₂
Proof state after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
hle₃ : succ a + c ≤ b
⊢ 0 = succ a + c - b
Theorem: Nat.sub_sub_eq_add_sub_of_le
Proof state before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
hle₃ : succ a + c ≤ b
⊢ 0 = succ a + c - b
Tactic:
rw [Nat.sub_eq_zero_of_le hle₃]
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isPrefixOf delim l = true ↔ delim <+: l
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isPrefixOf delim l = true → delim <+: l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true
Theorem: List.isPrefixOf_ext
Proof state before:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isPrefixOf delim l = true → delim <+: l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true
Tactic:
. intro h
  induction l  generalizing delim
  case nil =>
    unfold isPrefixOf at h
    cases delim <;> simp_all only [isPrefix_self]
  case cons head tail ih =>
    unfold isPrefixOf at h
    cases delim
    case nil => simp only [append_nil, nil_isPrefix]
    case cons dhead dtail =>
      simp at h
      have ⟨h₂,h₃⟩ := h
      have ⟨s, heq⟩  := ih dtail h₃
      exists s
      simp only [h₂, cons_append, heq]
Proof state after:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true
Theorem: List.isPrefixOf_ext
Proof state before:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true
Tactic:
. intro h
  have ⟨s, heq⟩ := h
  rw [← heq]
  clear heq h
  induction delim generalizing l
  case nil =>
    unfold isPrefixOf
    simp only
  case cons head tail ih =>
    unfold isPrefixOf
    simp
    apply ih l
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h : isPrefixOf delim [] = true
⊢ delim <+: []
Tactic:
unfold isPrefixOf at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ delim <+: []
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ delim <+: []
Tactic:
cases delim <;> simp_all only [isPrefix_self]
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
delim : List α
h : isPrefixOf delim (head :: tail) = true
⊢ delim <+: head :: tail
Tactic:
unfold isPrefixOf at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
delim : List α
h :
  (match delim, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ delim <+: head :: tail
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
delim : List α
h :
  (match delim, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ delim <+: head :: tail
Tactic:
cases delim
Proof state after:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
h :
  (match [], head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ [] <+: head :: tail

case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
head✝ : α
tail✝ : List α
h :
  (match head✝ :: tail✝, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ head✝ :: tail✝ <+: head :: tail
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
h :
  (match [], head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ [] <+: head :: tail
Tactic:
case nil => simp only [append_nil, nil_isPrefix]
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h :
  (match dhead :: dtail, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ dhead :: dtail <+: head :: tail
Tactic:
case cons dhead dtail =>
  simp at h
  have ⟨h₂,h₃⟩ := h
  have ⟨s, heq⟩  := ih dtail h₃
  exists s
  simp only [h₂, cons_append, heq]
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
h :
  (match [], head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ [] <+: head :: tail
Tactic:
simp only [append_nil, nil_isPrefix]
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h :
  (match dhead :: dtail, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ dhead :: dtail <+: head :: tail
Tactic:
simp at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail
Tactic:
have ⟨h₂,h₃⟩ := h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail
Tactic:
have ⟨s, heq⟩  := ih dtail h₃
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail <+: head :: tail
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail <+: head :: tail
Tactic:
exists s
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail ++ s = head :: tail
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail ++ s = head :: tail
Tactic:
simp only [h₂, cons_append, heq]
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s l : List α
⊢ isPrefixOf [] ([] ++ s) = true
Tactic:
unfold isPrefixOf
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s l : List α
⊢ (match [], [] ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s l : List α
⊢ (match [], [] ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
Tactic:
simp only
Proof state after:
no goals
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ isPrefixOf (head :: tail) (head :: tail ++ s) = true
Tactic:
unfold isPrefixOf
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ (match head :: tail, head :: tail ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ (match head :: tail, head :: tail ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
Tactic:
simp
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ isPrefixOf tail (tail ++ s) = true
Theorem: List.isPrefixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ isPrefixOf tail (tail ++ s) = true
Tactic:
apply ih l
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isInfixOf delim l = true ↔ delim <:+: l
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isInfixOf delim l = true → delim <:+: l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true
Theorem: List.isInfixOf_ext
Proof state before:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isInfixOf delim l = true → delim <:+: l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true
Tactic:
. intro h
  induction l
  case nil => 
    unfold isInfixOf at h
    split at h
    . simp only [nil_isInfix]
    . simp only at h
    . next heq => simp only at heq
  case cons head tail ih =>
    unfold isInfixOf at h
    simp at h
    cases h with
    | inl heq =>
      simp only [List.isPrefixOf_ext] at heq
      simp only [heq, List.isInfix_of_isPrefix]
    | inr heq =>
      have h₂:= ih heq
      apply List.isInfix_cons h₂
Proof state after:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true
Theorem: List.isInfixOf_ext
Proof state before:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true
Tactic:
. intro h
  have ⟨s,t, heq⟩ := h
  subst heq
  clear h
  induction s
  case nil =>
    unfold isInfixOf
    split
    case h_1 => simp only
    case h_2 hne heq => simp_all only [nil_append, append_eq_nil, forall_true_left]
    case h_3 heq => 
      simp at heq
      rw [← heq]
      simp only [Bool.or_eq_true, List.isPrefixOf_ext]
      left
      exists t
  case cons head tail ih =>
    unfold isInfixOf
    split
    case h_1 heq=>
      simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
    case h_2 hne heq =>
      simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
    case h_3 hd tl heq =>
      simp at heq
      have ⟨h₁, h₂⟩ := heq
      simp only [Bool.or_eq_true]
      right
      rw [ ← h₂]
      rw [append_assoc] at ih
      apply ih
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h : isInfixOf delim [] = true
⊢ delim <:+: []
Tactic:
unfold isInfixOf at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
⊢ delim <:+: []
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
⊢ delim <:+: []
Tactic:
split at h
Proof state after:
case h_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝¹ x✝ : List α
heq✝ : [] = []
h : true = true
⊢ [] <:+: []

case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
heq✝ : [] = []
h : false = true
⊢ x✝³ <:+: []

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Theorem: List.isInfixOf_ext
Proof state before:
case h_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝¹ x✝ : List α
heq✝ : [] = []
h : true = true
⊢ [] <:+: []

case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
heq✝ : [] = []
h : false = true
⊢ x✝³ <:+: []

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
. simp only [nil_isInfix]
Proof state after:
case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
heq✝ : [] = []
h : false = true
⊢ x✝³ <:+: []

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Theorem: List.isInfixOf_ext
Proof state before:
case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
heq✝ : [] = []
h : false = true
⊢ x✝³ <:+: []

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
. simp only at h
Proof state after:
case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Theorem: List.isInfixOf_ext
Proof state before:
case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
. next heq => simp only at heq
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
simp only at heq
Proof state after:
no goals