[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
l : List ι
⊢ Setoid ((i : ι) → i ∈ l → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ Quotient inferInstance
[PROOFSTEP]
refine'
  Quotient.liftOn₂ (f i (List.mem_cons_self _ _)) (Quotient.finChoiceAux l fun j h => f j (List.mem_cons_of_mem _ h)) _
    _
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ α i → ((i : ι) → i ∈ l → α i) → Quotient inferInstance
case refine'_2
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ ∀ (a₁ : α i) (b₁ : (i : ι) → i ∈ l → α i) (a₂ : α i) (b₂ : (i : ι) → i ∈ l → α i),
    a₁ ≈ a₂ → b₁ ≈ b₂ → ?refine'_1 a₁ b₁ = ?refine'_1 a₂ b₂
[PROOFSTEP]
exact fun a l => ⟦fun j h => if e : j = i then by rw [e]; exact a else l _ ((List.mem_cons.1 h).resolve_left e)⟧
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l✝ : List ι
f : (i_1 : ι) → i_1 ∈ i :: l✝ → Quotient (S i_1)
a : α i
l : (i : ι) → i ∈ l✝ → α i
j : ι
h : j ∈ i :: l✝
e : j = i
⊢ α j
[PROOFSTEP]
rw [e]
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l✝ : List ι
f : (i_1 : ι) → i_1 ∈ i :: l✝ → Quotient (S i_1)
a : α i
l : (i : ι) → i ∈ l✝ → α i
j : ι
h : j ∈ i :: l✝
e : j = i
⊢ α i
[PROOFSTEP]
exact a
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ ∀ (a₁ : α i) (b₁ : (i : ι) → i ∈ l → α i) (a₂ : α i) (b₂ : (i : ι) → i ∈ l → α i),
    a₁ ≈ a₂ →
      b₁ ≈ b₂ →
        (Quotient.mk inferInstance fun j h => if e : j = i then Eq.mpr (_ : α j = α i) a₁ else b₁ j (_ : j ∈ l)) =
          Quotient.mk inferInstance fun j h => if e : j = i then Eq.mpr (_ : α j = α i) a₂ else b₂ j (_ : j ∈ l)
[PROOFSTEP]
refine' fun a₁ l₁ a₂ l₂ h₁ h₂ => Quotient.sound fun j h => _
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
⊢ (if e : j = i then Eq.mpr (_ : α j = α i) a₁ else l₁ j (_ : j ∈ l)) ≈
    if e : j = i then Eq.mpr (_ : α j = α i) a₂ else l₂ j (_ : j ∈ l)
[PROOFSTEP]
by_cases e : j = i
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : j = i
⊢ (if e : j = i then Eq.mpr (_ : α j = α i) a₁ else l₁ j (_ : j ∈ l)) ≈
    if e : j = i then Eq.mpr (_ : α j = α i) a₂ else l₂ j (_ : j ∈ l)
[PROOFSTEP]
simp [e]
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ (if e : j = i then Eq.mpr (_ : α j = α i) a₁ else l₁ j (_ : j ∈ l)) ≈
    if e : j = i then Eq.mpr (_ : α j = α i) a₂ else l₂ j (_ : j ∈ l)
[PROOFSTEP]
simp [e]
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : α i = α j) a₁ ≈ cast (_ : α i = α j) a₂
[PROOFSTEP]
subst j
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
h : i ∈ i :: l
⊢ cast (_ : α i = α i) a₁ ≈ cast (_ : α i = α i) a₂
[PROOFSTEP]
exact h₁
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ l₁ j (_ : j ∈ l) ≈ l₂ j (_ : j ∈ l)
[PROOFSTEP]
exact h₂ _ _
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (finChoiceAux (i :: l) fun i_1 h => Quotient.mk (S i_1) (f i_1 h)) = Quotient.mk inferInstance f
[PROOFSTEP]
simp [Quotient.finChoiceAux, Quotient.finChoiceAux_eq l, -Quotient.eq]
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (Quotient.mk inferInstance fun j h =>
      if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l))
      else f j (_ : j ∈ i :: l)) =
    Quotient.mk inferInstance f
[PROOFSTEP]
refine' Quotient.sound fun j h => _
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
⊢ (if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) else f j (_ : j ∈ i :: l)) ≈
    f j h
[PROOFSTEP]
by_cases e : j = i
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ (if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) else f j (_ : j ∈ i :: l)) ≈
    f j h
[PROOFSTEP]
simp [e]
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ (if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) else f j (_ : j ∈ i :: l)) ≈
    f j h
[PROOFSTEP]
simp [e]
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) ≈ f j h
[PROOFSTEP]
try exact Setoid.refl _
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) ≈ f j h
[PROOFSTEP]
exact Setoid.refl _
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ f j (_ : j ∈ i :: l) ≈ f j h
[PROOFSTEP]
try exact Setoid.refl _
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ f j (_ : j ∈ i :: l) ≈ f j h
[PROOFSTEP]
exact Setoid.refl _
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) ≈ f j h
[PROOFSTEP]
subst j
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
h : i ∈ i :: l
⊢ cast (_ : (fun i => α i) i = (fun i => α i) i) (f i (_ : i ∈ i :: l)) ≈ f i h
[PROOFSTEP]
exact Setoid.refl _
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
l : Multiset ι
⊢ Setoid ((i : ι) → i ∈ l → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
⊢ (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸ (fun l => finChoiceAux l fun i x => f i) a =
    (fun l => finChoiceAux l fun i x => f i) b
[PROOFSTEP]
have := fun a => Quotient.finChoiceAux_eq a fun i _ => Quotient.out (f i)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this :
  ∀ (a : List ι),
    (finChoiceAux a fun i h => Quotient.mk (S i) (out (f i))) = Quotient.mk inferInstance fun i x => out (f i)
⊢ (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸ (fun l => finChoiceAux l fun i x => f i) a =
    (fun l => finChoiceAux l fun i x => f i) b
[PROOFSTEP]
simp [Quotient.out_eq] at this 
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
⊢ (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸ (fun l => finChoiceAux l fun i x => f i) a =
    (fun l => finChoiceAux l fun i x => f i) b
[PROOFSTEP]
simp [this]
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
⊢ ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i)) =
    Quotient.mk inferInstance fun i x => out (f i)
[PROOFSTEP]
let g := fun a : Multiset ι => (⟦fun (i : ι) (_ : i ∈ a) => Quotient.out (f i)⟧ : Quotient (by infer_instance))
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a✝ b : List ι
h : a✝ ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
a : Multiset ι
⊢ Setoid ((i : ι) → i ∈ a → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i)) =
    Quotient.mk inferInstance fun i x => out (f i)
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case h
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq
    ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i))
    (Quotient.mk inferInstance fun i x => out (f i))
[PROOFSTEP]
trans (g a)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq
    ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i))
    (g ↑a)
[PROOFSTEP]
exact eq_rec_heq (φ := fun l : Multiset ι => @Quotient (∀ i ∈ l, α i) (by infer_instance)) (Quotient.sound h) (g a)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
l : Multiset ι
⊢ Setoid ((i : ι) → i ∈ l → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq (g ↑a) (Quotient.mk inferInstance fun i x => out (f i))
[PROOFSTEP]
change HEq (g a) (g b)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq (g ↑a) (g ↑b)
[PROOFSTEP]
congr 1
[GOAL]
case e_1
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ ↑a = ↑b
[PROOFSTEP]
exact Quotient.sound h
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : (i : ι) → i ∈ Finset.univ.val → α i
h : a ≈ b
i : ι
⊢ a i (_ : i ∈ Finset.univ) ≈ b i (_ : i ∈ Finset.univ)
[PROOFSTEP]
apply h
[GOAL]
ι : 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
[PROOFSTEP]
dsimp only [Quotient.finChoice]
[GOAL]
ι : 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
[PROOFSTEP]
conv_lhs =>
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : 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))
[PROOFSTEP]
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : 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))
[PROOFSTEP]
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : 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))
[PROOFSTEP]
enter [1]
[GOAL]
ι : 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)
[PROOFSTEP]
tactic =>
  change _ = ⟦fun i _ => f i⟧
  exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : 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.23336
[PROOFSTEP]
change _ = ⟦fun i _ => f i⟧
[GOAL]
ι : 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
[PROOFSTEP]
exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
