Theorem: ENat.leNat_toNatAux (GMLInit/Data/Nat/Extended/Finite.lean)

State before:
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (ENat.toNatAux isFinite x) = true
Tactic:
rw [toNatAux_eq]
State after:
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (if e.leNat x = true then x else ENat.toNatAux isFinite (x + 1)) = true

State before:
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (if e.leNat x = true then x else ENat.toNatAux isFinite (x + 1)) = true
Tactic:
split
State after:
case isTrue
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : e.leNat x = true
⊢ e.leNat x = true

case isFalse
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : ¬e.leNat x = true
⊢ e.leNat (ENat.toNatAux isFinite (x + 1)) = true

State before:
case isTrue
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : e.leNat x = true
⊢ e.leNat x = true
Tactic:
assumption
State after:
no goals

State before:
case isFalse
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : ¬e.leNat x = true
⊢ e.leNat (ENat.toNatAux isFinite (x + 1)) = true
Tactic:
apply leNat_toNatAux
State after:
no goals

State before:
e : ENat
isFinite : e.IsFinite
x : Nat
a✝ : ∀ (y : Nat), (invImage (fun x => ⋯.wrap x) Acc.wfRel).1 y x → e.leNat (ENat.toNatAux isFinite y) = true
h✝ : ¬e.leNat x = true
⊢ (invImage (fun x => ⋯.wrap x) Acc.wfRel).1 (x + 1) x
Tactic:
trivial
State after:
no goals