obtain (h | h) := this.lt_or_eq
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)