Theorem: false_proof (meetings/ex6.lean)

State before:
⊢ False
Tactic:
let baldie : Person := ⟨[]⟩
State after:
baldie : Person := { hair := [] }
⊢ False

State before:
baldie : Person := { hair := [] }
⊢ False
Tactic:
have bald : Bald baldie := rfl
State after:
baldie : Person := { hair := [] }
bald : Bald baldie
⊢ False

State before:
baldie : Person := { hair := [] }
bald : Bald baldie
⊢ False
Tactic:
have still_bald := add_one_hair_still_bald bald
State after:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : Bald (add_one_hair baldie)
⊢ False

State before:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : Bald (add_one_hair baldie)
⊢ False
Tactic:
rw [Bald, add_one_hair] at still_bald
State after:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : { hair := Strand.strand :: baldie.hair }.hair = ∅
⊢ False

State before:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : { hair := Strand.strand :: baldie.hair }.hair = ∅
⊢ False
Tactic:
contradiction
State after:
no goals