Theorem: Nat.min_succ_succ' (Algdata/Init/Nat.lean)

State before:
m n : Nat
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
if h : m ≤ n then
  rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
else
  have : m ≥ n := Nat.le_of_lt (Nat.gt_of_not_le h)
  rw [Nat.min_eq_right' this, Nat.min_eq_right' (Nat.succ_le_succ this)]
State after:
no goals

State before:
m n : Nat
h : m ≤ n
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
State after:
no goals

State before:
m n : Nat
h : ¬m ≤ n
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
have : m ≥ n := Nat.le_of_lt (Nat.gt_of_not_le h)
State after:
m n : Nat
h : ¬m ≤ n
this : m ≥ n
⊢ min (succ m) (succ n) = succ (min m n)

State before:
m n : Nat
h : ¬m ≤ n
this : m ≥ n
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
rw [Nat.min_eq_right' this, Nat.min_eq_right' (Nat.succ_le_succ this)]
State after:
no goals