Theorem: all_people_bald (meetings/ex6.lean)

State before:
⊢ ∀ (person : Person), Bald person
Tactic:
intro person
State after:
person : Person
⊢ Bald person

State before:
person : Person
⊢ Bald person
Tactic:
rw [Bald]
State after:
person : Person
⊢ person.hair = ∅

State before:
person : Person
⊢ person.hair = ∅
Tactic:
induction' person.hair with _ h ih
State after:
case nil
person : Person
⊢ [] = ∅

case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
⊢ head✝ :: h = ∅

State before:
case nil
person : Person
⊢ [] = ∅
Tactic:
rfl
State after:
no goals

State before:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
⊢ head✝ :: h = ∅
Tactic:
have baldie := add_one_hair_still_bald ih
State after:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : Bald (add_one_hair { hair := h })
⊢ head✝ :: h = ∅

State before:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : Bald (add_one_hair { hair := h })
⊢ head✝ :: h = ∅
Tactic:
rw [add_one_hair, Bald] at baldie
State after:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : { hair := Strand.strand :: { hair := h }.hair }.hair = ∅
⊢ head✝ :: h = ∅

State before:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : { hair := Strand.strand :: { hair := h }.hair }.hair = ∅
⊢ head✝ :: h = ∅
Tactic:
exact baldie
State after:
no goals