Theorem: LoVe.Nat.le_lt_imp (LoVe/LoVelib.lean)

State before:
m n : ℕ
p : Prop
hge : m ≥ n
⊢ m < n → p ↔ True
Tactic:
apply Iff.intro
State after:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True

case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p

State before:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True

case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Tactic:
{ intro himp
  apply True.intro }
State after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p

State before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Tactic:
{ intro htrue
  intro hlt
  have hle : n ≤ m :=
    hge
  rw [←Nat.not_lt_eq] at hle
  apply False.elim
  exact hle hlt }
State after:
no goals

State before:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True
Tactic:
intro himp
State after:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
himp : m < n → p
⊢ True

State before:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
himp : m < n → p
⊢ True
Tactic:
apply True.intro
State after:
no goals

State before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Tactic:
intro htrue
State after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
⊢ m < n → p

State before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
⊢ m < n → p
Tactic:
intro hlt
State after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
⊢ p

State before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
⊢ p
Tactic:
have hle : n ≤ m :=
  hge
State after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : n ≤ m
⊢ p

State before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : n ≤ m
⊢ p
Tactic:
rw [←Nat.not_lt_eq] at hle
State after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ p

State before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ p
Tactic:
apply False.elim
State after:
case mpr.h
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ False

State before:
case mpr.h
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ False
Tactic:
exact hle hlt
State after:
no goals