-- Mathlib/Data/Fintype/Quotient.lean
theorem finChoice_eq (a : ∀ i, α i) :
    finChoice (S := S) (⟦a ·⟧) = ⟦a⟧

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l => ∀ (i : ι), i ∈ l) (fun s => ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l => Quotient.map (fun a i => a i ⋯) ⋯ (listChoice fun i x => ⟦a i⟧)) ⋯ =
    ⟦a⟧

Tactic:
obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep

Result:
case intro
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l => ∀ (i : ι), i ∈ l) (fun s => ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l => Quotient.map (fun a i => a i ⋯) ⋯ (listChoice fun i x => ⟦a i⟧)) ⋯ =
    ⟦a⟧

Proof state:
case intro
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l => ∀ (i : ι), i ∈ l) (fun s => ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l => Quotient.map (fun a i => a i ⋯) ⋯ (listChoice fun i x => ⟦a i⟧)) ⋯ =
    ⟦a⟧

Tactic:
simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]

Result:
case intro
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a =>
              Quotient.hrecOn (motive := fun x =>
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l => ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h => ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a => a.liftOn (fun a => ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l => Quotient.map (fun a i => a i ⋯) ⋯ ⟦fun x1 x2 => a x1⟧) ⋯ =
    ⟦a⟧

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
⊢ (finChoice fun x => ⟦a x⟧) = ⟦a⟧

Tactic:
dsimp [finChoice]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l => ∀ (i : ι), i ∈ l) (fun s => ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l => Quotient.map (fun a i => a i ⋯) ⋯ (listChoice fun i x => ⟦a i⟧)) ⋯ =
    ⟦a⟧

Proof state:
case intro
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a =>
              Quotient.hrecOn (motive := fun x =>
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l => ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h => ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a => a.liftOn (fun a => ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l => Quotient.map (fun a i => a i ⋯) ⋯ ⟦fun x1 x2 => a x1⟧) ⋯ =
    ⟦a⟧

Tactic:
rfl

Result:
no goals