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

State before:
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ ENat.toNatAux ⋯ x ≤ y
Tactic:
rw [toNatAux_eq]
State after:
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ (if e.leNat x = true then x else ENat.toNatAux ⋯ (x + 1)) ≤ y

State before:
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ (if e.leNat x = true then x else ENat.toNatAux ⋯ (x + 1)) ≤ y
Tactic:
split
State after:
case isTrue
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : e.leNat x = true
⊢ x ≤ y

case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ENat.toNatAux ⋯ (x + 1) ≤ y

State before:
case isTrue
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : e.leNat x = true
⊢ x ≤ y
Tactic:
exact hle
State after:
no goals

State before:
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ENat.toNatAux ⋯ (x + 1) ≤ y
Tactic:
apply toNatAux_le hy
State after:
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x + 1 ≤ y

State before:
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x + 1 ≤ y
Tactic:
apply Nat.succ_le_of_lt
State after:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x < y

State before:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x < y
Tactic:
apply Nat.lt_of_le_of_ne hle
State after:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ¬x = y

State before:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ¬x = y
Tactic:
intro | rfl => contradiction
State after:
no goals

State before:
y : Nat
e : ENat
x : Nat
h✝ : ¬e.leNat x = true
x✝ : x = y
hy : e.leNat x = true
hle : x ≤ x
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
y : Nat
e : ENat
hy : e.leNat y = true
x✝ : (x : Nat) ×' x ≤ y
a✝¹ :
  ∀ (y_1 : (x : Nat) ×' x ≤ y),
    (invImage (fun x => PSigma.casesOn x fun x hle => ⋯.wrap x) Acc.wfRel).1 y_1 x✝ → ENat.toNatAux ⋯ y_1.1 ≤ y
x : Nat
hle : x ≤ y
a✝ :
  ∀ (y_1 : (x : Nat) ×' x ≤ y),
    (invImage (fun x => PSigma.casesOn x fun x hle => ⋯.wrap x) Acc.wfRel).1 y_1 ⟨x, hle⟩ → ENat.toNatAux ⋯ y_1.1 ≤ y
h✝ : ¬e.leNat x = true
⊢ (invImage (fun x => PSigma.casesOn x fun x hle => ⋯.wrap x) Acc.wfRel).1 ⟨x + 1, ⋯⟩ ⟨x, hle⟩
Tactic:
trivial
State after:
no goals