-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem prefix_take_iff {x y : List α} {n : Nat} : x <+: y.take n ↔ x <+: y ∧ x.length ≤ n

Proof state:
case mp.right
α : Type u_1
x y : List α
n : Nat
h : x <+: take n y
⊢ x.length ≤ n

Tactic:
replace h := h.length_le

Result:
case mp.right
α : Type u_1
x y : List α
n : Nat
h : x.length ≤ (take n y).length
⊢ x.length ≤ n

Proof state:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x = take x.length y
hl : x.length ≤ n
hl' : x.length ≤ y.length
⊢ take x.length y = take (min (take x.length y).length n) y

Tactic:
simp [Nat.min_eq_left, hl, hl']

Result:
no goals

Proof state:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x = take x.length y
hl : x.length ≤ n
hl' : x.length ≤ y.length
⊢ x = take x.length (take n y)

Tactic:
rw [hp, List.take_take]

Result:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x = take x.length y
hl : x.length ≤ n
hl' : x.length ≤ y.length
⊢ take x.length y = take (min (take x.length y).length n) y

Proof state:
case mp.left
α : Type u_1
x y : List α
n : Nat
h : x <+: take n y
⊢ x <+: y

Tactic:
exact List.IsPrefix.trans h <| List.take_prefix n y

Result:
no goals

Proof state:
case mp.right
α : Type u_1
x y : List α
n : Nat
h : x.length ≤ n ∧ x.length ≤ y.length
⊢ x.length ≤ n

Tactic:
exact h.left

Result:
no goals

Proof state:
case mp
α : Type u_1
x y : List α
n : Nat
h : x <+: take n y
⊢ x <+: y ∧ x.length ≤ n

Tactic:
constructor

Result:
case mp.left
α : Type u_1
x y : List α
n : Nat
h : x <+: take n y
⊢ x <+: y

case mp.right
α : Type u_1
x y : List α
n : Nat
h : x <+: take n y
⊢ x.length ≤ n

Proof state:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x <+: y
hl : x.length ≤ n
⊢ x <+: take n y

Tactic:
have hl' := hp.length_le

Result:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x <+: y
hl : x.length ≤ n
hl' : x.length ≤ y.length
⊢ x <+: take n y

Proof state:
case mp.right
α : Type u_1
x y : List α
n : Nat
h : x.length ≤ (take n y).length
⊢ x.length ≤ n

Tactic:
rw [length_take, Nat.le_min] at h

Result:
case mp.right
α : Type u_1
x y : List α
n : Nat
h : x.length ≤ n ∧ x.length ≤ y.length
⊢ x.length ≤ n

Proof state:
case mpr
α : Type u_1
x y : List α
n : Nat
⊢ x <+: y ∧ x.length ≤ n → x <+: take n y

Tactic:
intro ⟨hp, hl⟩

Result:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x <+: y
hl : x.length ≤ n
⊢ x <+: take n y

Proof state:
α : Type u_1
x y : List α
n : Nat
⊢ x <+: take n y ↔ x <+: y ∧ x.length ≤ n

Tactic:
constructor

Result:
case mp
α : Type u_1
x y : List α
n : Nat
⊢ x <+: take n y → x <+: y ∧ x.length ≤ n

case mpr
α : Type u_1
x y : List α
n : Nat
⊢ x <+: y ∧ x.length ≤ n → x <+: take n y

Proof state:
case mp
α : Type u_1
x y : List α
n : Nat
⊢ x <+: take n y → x <+: y ∧ x.length ≤ n

Tactic:
intro h

Result:
case mp
α : Type u_1
x y : List α
n : Nat
h : x <+: take n y
⊢ x <+: y ∧ x.length ≤ n

Proof state:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x <+: y
hl : x.length ≤ n
hl' : x.length ≤ y.length
⊢ x <+: take n y

Tactic:
rw [List.prefix_iff_eq_take] at *

Result:
case mpr
α : Type u_1
x y : List α
n : Nat
hp : x = take x.length y
hl : x.length ≤ n
hl' : x.length ≤ y.length
⊢ x = take x.length (take n y)