Theorem: List.join_eq_nil (One.lean)

State before:
α✝ : Type u_1
l : List (List α✝)
h : join l = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Tactic:
induction l with
| nil =>
  simp only [not_mem_nil, IsEmpty.forall_iff, forall_const]
| cons head tail ih=>
  simp_all only [join, append_eq_nil, mem_cons, forall_eq_or_imp, true_and, forall_true_left]
  apply ih
State after:
no goals

State before:
case nil
α✝ : Type u_1
h : join [] = []
⊢ ∀ (e : List α✝), e ∈ [] → e = []
Tactic:
simp only [not_mem_nil, IsEmpty.forall_iff, forall_const]
State after:
no goals

State before:
case cons
α✝ : Type u_1
head : List α✝
tail : List (List α✝)
ih : join tail = [] → ∀ (e : List α✝), e ∈ tail → e = []
h : join (head :: tail) = []
⊢ ∀ (e : List α✝), e ∈ head :: tail → e = []
Tactic:
simp_all only [join, append_eq_nil, mem_cons, forall_eq_or_imp, true_and, forall_true_left]
State after:
case cons
α✝ : Type u_1
head : List α✝
tail : List (List α✝)
ih : ∀ (e : List α✝), e ∈ tail → e = []
h : head = [] ∧ join tail = []
⊢ ∀ (a : List α✝), a ∈ tail → a = []

State before:
case cons
α✝ : Type u_1
head : List α✝
tail : List (List α✝)
ih : ∀ (e : List α✝), e ∈ tail → e = []
h : head = [] ∧ join tail = []
⊢ ∀ (a : List α✝), a ∈ tail → a = []
Tactic:
apply ih
State after:
no goals