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

State before:
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] ↔ xs = [] ∧ ys = []
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] → xs = [] ∧ ys = []

case mpr
α : Type u_1
xs ys : List α
⊢ xs = [] ∧ ys = [] → xs ++ ys = []

State before:
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] → xs = [] ∧ ys = []
Tactic:
case mp =>
  cases xs with
  | nil =>
    simp only [nil_append, true_and, imp_self]
  | cons head tail =>
    intro h'
    contradiction
State after:
no goals

State before:
α : Type u_1
xs ys : List α
⊢ xs = [] ∧ ys = [] → xs ++ ys = []
Tactic:
case mpr =>
  intro h'
  cases h' with
  | intro h1 h2 =>
    rw [h1, h2]
    rfl
State after:
no goals

State before:
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] → xs = [] ∧ ys = []
Tactic:
cases xs with
| nil =>
  simp only [nil_append, true_and, imp_self]
| cons head tail =>
  intro h'
  contradiction
State after:
no goals

State before:
case nil
α : Type u_1
ys : List α
⊢ [] ++ ys = [] → [] = [] ∧ ys = []
Tactic:
simp only [nil_append, true_and, imp_self]
State after:
no goals

State before:
case cons
α : Type u_1
ys : List α
head : α
tail : List α
⊢ head :: tail ++ ys = [] → head :: tail = [] ∧ ys = []
Tactic:
intro h'
State after:
case cons
α : Type u_1
ys : List α
head : α
tail : List α
h' : head :: tail ++ ys = []
⊢ head :: tail = [] ∧ ys = []

State before:
case cons
α : Type u_1
ys : List α
head : α
tail : List α
h' : head :: tail ++ ys = []
⊢ head :: tail = [] ∧ ys = []
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
xs ys : List α
⊢ xs = [] ∧ ys = [] → xs ++ ys = []
Tactic:
intro h'
State after:
α : Type u_1
xs ys : List α
h' : xs = [] ∧ ys = []
⊢ xs ++ ys = []

State before:
α : Type u_1
xs ys : List α
h' : xs = [] ∧ ys = []
⊢ xs ++ ys = []
Tactic:
cases h' with
| intro h1 h2 =>
  rw [h1, h2]
  rfl
State after:
no goals

State before:
case intro
α : Type u_1
xs ys : List α
h1 : xs = []
h2 : ys = []
⊢ xs ++ ys = []
Tactic:
rw [h1, h2]
State after:
case intro
α : Type u_1
xs ys : List α
h1 : xs = []
h2 : ys = []
⊢ [] ++ [] = []

State before:
case intro
α : Type u_1
xs ys : List α
h1 : xs = []
h2 : ys = []
⊢ [] ++ [] = []
Tactic:
rfl
State after:
no goals