display of setoid.r

Stream: general

[ZHAO Jinxiang]

import group_theory.quotient_group

variables {α β : Type*} (f : α → β)

noncomputable def my_setoid_comap_quotient_equiv (f : α → β) (r : setoid β) :
  quotient (setoid.comap f r) ≃ set.range (@quotient.mk _ r ∘ f) :=
begin
  symmetry,
  apply (setoid.quotient_ker_equiv_range (quotient.mk ∘ f)).symm.trans,
  dunfold setoid.ker function.on_fun function.comp setoid.comap setoid.rel,
  apply quotient.congr_right,
  intros a b,
  convert_to ⟦f a⟧ = ⟦f b⟧ ↔ setoid.r (f a) (f b),
  convert_to ⟦f a⟧ = ⟦f b⟧ ↔ f a ≈ f b,
  simp,
end

image.png

You can find it shows setoid.r a b ↔ setoid.r a b and I should search the setoid and convert it to ⟦f a⟧ = ⟦f b⟧ ↔ setoid.r (f a) (f b) by hand.

Can we unfold the setoid.r definitions by tactics?

[Eric Wieser]

convert_to is a tactic, so I'm not sure of your question

[ZHAO Jinxiang]

I want to use dunfold setoid.r, but it fails.
If I need to use convert_to , I should search the context and know which is the setoid.r's definition.
convert_to requires me to query the setoid.r's definition in context every time, which is inconvenient.

[Eric Wieser]

setoid.r is a field, there's nothing to unfold

[ZHAO Jinxiang]

But setoid.r a b could be simplify.

[Eric Wieser]

Your term is probably @setoid.r some_s x y, which means you actually need to unfold some_s

[Eric Wieser]

You can hover over the goal in the infoview to find out

[Eric Wieser]

Note that ≈ unfolds to setoid.r, not the other way around

[Kevin Buzzard]

I've always felt that there was something wrong here. It's hard to get from a goal with ≈ in to the actual definition of the equivalence relation, unless you know it already and just do it yourself with change.

[ZHAO Jinxiang]

Yes. Every time I want to proof theorem about quotient and setoid, I need to use change tactic a lot.

[ZHAO Jinxiang]

Especially setoid.r x y

[ZHAO Jinxiang]

import group_theory.quotient_group

variables {α β : Type*} (f : α → β)

def function_to_image (f : α → β):  α → {x // x ∈ set.range f} := λ x , ⟨f x, set.mem_range_self x⟩
noncomputable def my_quotient_ker_equiv_range : @quotient α (setoid.ker f) ≃ set.range f :=
begin
  refine equiv.of_bijective (λ k , @quotient.lift _ _ (setoid.ker f) (function_to_image f) (λ a b h , subtype.ext_val h) k)  _,
  split,
  {
    intros x y, simp,
    intro h,
    simp [function_to_image] at h,
    rcases x,
    rcases y,
    simp at h,
    apply quotient.sound,
    unfold has_equiv.equiv,
    -- Why exact h
    exact h,
  },
  {
    rintro ⟨y, z, hz⟩,
    simp,
    use @quotient.mk _ (setoid.ker f) z,
    rw quotient.lift_mk,
    rw function_to_image,
    simp,
    exact hz,
  }
end

image.png

I don't know why I can use exact h here, unless I search the definition of setoid.ker. I need some tactic to unfold the definition of setoid.r a d setoid.ker.

[Eric Wieser]

dunfold setoid.ker should work

[ZHAO Jinxiang]

Thank you. I try dunfold setoid.ker function.on_fun setoid.r, and it works.

[Kevin Buzzard]

By the way, here is the same proof as yours, but re-arranged so that it takes far fewer lines:

begin
  refine equiv.of_bijective (λ k , @quotient.lift _ _ (setoid.ker f) (function_to_image f) (λ a b h , subtype.ext_val h) k)  _,
  split,
  {
    rintros ⟨x⟩ ⟨y⟩ h,
    apply quotient.sound,
    simpa [function_to_image] using h,
  },
  {
    rintro ⟨y, z, hz⟩,
    use @quotient.mk _ (setoid.ker f) z,
    simpa [function_to_image] using hz,
  }
end

[Kyle Miller]

Does tactic#unfold_projs help here to unfold setoid.r?

[ZHAO Jinxiang]

Kyle Miller said:

Does tactic#unfold_projs help here to unfold setoid.r?

Thank you a lot. That is the static I need.