α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h this : map f l = s₁ ++ s₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
have := h
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l ++ drop (length s₁) l) = s₁ ++ s₂
⊢ ∃ l₁ l₂, take (length s₁) l ++ drop (length s₁) l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h this : map f l = s₁ ++ s₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
rw [← take_append_drop (length s₁) l] at this ⊢
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ ∃ l₁ l₂, take (length s₁) l ++ drop (length s₁) l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l ++ drop (length s₁) l) = s₁ ++ s₂
⊢ ∃ l₁ l₂, take (length s₁) l ++ drop (length s₁) l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
rw [map_append] at this
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ length (map f (take (length s₁) l)) = length s₁
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ ∃ l₁ l₂, take (length s₁) l ++ drop (length s₁) l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂
refine ⟨_, _, rfl, append_inj this ?_⟩
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ length s₁ ≤ length l
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ length (map f (take (length s₁) l)) = length s₁
rw [length_map, length_take, Nat.min_eq_left]
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ length s₁ ≤ length s₁ + length s₂
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ length s₁ ≤ length l
rw [← length_map l f, h, length_append]
no goals
α : Type u_1
β : Type u_2
f : α → β
l : List α
s₁ s₂ : List β
h : map f l = s₁ ++ s₂
this : map f (take (length s₁) l) ++ map f (drop (length s₁) l) = s₁ ++ s₂
⊢ length s₁ ≤ length s₁ + length s₂
apply Nat.le_add_right