Theorem: List.induction_with_singleton (Logic/Logic/LogicSymbol.lean)

State before:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
⊢ ∀ (as : List F), motive as
Tactic:
intro as
State after:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
as : List F
⊢ motive as

State before:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
as : List F
⊢ motive as
Tactic:
induction as with
| nil => exact hnil;
| cons a as ih => cases as with
  | nil => exact hsingle a;
  | cons b bs => exact hcons a (b :: bs) (by simp) ih;
State after:
no goals

State before:
case nil
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
⊢ motive []
Tactic:
exact hnil
State after:
no goals

State before:
case cons
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a : F
as : List F
ih : motive as
⊢ motive (a :: as)
Tactic:
cases as with
| nil => exact hsingle a;
| cons b bs => exact hcons a (b :: bs) (by simp) ih;
State after:
no goals

State before:
case cons.nil
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a : F
ih : motive []
⊢ motive [a]
Tactic:
exact hsingle a
State after:
no goals

State before:
case cons.cons
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a b : F
bs : List F
ih : motive (b :: bs)
⊢ motive (a :: b :: bs)
Tactic:
exact hcons a (b :: bs) (by simp) ih
State after:
no goals

State before:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a b : F
bs : List F
ih : motive (b :: bs)
⊢ b :: bs ≠ []
Tactic:
simp
State after:
no goals