[GOAL]
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n : ℕ
inst✝ : GradeMinOrder (Fin n) α
a : Fin n
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
cases n
[GOAL]
case zero
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : GradeMinOrder (Fin zero) α
a : Fin zero
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
exact a.elim0
[GOAL]
case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (succ n✝)) α
a : Fin (succ n✝)
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
rw [h.eq_bot, Fin.bot_eq_zero]
[GOAL]
case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (succ n✝)) α
a : Fin (succ n✝)
h : IsMin a
⊢ IsMin ↑0
[PROOFSTEP]
exact isMin_bot
