Theorem: ENat.first_leNat_iff_exists_le (GMLInit/Data/Nat/Extended/First.lean)

State before:
p : Nat → Bool
x : Nat
⊢ (first p).leNat x = true ↔ ∃ y, y ≤ x ∧ p y = true
Tactic:
constructor
State after:
case mp
p : Nat → Bool
x : Nat
⊢ (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true

case mpr
p : Nat → Bool
x : Nat
⊢ (∃ y, y ≤ x ∧ p y = true) → (first p).leNat x = true

State before:
case mp
p : Nat → Bool
x : Nat
⊢ (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
Tactic:
exact exists_le_first_of_first_leNat
State after:
no goals

State before:
case mpr
p : Nat → Bool
x : Nat
⊢ (∃ y, y ≤ x ∧ p y = true) → (first p).leNat x = true
Tactic:
intro ⟨y, hle, hy⟩
State after:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat x = true

State before:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat x = true
Tactic:
apply mono hle
State after:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat y = true

State before:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat y = true
Tactic:
exact first_leNat_of hy
State after:
no goals