Theorem: lt_of_size_lt_size (Fl/Lemmas.lean)

State before:
x y : ℕ
h : Nat.size x < Nat.size y
⊢ x < y
Tactic:
apply Nat.lt_of_not_le
State after:
case a
x y : ℕ
h : Nat.size x < Nat.size y
⊢ ¬y ≤ x

State before:
case a
x y : ℕ
h : Nat.size x < Nat.size y
⊢ ¬y ≤ x
Tactic:
intro (hle : y ≤ x)
State after:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ False

State before:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ False
Tactic:
apply Nat.lt_le_asymm h
State after:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ Nat.size y ≤ Nat.size x

State before:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ Nat.size y ≤ Nat.size x
Tactic:
apply Nat.size_le_size
State after:
case a.h
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ y ≤ x

State before:
case a.h
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ y ≤ x
Tactic:
exact hle
State after:
no goals