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

State before:
m n : Nat
h : m ≥ n
⊢ min m n = n
Tactic:
rw [Nat.min_def]
State after:
m n : Nat
h : m ≥ n
⊢ (if m ≤ n then m else n) = n

State before:
m n : Nat
h : m ≥ n
⊢ (if m ≤ n then m else n) = n
Tactic:
if hmn : m ≤ n then
  have : m = n := Nat.le_antisymm hmn h
  rw [if_pos hmn, this]
else
  rw [if_neg hmn]
State after:
no goals

State before:
m n : Nat
h : m ≥ n
hmn : m ≤ n
⊢ (if m ≤ n then m else n) = n
Tactic:
have : m = n := Nat.le_antisymm hmn h
State after:
m n : Nat
h : m ≥ n
hmn : m ≤ n
this : m = n
⊢ (if m ≤ n then m else n) = n

State before:
m n : Nat
h : m ≥ n
hmn : m ≤ n
this : m = n
⊢ (if m ≤ n then m else n) = n
Tactic:
rw [if_pos hmn, this]
State after:
no goals

State before:
m n : Nat
h : m ≥ n
hmn : ¬m ≤ n
⊢ (if m ≤ n then m else n) = n
Tactic:
rw [if_neg hmn]
State after:
no goals