## Stream: new members

### Topic: Argument interpreted as instance?

#### Pedro Minicz (Aug 14 2020 at 16:55):

Why is unfreezeI necessary in the following example? I'd expect hX not to be an instance, as I specified it as an argument ((hX : nonempty X)) not an instance ([nonempty X] or [hX : nonempty X]).

example (hX : nonempty X) (hY : #Y ≤ 1) :
¬ ∃ (f : X → Y) (B : set Y), f '' (f ⁻¹' B) ⊊ B :=
begin
rintros ⟨f, A, h₁, h₂⟩,
refine h₂ (le_antisymm h₁ _),
intros y hy,
rw cardinal.le_one_iff_subsingleton at hY,
cases hY with hY,
unfreezeI,
cases hX with x,
use x,
specialize hY (f x) y,
simpa [hY]
end


#### Reid Barton (Aug 14 2020 at 16:56):

The binder type matters to your caller, not to you.

#### Pedro Minicz (Aug 14 2020 at 16:59):

But the type of the lemma is still nonempty ?m_1 → _, so it doesn't seem that the argument would even be given as an instance by the user.

#### Reid Barton (Aug 14 2020 at 17:27):

It wouldn't, but what would happen at a hypothetical use site is not relevant to processing the definition itself.

#### Reid Barton (Aug 14 2020 at 17:29):

The different binder types don't make a difference for the purpose of the definition. hX is treated as an instance because nonempty is a class.

#### Pedro Minicz (Aug 14 2020 at 22:19):

Weird behavior. I'd expect my definition to specify how hX is treated.

Last updated: May 10 2021 at 18:22 UTC