α✝ : Sort ?u.35644
β : Sort ?u.35647
ι : Type u_1
α : ι → Sort u_2
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p fun i => Quotient.mk (s i) (out (f i))
α✝ : Sort ?u.35644
β : Sort ?u.35647
ι : Type u_1
α : ι → Sort u_2
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p f
rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]
no goals
α✝ : Sort ?u.35644
β : Sort ?u.35647
ι : Type u_1
α : ι → Sort u_2
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p fun i => Quotient.mk (s i) (out (f i))
apply h