Theorem: Nat.tri_mono (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
case zero_zero

⊢ 0 ≤ 0 → tri 0 ≤ tri 0
Tactic:
intro
State after:
case zero_zero
a✝ : 0 ≤ 0
⊢ tri 0 ≤ tri 0

State before:
case zero_zero
a✝ : 0 ≤ 0
⊢ tri 0 ≤ tri 0
Tactic:
reflexivity
State after:
no goals

State before:
case zero_succ
n : Nat
a✝ : 0 ≤ n → tri 0 ≤ n.tri
⊢ 0 ≤ n + 1 → tri 0 ≤ (n + 1).tri
Tactic:
intro
State after:
case zero_succ
n : Nat
a✝¹ : 0 ≤ n → tri 0 ≤ n.tri
a✝ : 0 ≤ n + 1
⊢ tri 0 ≤ (n + 1).tri

State before:
case zero_succ
n : Nat
a✝¹ : 0 ≤ n → tri 0 ≤ n.tri
a✝ : 0 ≤ n + 1
⊢ tri 0 ≤ (n + 1).tri
Tactic:
exact Nat.zero_le ..
State after:
no goals

State before:
case succ_zero
m : Nat
a✝ : m ≤ 0 → m.tri ≤ tri 0
⊢ m + 1 ≤ 0 → (m + 1).tri ≤ tri 0
Tactic:
intro
State after:
case succ_zero
m : Nat
a✝¹ : m ≤ 0 → m.tri ≤ tri 0
a✝ : m + 1 ≤ 0
⊢ (m + 1).tri ≤ tri 0

State before:
case succ_zero
m : Nat
a✝¹ : m ≤ 0 → m.tri ≤ tri 0
a✝ : m + 1 ≤ 0
⊢ (m + 1).tri ≤ tri 0
Tactic:
contradiction
State after:
no goals

State before:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
⊢ m + 1 ≤ n + 1 → (m + 1).tri ≤ (n + 1).tri
Tactic:
intro h
State after:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ (m + 1).tri ≤ (n + 1).tri

State before:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ (m + 1).tri ≤ (n + 1).tri
Tactic:
rw [tri_succ, tri_succ]
State after:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m + 1 ≤ n.tri + n + 1

State before:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m + 1 ≤ n.tri + n + 1
Tactic:
apply Nat.add_le_add_right
State after:
case succ_succ.h
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m ≤ n.tri + n

State before:
case succ_succ.h
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m ≤ n.tri + n
Tactic:
apply Nat.add_le_add
State after:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri ≤ n.tri

case succ_succ.h.h₂
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n

State before:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri ≤ n.tri
Tactic:
apply H
State after:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n

State before:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n
Tactic:
exact Nat.le_of_succ_le_succ h
State after:
no goals

State before:
case succ_succ.h.h₂
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n
Tactic:
exact Nat.le_of_succ_le_succ h
State after:
no goals