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

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

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

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

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

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ ∃ x, p x = true
Tactic:
exists x
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ p x = true

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ p x = true
Tactic:
exact find?_eq_some hp
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
⊢ none.isSome = true → ∃ x, p x = true
Tactic:
intro
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isSome = true
⊢ ∃ x, p x = true

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isSome = true
⊢ ∃ x, p x = true
Tactic:
contradiction
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∃ x, p x = true) → (find? p).isSome = true
Tactic:
intro
| ⟨x, hx⟩ =>
  match hp : find? p with
  | some _ =>
    rfl
  | none =>
    rw [find?_eq_none hp] at hx
    contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : p x = true
⊢ (find? p).isSome = true
Tactic:
match hp : find? p with
| some _ =>
  rfl
| none =>
  rw [find?_eq_none hp] at hx
  contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : p x = true
val✝ : α
hp : find? p = some val✝
⊢ (some val✝).isSome = true
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : p x = true
hp : find? p = none
⊢ none.isSome = true
Tactic:
rw [find?_eq_none hp] at hx
State after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : false = true
hp : find? p = none
⊢ none.isSome = true

State before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : false = true
hp : find? p = none
⊢ none.isSome = true
Tactic:
contradiction
State after:
no goals