Theorem: list_prefix_is_gt_zero_and_leq (Katydid/Std/Lists.lean)

State before:
α : Type u_1
⊢ ∀ (xs ys zs : List α), xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Tactic:
intro xs ys zs
State after:
α : Type u_1
xs ys zs : List α
⊢ xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs

State before:
α : Type u_1
xs ys zs : List α
⊢ xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Tactic:
revert xs ys
State after:
α : Type u_1
zs : List α
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs

State before:
α : Type u_1
zs : List α
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Tactic:
cases zs with
| nil =>
  intro xs ys hneq ha
  rw [list_app_nil_nil] at ha
  cases ha with
  | intro hxs hys =>
    contradiction
| cons z zs =>
  intro xs ys hneq ha
  have hl := list_length_gt_zero _ hneq
  rw [<- ha]
  apply And.intro
  case left =>
    exact hl
  case right =>
    rw [list_app_length]
    apply Nat.le_add_right
State after:
no goals

State before:
case nil
α : Type u_1
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = [] → 0 < length xs ∧ length xs ≤ length []
Tactic:
intro xs ys hneq ha
State after:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []

State before:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Tactic:
rw [list_app_nil_nil] at ha
State after:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs = [] ∧ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []

State before:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs = [] ∧ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Tactic:
cases ha with
| intro hxs hys =>
  contradiction
State after:
no goals

State before:
case nil.intro
α : Type u_1
xs ys : List α
hneq : xs ≠ []
hxs : xs = []
hys : ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
z : α
zs : List α
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = z :: zs → 0 < length xs ∧ length xs ≤ length (z :: zs)
Tactic:
intro xs ys hneq ha
State after:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)

State before:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)
Tactic:
have hl := list_length_gt_zero _ hneq
State after:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)

State before:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)
Tactic:
rw [<- ha]
State after:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (xs ++ ys)

State before:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (xs ++ ys)
Tactic:
apply And.intro
State after:
case cons.left
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs

case cons.right
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length (xs ++ ys)

State before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs
Tactic:
case left =>
  exact hl
State after:
no goals

State before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length (xs ++ ys)
Tactic:
case right =>
  rw [list_app_length]
  apply Nat.le_add_right
State after:
no goals

State before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs
Tactic:
exact hl
State after:
no goals

State before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length (xs ++ ys)
Tactic:
rw [list_app_length]
State after:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length xs + length ys

State before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length xs + length ys
Tactic:
apply Nat.le_add_right
State after:
no goals