Theorem: succ_leq_succ_of_leq (Notes4/MoreTacs.lean)

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ plus m a ≤ plus n a
Tactic:
match a with 
| 0 => simp [plus]; assumption 
| b+1 => 
  simp [plus] 
  apply Nat.succ_le_succ
  exact succ_leq_succ_of_leq m n b h
State after:
no goals

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ plus m 0 ≤ plus n 0
Tactic:
simp [plus]
State after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ m ≤ n

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ m ≤ n
Tactic:
assumption
State after:
no goals

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m (b + 1) ≤ plus n (b + 1)
Tactic:
simp [plus]
State after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ Nat.succ (plus m b) ≤ Nat.succ (plus n b)

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ Nat.succ (plus m b) ≤ Nat.succ (plus n b)
Tactic:
apply Nat.succ_le_succ
State after:
case a
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m b ≤ plus n b

State before:
case a
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m b ≤ plus n b
Tactic:
exact succ_leq_succ_of_leq m n b h
State after:
no goals