Theorem: List.isInfix_length (One.lean)

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ length l₁ ≤ length l₂
Tactic:
have ⟨s,t, heq⟩ := h
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ length l₁ ≤ length l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ length l₁ ≤ length l₂
Tactic:
apply_fun @length α at heq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₂
Tactic:
rw [← heq]
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length (s ++ l₁ ++ t)

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length (s ++ l₁ ++ t)
Tactic:
rw [length_append, length_append,  add_comm (length s), add_assoc]
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₁ + (length s + length t)

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₁ + (length s + length t)
Tactic:
apply Nat.le_add_right
State after:
no goals