## Stream: new members

### Topic: Unfolding creates now hypothesis

#### Pedro Minicz (Jun 12 2020 at 22:26):

Why does unfold create new hypothesis?

import group_theory.quotient_group

variables {α : Type} [group α] {s : set α} [is_subgroup s]

def r (a b : α) : Prop := a⁻¹ * b ∈ s

example {a b : quotient_group.quotient s} : a = b :=
begin
unfold quotient_group.quotient at a b,
sorry
end


#### Mario Carneiro (Jun 12 2020 at 22:31):

because the goal depends on a and b

#### Mario Carneiro (Jun 12 2020 at 22:32):

When simp runs on the reverted version of the goal, it can't rewrite inside the binder domain

#### Mario Carneiro (Jun 12 2020 at 22:32):

Use dunfold

Interesting.

#### Pedro Minicz (Jun 12 2020 at 22:39):

Also on (d)unfold/(d)simp, how can I unfold setoid.r on the goal setoid.r (quotient.out' a) (quotient.out' b) (the goal at sorry).

import group_theory.quotient_group

variables {α : Type} [group α] {s : set α} [is_subgroup s]

def r (a b : α) : Prop := a⁻¹ * b ∈ s

example {a b : quotient_group.quotient s} : a = b :=
begin
rw [←a.out_eq', ←b.out_eq'],
apply quotient.sound',
sorry
end


#### Pedro Minicz (Jun 12 2020 at 22:40):

I know that setoid.r = r defined above (it is how its defined in group_theory.quotient_group and would like to leverage that fact.

#### Mario Carneiro (Jun 12 2020 at 22:42):

do you want the r you defined or the one in quotient_group?

#### Mario Carneiro (Jun 12 2020 at 22:43):

you can always force it with change

#### Pedro Minicz (Jun 12 2020 at 22:44):

I don't seem to be able to use change. change r a.out' b.out' nor change setoid.r a.out' b.out' work.

#### Kevin Buzzard (Jun 12 2020 at 22:45):

I've found it frustrating in the past that sometimes one can't just say "unfold this relation". You can use set instead of let to unfold a definitional let but there's no analogue here

#### Mario Carneiro (Jun 12 2020 at 22:45):

  change @r _ _ s _ (quotient.out' a) (quotient.out' b),


works

#### Kevin Buzzard (Jun 12 2020 at 22:45):

Sometimes simp only [setoid.r] works

#### Pedro Minicz (Jun 12 2020 at 22:46):

Mario Carneiro said:

  change @r _ _ s _ (quotient.out' a) (quotient.out' b),


works

Omg, you are a wizard. :grinning_face_with_smiling_eyes:

#### Mario Carneiro (Jun 12 2020 at 22:46):

it is complicated here because it's not actually a simple unfold, r is not involved in the definition at all

#### Pedro Minicz (Jun 12 2020 at 22:46):

That sure is quite the work around (although not really), I would have taken a long while to figure it out myself, thanks!

#### Pedro Minicz (Jun 12 2020 at 22:47):

(Maybe making this whole ordeal less opaque would be good. It is not clear at all that this was even possible after a lot of messing around with unfold and simp.)

#### Mario Carneiro (Jun 12 2020 at 22:48):

What I actually did was change r _ _, but that didn't work until I did change _ ∈ _, change r _ _, which yields a is_subgroup s subgoal. So apparently it can't figure out the implicit arguments to r without help

#### Pedro Minicz (Jun 12 2020 at 22:48):

Wow, that is amazing!

#### Mario Carneiro (Jun 12 2020 at 22:48):

which makes sense, because r doesn't have anything in its type that would help infer s

#### Pedro Minicz (Jun 12 2020 at 22:49):

Thank you for explaining your thought process. I just started using change earlier today actually (but I remember someone mentioning in another thread a while ago) and am not very good at it. :grinning_face_with_smiling_eyes:

#### Mario Carneiro (Jun 12 2020 at 22:50):

when in doubt, use lots of underscores :grinning:

#### Mario Carneiro (Jun 12 2020 at 22:53):

I think it helps to know that there is always the fallback of being completely explicit and providing a fully elaborated term. That will always work unless the kernel is broken, so it's really a matter of inserting more implicit info until it works and then scaling back until you have just enough for lean to close the distance

(deleted)

#### Eric Wieser (Jul 29 2020 at 16:53):

(sorry, caught out by zulip's filtered search)

Last updated: May 14 2021 at 07:19 UTC