Theorem: List.splitOn_append (One.lean)

State before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ splitOn delim (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOn delim l₁)
Tactic:
unfold splitOn
State after:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ splitOnP (fun x => x == delim) (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP (fun x => x == delim) l₁)

State before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ splitOnP (fun x => x == delim) (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP (fun x => x == delim) l₁)
Tactic:
rw [List.splitOnP_append]
State after:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true

State before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
Tactic:
intro e ein
State after:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
e : α
ein : e ∈ l₂
⊢ ¬(e == delim) = true

State before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
e : α
ein : e ∈ l₂
⊢ ¬(e == delim) = true
Tactic:
exact h e ein
State after:
no goals