Theorem: leq_succ_of_leq (Notes4/MoreTacs.lean)

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ n
⊢ m ≤ plus n 1
Tactic:
match n with 
| 0 => 
  have meq0 : m = 0 := Nat.eq_zero_of_le_zero h
  rw [meq0]
  simp
| n'+1 => 
  simp [plus]
  calc 
    m ≤ n'+1 := by exact h 
    _ ≤ (n'+1)+1 := by exact Nat.le_succ _
State after:
no goals

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
⊢ m ≤ plus 0 1
Tactic:
have meq0 : m = 0 := Nat.eq_zero_of_le_zero h
State after:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
meq0 : m = 0
⊢ m ≤ plus 0 1

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

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n : ℕ
h : m ≤ 0
meq0 : m = 0
⊢ 0 ≤ plus 0 1
Tactic:
simp
State after:
no goals

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

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ m ≤ Nat.succ (n' + 1)
Tactic:
calc 
  m ≤ n'+1 := by exact h 
  _ ≤ (n'+1)+1 := by exact Nat.le_succ _
State after:
no goals

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ m ≤ n' + 1
Tactic:
exact h
State after:
no goals

State before:
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n n' : ℕ
h : m ≤ n' + 1
⊢ n' + 1 ≤ n' + 1 + 1
Tactic:
exact Nat.le_succ _
State after:
no goals