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

State before:
case zero
p : Nat → Bool
h : (first p).leNat 0 = true
⊢ ∃ y, y ≤ 0 ∧ p y = true
Tactic:
exists 0
State after:
no goals

State before:
case succ
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : (first p).leNat (x + 1) = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Tactic:
simp [first, first.leNat] at h
State after:
case succ
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true ∨ ENat.first.leNat p x = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true

State before:
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Tactic:
exists x+1
State after:
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1 ∧ p (x + 1) = true

State before:
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1 ∧ p (x + 1) = true
Tactic:
constructor
State after:
case succ.inl.left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1

case succ.inl.right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ p (x + 1) = true

State before:
case succ.inl.left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1
Tactic:
exact Nat.le_refl ..
State after:
no goals

State before:
case succ.inl.right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ p (x + 1) = true
Tactic:
exact h
State after:
no goals

State before:
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Tactic:
exists y
State after:
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1 ∧ p y = true

State before:
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1 ∧ p y = true
Tactic:
constructor
State after:
case left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1

case right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ p y = true

State before:
case left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1
Tactic:
exact Nat.le_trans hle (Nat.le_succ ..)
State after:
no goals

State before:
case right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ p y = true
Tactic:
exact hy
State after:
no goals