case h.e'_2
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n) l = take (m + n) (take m l ++ drop m l)

ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l)
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n) l = take m l ++ take n (drop m l)
convert_to take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l)
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n - length (take m l)) (drop m l) = take n (drop m l)

ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ length (take m l) ≤ m + n
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l)
rw [take_append_eq_append_take, take_all_of_le, append_right_inj]
no goals
case h.e'_2
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n) l = take (m + n) (take m l ++ drop m l)
rw [take_append_drop]
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ min (m + n - min m (length l)) (length l - m) = min n (length l - m)
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ take (m + n - length (take m l)) (drop m l) = take n (drop m l)
simp only [take_eq_take, length_take, length_drop]
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
⊢ min (m + n - min m k) (k - m) = min n (k - m)
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ min (m + n - min m (length l)) (length l - m) = min n (length l - m)
generalize l.length = k
case pos
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
h : m ≤ k
⊢ min (m + n - min m k) (k - m) = min n (k - m)

case neg
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
h : ¬m ≤ k
⊢ min (m + n - min m k) (k - m) = min n (k - m)
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
⊢ min (m + n - min m k) (k - m) = min n (k - m)
by_cases h : m ≤ k
no goals
case pos
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
h : m ≤ k
⊢ min (m + n - min m k) (k - m) = min n (k - m)
simp [min_eq_left_iff.mpr h]
case neg
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
h : k < m
⊢ min (m + n - min m k) (k - m) = min n (k - m)
case neg
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
h : ¬m ≤ k
⊢ min (m + n - min m k) (k - m) = min n (k - m)
push_neg  at h
no goals
case neg
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n k : ℕ
h : k < m
⊢ min (m + n - min m k) (k - m) = min n (k - m)
simp [Nat.sub_eq_zero_of_le (le_of_lt h)]
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ length (take m l) ≤ m

ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ m ≤ m + n
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ length (take m l) ≤ m + n
trans m
no goals
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ length (take m l) ≤ m
apply length_take_le
no goals
ι : Type ?u.185033
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
m n : ℕ
⊢ m ≤ m + n
simp