internlm/Lean-Github huggingface dataset:
Theorem: ENat.not_lt
Proof state before:
x y : ENat
⊢ ¬x < y ↔ y ≤ x
Tactic:
constructor
Proof state after:
case mp
x y : ENat
⊢ ¬x < y → y ≤ x

case mpr
x y : ENat
⊢ y ≤ x → ¬x < y
Theorem: ENat.not_lt
Proof state before:
case mp
x y : ENat
⊢ ¬x < y → y ≤ x
Tactic:
intro h n
Proof state after:
case mp
x y : ENat
h : ¬x < y
n : Nat
⊢ y.leNat n = true ∨ x.leNat n = false
Theorem: ENat.not_lt
Proof state before:
case mp
x y : ENat
h : ¬x < y
n : Nat
⊢ y.leNat n = true ∨ x.leNat n = false
Tactic:
match hx : x.leNat n, hy : y.leNat n with
| false, _ => right; rfl
| _, true => left; rfl
| true, false => absurd h; exists n
Proof state after:
no goals
Theorem: ENat.not_lt
Proof state before:
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = false
hy : y.leNat n = x✝
⊢ x✝ = true ∨ false = false
Tactic:
right
Proof state after:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = false
hy : y.leNat n = x✝
⊢ false = false
Theorem: ENat.not_lt
Proof state before:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = false
hy : y.leNat n = x✝
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: ENat.not_lt
Proof state before:
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = x✝
hy : y.leNat n = true
⊢ true = true ∨ x✝ = false
Tactic:
left
Proof state after:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = x✝
hy : y.leNat n = true
⊢ true = true
Theorem: ENat.not_lt
Proof state before:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = x✝
hy : y.leNat n = true
⊢ true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: ENat.not_lt
Proof state before:
x y : ENat
h : ¬x < y
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ false = true ∨ true = false
Tactic:
absurd h
Proof state after:
x y : ENat
h : ¬x < y
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ x < y
Theorem: ENat.not_lt
Proof state before:
x y : ENat
h : ¬x < y
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ x < y
Tactic:
exists n
Proof state after:
no goals
Theorem: ENat.not_lt
Proof state before:
case mpr
x y : ENat
⊢ y ≤ x → ¬x < y
Tactic:
intro h ⟨n₀, hx, hy⟩
Proof state after:
case mpr
x y : ENat
h : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
⊢ False
Theorem: ENat.not_lt
Proof state before:
case mpr
x y : ENat
h : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
⊢ False
Tactic:
cases h n₀ with
| inl h => simp only [h] at hy
| inr h => simp only [h] at hx
Proof state after:
no goals
Theorem: ENat.not_lt
Proof state before:
case mpr.inl
x y : ENat
h✝ : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
h : y.leNat n₀ = true
⊢ False
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.not_lt
Proof state before:
case mpr.inr
x y : ENat
h✝ : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
h : x.leNat n₀ = false
⊢ False
Tactic:
simp only [h] at hx
Proof state after:
no goals
Theorem: ENat.zero_le
Proof state before:
x : ENat
⊢ 0 ≤ x
Tactic:
intro n
Proof state after:
x : ENat
n : Nat
⊢ leNat 0 n = true ∨ x.leNat n = false
Theorem: ENat.zero_le
Proof state before:
x : ENat
n : Nat
⊢ leNat 0 n = true ∨ x.leNat n = false
Tactic:
simp only [OfNat.ofNat, leNat_coe_eq_true_iff_le]
Proof state after:
x : ENat
n : Nat
⊢ 0 ≤ n ∨ x.leNat n = false
Theorem: ENat.zero_le
Proof state before:
x : ENat
n : Nat
⊢ 0 ≤ n ∨ x.leNat n = false
Tactic:
left
Proof state after:
case h
x : ENat
n : Nat
⊢ 0 ≤ n
Theorem: ENat.zero_le
Proof state before:
case h
x : ENat
n : Nat
⊢ 0 ≤ n
Tactic:
exact Nat.zero_le ..
Proof state after:
no goals
Theorem: ENat.le_infinity
Proof state before:
x : ENat
⊢ x ≤ ∞
Tactic:
intro n
Proof state after:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ ∞.leNat n = false
Theorem: ENat.le_infinity
Proof state before:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ ∞.leNat n = false
Tactic:
right
Proof state after:
case h
x : ENat
n : Nat
⊢ ∞.leNat n = false
Theorem: ENat.le_infinity
Proof state before:
case h
x : ENat
n : Nat
⊢ ∞.leNat n = false
Tactic:
rfl
Proof state after:
no goals
Theorem: ENat.le_refl
Proof state before:
x : ENat
⊢ x ≤ x
Tactic:
intro n
Proof state after:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ x.leNat n = false
Theorem: ENat.le_refl
Proof state before:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ x.leNat n = false
Tactic:
cases x.leNat n <;> trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
⊢ x ≤ y → y ≤ z → x ≤ z
Tactic:
intro hxy hyz n
Proof state after:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
⊢ x.leNat n = true ∨ z.leNat n = false
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
⊢ x.leNat n = true ∨ z.leNat n = false
Tactic:
match hx : x.leNat n, hy : y.leNat n, hz : z.leNat n with
| true, true, true => trivial
| true, true, false => trivial
| true, false, true => trivial
| true, false, false => trivial
| false, true, true =>
  cases hxy n with
  | inl h => simp only [h] at hx
  | inr h => simp only [h] at hy
| false, true, false => trivial
| false, false, true =>
  cases hyz n with
  | inl h => simp only [h] at hy
  | inr h => simp only [h] at hz
| false, false, false => trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = true
hz : z.leNat n = true
⊢ true = true ∨ true = false
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = true
hz : z.leNat n = false
⊢ true = true ∨ false = false
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hz : z.leNat n = true
⊢ true = true ∨ true = false
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hz : z.leNat n = false
⊢ true = true ∨ false = false
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
hz : z.leNat n = true
⊢ false = true ∨ true = false
Tactic:
cases hxy n with
| inl h => simp only [h] at hx
| inr h => simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
case inl
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
hz : z.leNat n = true
h : x.leNat n = true
⊢ false = true ∨ true = false
Tactic:
simp only [h] at hx
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
case inr
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
hz : z.leNat n = true
h : y.leNat n = false
⊢ false = true ∨ true = false
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
hz : z.leNat n = false
⊢ false = true ∨ false = false
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
hz : z.leNat n = true
⊢ false = true ∨ true = false
Tactic:
cases hyz n with
| inl h => simp only [h] at hy
| inr h => simp only [h] at hz
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
case inl
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
hz : z.leNat n = true
h : y.leNat n = true
⊢ false = true ∨ true = false
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
case inr
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
hz : z.leNat n = true
h : z.leNat n = false
⊢ false = true ∨ true = false
Tactic:
simp only [h] at hz
Proof state after:
no goals
Theorem: ENat.le_trans
Proof state before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
hz : z.leNat n = false
⊢ false = true ∨ false = false
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
x y : ENat
⊢ x ≤ y → y ≤ x → x = y
Tactic:
intro hxy hyx
Proof state after:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
⊢ x = y
Theorem: ENat.le_antisymm
Proof state before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
⊢ x = y
Tactic:
ext n
Proof state after:
case leNat.h
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
⊢ x.leNat n = y.leNat n
Theorem: ENat.le_antisymm
Proof state before:
case leNat.h
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
⊢ x.leNat n = y.leNat n
Tactic:
match hx : x.leNat n, hy : y.leNat n with
| true, true => rfl
| true, false =>
  cases hyx n with
  | inl h => simp only [h] at hy
  | inr h => simp only [h] at hx
| false, true =>
  cases hxy n with
  | inl h => simp only [h] at hx
  | inr h => simp only [h] at hy
| false, false => rfl
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = true
⊢ true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ true = false
Tactic:
cases hyx n with
| inl h => simp only [h] at hy
| inr h => simp only [h] at hx
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
case inl
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
h : y.leNat n = true
⊢ true = false
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
case inr
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
h : x.leNat n = false
⊢ true = false
Tactic:
simp only [h] at hx
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
⊢ false = true
Tactic:
cases hxy n with
| inl h => simp only [h] at hx
| inr h => simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
case inl
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
h : x.leNat n = true
⊢ false = true
Tactic:
simp only [h] at hx
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
case inr
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
h : y.leNat n = false
⊢ false = true
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.le_antisymm
Proof state before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: ENat.le_of_lt
Proof state before:
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
⊢ x ≤ y
Tactic:
intro n
Proof state after:
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
⊢ x.leNat n = true ∨ y.leNat n = false
Theorem: ENat.le_of_lt
Proof state before:
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
⊢ x.leNat n = true ∨ y.leNat n = false
Tactic:
cases Nat.le_total n n₀ with
| inl h => right; exact mono' h hy
| inr h => left; exact mono h hx
Proof state after:
no goals
Theorem: ENat.le_of_lt
Proof state before:
case inl
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n ≤ n₀
⊢ x.leNat n = true ∨ y.leNat n = false
Tactic:
right
Proof state after:
case inl.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n ≤ n₀
⊢ y.leNat n = false
Theorem: ENat.le_of_lt
Proof state before:
case inl.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n ≤ n₀
⊢ y.leNat n = false
Tactic:
exact mono' h hy
Proof state after:
no goals
Theorem: ENat.le_of_lt
Proof state before:
case inr
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true ∨ y.leNat n = false
Tactic:
left
Proof state after:
case inr.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true
Theorem: ENat.le_of_lt
Proof state before:
case inr.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true
Tactic:
exact mono h hx
Proof state after:
no goals
Theorem: ENat.lt_irrefl
Proof state before:
x : ENat
⊢ ¬x < x
Tactic:
rw [ENat.not_lt]
Proof state after:
x : ENat
⊢ x ≤ x
Theorem: ENat.lt_irrefl
Proof state before:
x : ENat
⊢ x ≤ x
Tactic:
exact le_refl _
Proof state after:
no goals
Theorem: ENat.lt_of_le_of_lt
Proof state before:
x y z : ENat
⊢ x ≤ y → y < z → x < z
Tactic:
intro hxy ⟨n, hy, hz⟩
Proof state after:
x y z : ENat
hxy : x ≤ y
n : Nat
hy : y.leNat n = true
hz : z.leNat n = false
⊢ x < z
Theorem: ENat.lt_of_le_of_lt
Proof state before:
x y z : ENat
hxy : x ≤ y
n : Nat
hy : y.leNat n = true
hz : z.leNat n = false
⊢ x < z
Tactic:
cases hxy n with
| inl hx => exists n
| inr h => simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.lt_of_le_of_lt
Proof state before:
case inl
x y z : ENat
hxy : x ≤ y
n : Nat
hy : y.leNat n = true
hz : z.leNat n = false
hx : x.leNat n = true
⊢ x < z
Tactic:
exists n
Proof state after:
no goals
Theorem: ENat.lt_of_le_of_lt
Proof state before:
case inr
x y z : ENat
hxy : x ≤ y
n : Nat
hy : y.leNat n = true
hz : z.leNat n = false
h : y.leNat n = false
⊢ x < z
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.lt_of_lt_of_le
Proof state before:
x y z : ENat
⊢ x < y → y ≤ z → x < z
Tactic:
intro ⟨n, hx, hy⟩ hyz
Proof state after:
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
⊢ x < z
Theorem: ENat.lt_of_lt_of_le
Proof state before:
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
⊢ x < z
Tactic:
cases hyz n with
| inl h => simp only [h] at hy
| inr hz => exists n
Proof state after:
no goals
Theorem: ENat.lt_of_lt_of_le
Proof state before:
case inl
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
h : y.leNat n = true
⊢ x < z
Tactic:
simp only [h] at hy
Proof state after:
no goals
Theorem: ENat.lt_of_lt_of_le
Proof state before:
case inr
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
hz : z.leNat n = false
⊢ x < z
Tactic:
exists n
Proof state after:
no goals
Theorem: ENat.lt_trans
Proof state before:
x y z : ENat
⊢ x < y → y < z → x < z
Tactic:
intro hxy hyz
Proof state after:
x y z : ENat
hxy : x < y
hyz : y < z
⊢ x < z
Theorem: ENat.lt_trans
Proof state before:
x y z : ENat
hxy : x < y
hyz : y < z
⊢ x < z
Tactic:
exact lt_of_lt_of_le hxy (le_of_lt hyz)
Proof state after:
no goals
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
x : ENat
n : Nat
⊢ x.leNat n = true → x ≤ ENat.ofNat n
Tactic:
intro h k
Proof state after:
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Tactic:
cases Nat.lt_or_ge k n with
| inl hlt => right; rw [leNat_coe_eq_false_iff_gt]; exact hlt
| inr hge => left; exact mono hge h
Proof state after:
no goals
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
case inl
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Tactic:
right
Proof state after:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ (ENat.ofNat n).leNat k = false
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ (ENat.ofNat n).leNat k = false
Tactic:
rw [leNat_coe_eq_false_iff_gt]
Proof state after:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ k < n
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ k < n
Tactic:
exact hlt
Proof state after:
no goals
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
case inr
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hge : k ≥ n
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Tactic:
left
Proof state after:
case inr.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hge : k ≥ n
⊢ x.leNat k = true
Theorem: ENat.le_coe_of_leNat_eq_true
Proof state before:
case inr.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hge : k ≥ n
⊢ x.leNat k = true
Tactic:
exact mono hge h
Proof state after:
no goals
Theorem: ENat.leNat_eq_true_of_le_coe
Proof state before:
x : ENat
n : Nat
⊢ x ≤ ENat.ofNat n → x.leNat n = true
Tactic:
intro h
Proof state after:
x : ENat
n : Nat
h : x ≤ ENat.ofNat n
⊢ x.leNat n = true
Theorem: ENat.leNat_eq_true_of_le_coe
Proof state before:
x : ENat
n : Nat
h : x ≤ ENat.ofNat n
⊢ x.leNat n = true
Tactic:
cases h n with
| inl h => exact h
| inr h => absurd h; simp only [leNat_coe_eq_false_iff_gt]; exact Nat.lt_irrefl _
Proof state after:
no goals
Theorem: ENat.leNat_eq_true_of_le_coe
Proof state before:
case inl
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : x.leNat n = true
⊢ x.leNat n = true
Tactic:
exact h
Proof state after:
no goals
Theorem: ENat.leNat_eq_true_of_le_coe
Proof state before:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ x.leNat n = true
Tactic:
absurd h
Proof state after:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬(ENat.ofNat n).leNat n = false
Theorem: ENat.leNat_eq_true_of_le_coe
Proof state before:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬(ENat.ofNat n).leNat n = false
Tactic:
simp only [leNat_coe_eq_false_iff_gt]
Proof state after:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬n < n
Theorem: ENat.leNat_eq_true_of_le_coe
Proof state before:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬n < n
Tactic:
exact Nat.lt_irrefl _
Proof state after:
no goals
Theorem: ENat.leNat_eq_false_of_coe_lt
Proof state before:
n : Nat
x : ENat
⊢ ENat.ofNat n < x → x.leNat n = false
Tactic:
intro ⟨m, h, hm⟩
Proof state after:
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
⊢ x.leNat n = false
Theorem: ENat.leNat_eq_false_of_coe_lt
Proof state before:
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
⊢ x.leNat n = false
Tactic:
rw [leNat_coe_eq_true_iff_le] at h
Proof state after:
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
⊢ x.leNat n = false
Theorem: ENat.leNat_eq_false_of_coe_lt
Proof state before:
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
⊢ x.leNat n = false
Tactic:
exact mono' h hm
Proof state after:
no goals
Theorem: ENat.coe_lt_of_leNat_eq_false
Proof state before:
n : Nat
x : ENat
⊢ x.leNat n = false → ENat.ofNat n < x
Tactic:
intro h
Proof state after:
n : Nat
x : ENat
h : x.leNat n = false
⊢ ENat.ofNat n < x
Theorem: ENat.coe_lt_of_leNat_eq_false
Proof state before:
n : Nat
x : ENat
h : x.leNat n = false
⊢ ENat.ofNat n < x
Tactic:
exists n
Proof state after:
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
Theorem: ENat.coe_lt_of_leNat_eq_false
Proof state before:
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
Tactic:
constructor
Proof state after:
case left
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true

case right
n : Nat
x : ENat
h : x.leNat n = false
⊢ x.leNat n = false
Theorem: ENat.coe_lt_of_leNat_eq_false
Proof state before:
case left
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true
Tactic:
rw [leNat_coe_eq_true_iff_le]
Proof state after:
case left
n : Nat
x : ENat
h : x.leNat n = false
⊢ n ≤ n
Theorem: ENat.coe_lt_of_leNat_eq_false
Proof state before:
case left
n : Nat
x : ENat
h : x.leNat n = false
⊢ n ≤ n
Tactic:
exact Nat.le_refl _
Proof state after:
no goals
Theorem: ENat.coe_lt_of_leNat_eq_false
Proof state before:
case right
n : Nat
x : ENat
h : x.leNat n = false
⊢ x.leNat n = false
Tactic:
exact h
Proof state after:
no goals
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
n : Nat
x : ENat
⊢ ENat.ofNat n < x ↔ ENat.ofNat (n + 1) ≤ x
Tactic:
constructor
Proof state after:
case mp
n : Nat
x : ENat
⊢ ENat.ofNat n < x → ENat.ofNat (n + 1) ≤ x

case mpr
n : Nat
x : ENat
⊢ ENat.ofNat (n + 1) ≤ x → ENat.ofNat n < x
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp
n : Nat
x : ENat
⊢ ENat.ofNat n < x → ENat.ofNat (n + 1) ≤ x
Tactic:
intro ⟨m, h, hm⟩ k
Proof state after:
case mp
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
k : Nat
⊢ (ENat.ofNat (n + 1)).leNat k = true ∨ x.leNat k = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
k : Nat
⊢ (ENat.ofNat (n + 1)).leNat k = true ∨ x.leNat k = false
Tactic:
rw [leNat_coe_eq_true_iff_le] at h ⊢
Proof state after:
case mp
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
⊢ n + 1 ≤ k ∨ x.leNat k = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
⊢ n + 1 ≤ k ∨ x.leNat k = false
Tactic:
cases Nat.lt_or_ge n k with
| inl hlt => left; exact hlt
| inr hge => right; apply mono' hge; apply mono' h; exact hm
Proof state after:
no goals
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp.inl
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hlt : n < k
⊢ n + 1 ≤ k ∨ x.leNat k = false
Tactic:
left
Proof state after:
case mp.inl.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hlt : n < k
⊢ n + 1 ≤ k
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp.inl.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hlt : n < k
⊢ n + 1 ≤ k
Tactic:
exact hlt
Proof state after:
no goals
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp.inr
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ n + 1 ≤ k ∨ x.leNat k = false
Tactic:
right
Proof state after:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat k = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat k = false
Tactic:
apply mono' hge
Proof state after:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat n = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat n = false
Tactic:
apply mono' h
Proof state after:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat m = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat m = false
Tactic:
exact hm
Proof state after:
no goals
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr
n : Nat
x : ENat
⊢ ENat.ofNat (n + 1) ≤ x → ENat.ofNat n < x
Tactic:
intro h
Proof state after:
case mpr
n : Nat
x : ENat
h : ENat.ofNat (n + 1) ≤ x
⊢ ENat.ofNat n < x
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr
n : Nat
x : ENat
h : ENat.ofNat (n + 1) ≤ x
⊢ ENat.ofNat n < x
Tactic:
cases h n with
| inl h => rw [leNat_coe_eq_true_iff_le] at h; absurd h; exact Nat.lt_irrefl n
| inr h => exists n; rw [leNat_coe_eq_true_iff_le]; exact ⟨Nat.le_refl n, h⟩
Proof state after:
no goals
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : (ENat.ofNat (n + 1)).leNat n = true
⊢ ENat.ofNat n < x
Tactic:
rw [leNat_coe_eq_true_iff_le] at h
Proof state after:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ENat.ofNat n < x