match choice_aut with
 | Exists.intro f h =>
     exists (λ n ↦ f^[n] a)
     apply And.intro
     . simp [Nat.iterate]
     . intros n
       simp
       rw [iterate_left]
       apply h
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
no goals