ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.liftOn
      (Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
        (_ :
          ∀ (a b : List ι) (h : a ≈ b),
            (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
                (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b))
      (fun f => Quotient.mk inferInstance fun i => f i (_ : i ∈ Finset.univ))
      (_ :
        ∀ (a b : (i : ι) → i ∈ Finset.univ.val → α i),
          a ≈ b →
            (Quotient.mk inferInstance fun i => a i (_ : i ∈ Finset.univ)) =
              Quotient.mk inferInstance fun i => b i (_ : i ∈ Finset.univ)) =
    Quotient.mk inferInstance f
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ (finChoice fun i => Quotient.mk (inst✝ i) (f i)) = Quotient.mk inferInstance f
dsimp only [Quotient.finChoice]
no goals
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.liftOn
      (Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
        (_ :
          ∀ (a b : List ι) (h : a ≈ b),
            (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
                (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b))
      (fun f => Quotient.mk inferInstance fun i => f i (_ : i ∈ Finset.univ))
      (_ :
        ∀ (a b : (i : ι) → i ∈ Finset.univ.val → α i),
          a ≈ b →
            (Quotient.mk inferInstance fun i => a i (_ : i ∈ Finset.univ)) =
              Quotient.mk inferInstance fun i => b i (_ : i ∈ Finset.univ)) =
    Quotient.mk inferInstance f
conv_lhs =>
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b) =
    Quotient.mk inferInstance fun i x => f i
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b) =
    ?m.24194
change _ = ⟦fun i _ => f i⟧
no goals
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b) =
    Quotient.mk inferInstance fun i x => f i
exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _