Theorem: List.nil_iff (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
l : List α
⊢ l = [] ↔ ∀ (a : α), a ∉ l
Tactic:
induction l with
| nil => simp only [not_mem_nil, not_false_eq_true, implies_true];
| cons a _ _ =>
  simp_all only [mem_cons, not_or, false_iff, not_forall, not_and, not_not];
  use a;
  tauto;
State after:
no goals

State before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
⊢ [] = [] ↔ ∀ (a : α), a ∉ []
Tactic:
simp only [not_mem_nil, not_false_eq_true, implies_true]
State after:
no goals

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ a :: tail✝ = [] ↔ ∀ (a_1 : α), a_1 ∉ a :: tail✝
Tactic:
simp_all only [mem_cons, not_or, false_iff, not_forall, not_and, not_not]
State after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ∃ x, ¬x = a → x ∈ tail✝

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ∃ x, ¬x = a → x ∈ tail✝
Tactic:
use a
State after:
case h
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ¬a = a → a ∈ tail✝

State before:
case h
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ¬a = a → a ∈ tail✝
Tactic:
tauto
State after:
no goals