Theorem: Find.find_is_none_iff_forall_false (Extra/Find.lean)

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isNone = true ↔ ∀ (x : α), p x = false
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isNone = true → ∀ (x : α), p x = false

case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∀ (x : α), p x = false) → (find? p).isNone = true

State before:
case mp
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isNone = true → ∀ (x : α), p x = false
Tactic:
match hp : find? p with
| some x =>
  intro _
  contradiction
| none =>
  intro _ x
  exact find?_eq_none hp
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
⊢ (some x).isNone = true → ∀ (x : α), p x = false
Tactic:
intro _
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isNone = true
⊢ ∀ (x : α), p x = false

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isNone = true
⊢ ∀ (x : α), p x = false
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
⊢ none.isNone = true → ∀ (x : α), p x = false
Tactic:
intro _ x
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isNone = true
x : α
⊢ p x = false

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isNone = true
x : α
⊢ p x = false
Tactic:
exact find?_eq_none hp
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∀ (x : α), p x = false) → (find? p).isNone = true
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
⊢ (find? p).isNone = true

State before:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
⊢ (find? p).isNone = true
Tactic:
match hp : find? p with
| some x =>
  absurd find?_eq_some hp
  rw [h]
  intro
  contradiction
| none =>
  rfl
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ (some x).isNone = true
Tactic:
absurd find?_eq_some hp
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬p x = true

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬p x = true
Tactic:
rw [h]
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬false = true

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬false = true
Tactic:
intro
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
a✝ : false = true
⊢ False

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
a✝ : false = true
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
hp : find? p = none
⊢ none.isNone = true
Tactic:
rfl
State after:
no goals