ι : 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
ι : 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
simp [Quotient.finChoiceAux, Quotient.finChoiceAux_eq l, -Quotient.eq]
ι : 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
ι : 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
refine' Quotient.sound fun j h => _
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
ι : 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
by_cases e : j = i <;> simp [e] <;> try exact Setoid.refl _
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
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
subst j
no goals
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
exact Setoid.refl _
no goals
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
exact Setoid.refl _