obtain ⟨n, h⟩ := Subgroup.mem_closure_singleton.mp h
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h : x ∈ H
⊢ { val := x, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h✝ : x ∈ H
n : ℤ
h : a ^ n = x
⊢ { val := x, property := h✝ } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }