## Stream: new members

### Topic: failed to instantiate goal

#### Huỳnh Trần Khanh (Jun 28 2021 at 09:10):

what does this error mean?

failed to instantiate goal with function.embedding.mk (fun (x : 4._.10), (dite ((frozen_name has_mem.mem) x a) (fun (h : (frozen_name has_mem.mem) x a), (b.to_fun (subtype.mk x h))) (fun (h : not ((frozen_name has_mem.mem) x a)), (dite (nonempty a) (fun (h : nonempty a), (a.max' h)) (fun (h : not (nonempty a)), x)))))


this is the proof that i got

lemma goal_injective : ∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ ↪ ℕ), set.restrict h S = f := begin
intros a b,
rw [finset.set_of_mem.symm, set.set_coe_eq_subtype] at b,
classical,
use function.embedding.mk (λ x, if h : x ∈ a then b.to_fun (subtype.mk x h)
else if h : nonempty a then a.max' h else x),
sorry,
end


here is the room numbering scheme that i'm trying to implement: if the set of VIP people is empty then the room number is equal to the person number. otherwise, if the person is VIP then the room number is retrieved from the ↥(↑S : set ℕ) ↪ ℕ bundle. if the person is not VIP then the room number is equal to the max room number that is assigned to a VIP person, plus 1, plus that person's number.

#### Kevin Buzzard (Jun 28 2021 at 09:12):

If you break this up a bit and try

let g := function.embedding.mk (λ x, if h : x ∈ a then b.to_fun (subtype.mk x h)
else if h : nonempty a then a.max' h else x),


then you can see your error, this term doesn't quite typecheck.

#### Kevin Buzzard (Jun 28 2021 at 09:16):

I don't know why the error use gives is so obfuscated; somehow the term has been partially translated into some more primitive form before stuff bombs out. If you look at the code which defines use (e.g. by right clicking on it) you might be able to work out what's going on better than I can!

#### Anne Baanen (Jun 28 2021 at 09:18):

tactic#use and tactic#show are two tactics that I almost never use because their error messages are useless. Instead there is refine \<something, _\> or tactic#change

#### Kevin Buzzard (Jun 28 2021 at 09:19):

use is absolutely great for beginners though, and I use show a lot in my teaching when Lean decides to obfuscate the goal for whatever reason and I use show to tidy it up before the sorry that the students then have to deal with.

#### Anne Baanen (Jun 28 2021 at 09:23):

Sure, refine \<something, _\> is a bit more complicated, but the basic use of change is exactly the same as show except the error change reports is not just literally show tactic failed

#### Anne Baanen (Jun 28 2021 at 09:25):

(I just remembered show has a secondary use where you can choose which goal to work on. Still the basic purpose of show and change is identical.)

#### Vasily Ilin (May 13 2022 at 00:31):

I am getting an error failed to instantiate goal with polynomial K after use polynomial K when my goal is ∃ (X : (Algebra K)ᵒᵖ) (f : coyoneda.obj X ⟶ forget (Algebra K)), is_iso f. Why could this be? The file is below

import category_theory.types
import algebra.category.Algebra.basic
import algebra.category.Group.basic
import data.polynomial.basic

open_locale polynomial
open polynomial
open category_theory

variables (K : Type*) [comm_ring K]

class affine_scheme :=
(scheme : Algebra K ⥤ Type*)
(corepresentable : scheme.corepresentable)

class affine_group_scheme :=
(scheme : Algebra K ⥤ Group)
(corepresentable : (scheme ⋙ forget Group).corepresentable)

-- DEFINING G_a
instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
use polynomial K, -- failed to instantiate goal with polynomial K
end,
}


#### Eric Wieser (May 13 2022 at 06:37):

I would guess you need to use docs#Algebra.of

#### Kevin Buzzard (May 13 2022 at 06:46):

If you want to see what use exists you can always try refine \<_, _\>

#### Vasily Ilin (May 14 2022 at 08:46):

@Kevin Buzzard I do not understand what refine \<_, _\> does. It splits goal ⊢ ∃ (X : (Algebra K)ᵒᵖ), Exists is_iso into ⊢ (Algebra K)ᵒᵖ and ⊢ Exists is_iso. But I don't understand what it means to prove ⊢ (Algebra K)ᵒᵖ.

#### Vasily Ilin (May 14 2022 at 08:48):

@Eric Wieser , this is a good suggestion but it did not work for me. I'm getting failed to instantiate goal with Algebra.of K ((frozen_name polynomial) K) error.

#### Alex J. Best (May 14 2022 at 08:48):

It means you have to give an element of Algebra K^op, which is as per https://leanprover-community.github.io/mathlib_docs/algebra/category/Algebra/basic.html#Algebra a triple of a Type a ring structure and an algebra structure.

#### Eric Wieser (May 14 2022 at 08:49):

Alex, I think your parens are missing there

#### Alex J. Best (May 14 2022 at 08:49):

Sure, its also not unicode

#### Vasily Ilin (May 14 2022 at 08:50):

But this does not work:

instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
simp only,
have : algebra K K[X],
refine ring_hom.to_algebra _,
exact C,
refine ⟨_, _⟩,
refine opposite.op _,
use Algebra.of K (K[X]) -- failed to instantiate goal with Algebra.of K ((frozen_name polynomial) K)

end,
}


#### Eric Wieser (May 14 2022 at 08:50):

Can you change that use to a refine?

#### Eric Wieser (May 14 2022 at 08:50):

You'll get a better error message

#### Alex J. Best (May 14 2022 at 08:51):

Or existsi  instead of use

#### Eric Wieser (May 14 2022 at 08:51):

It's not even an existential at that point

#### Vasily Ilin (May 14 2022 at 08:51):

Error: failed to synthesize type class instance for K : Type u_1, _inst_1 : comm_ring K, this : algebra K K[X] ⊢ algebra K K[X]

#### Alex J. Best (May 14 2022 at 08:52):

Eric Wieser said:

It's not even an existential at that point

I'm confused why we are using use instead of exact then?

#### Eric Wieser (May 14 2022 at 08:52):

I think tactic#use tries to be clever

#### Vasily Ilin (May 14 2022 at 08:52):

Actually, this also errors: #check Algebra.of K K[X]. Not sure what's going on

#### Eric Wieser (May 14 2022 at 08:53):

Do you have data.polynomial.algebra_map imported?

#### Eric Wieser (May 14 2022 at 08:54):

You need to have docs#polynomial.algebra_of_algebra imported

#### Vasily Ilin (May 14 2022 at 08:55):

I did not. I thought it would be part of polyonmial.basic. Now #check Algebra.of K K[X] works. But the proof still does not

#### Vasily Ilin (May 14 2022 at 08:55):

I am not getting an error any more though

#### Eric Wieser (May 14 2022 at 08:56):

Surely if the proof doesn't work, then you're still getting an error?

#### Vasily Ilin (May 14 2022 at 08:56):

instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
simp only,
have : algebra K K[X],
refine ring_hom.to_algebra _,
exact C,
refine ⟨_, _⟩,
refine opposite.op _, -- ⊢ Algebra K
refine Algebra.of K (K[X]) -- ⊢ Algebra K
end,
}


#### Vasily Ilin (May 14 2022 at 08:56):

This is what I have. I give it a K-algebra but it doesn't wanna take it

#### Eric Wieser (May 14 2022 at 08:57):

You're not done, you have another goal to prove

#### Vasily Ilin (May 14 2022 at 08:57):

Well, that worked

#### Vasily Ilin (May 14 2022 at 09:01):

What does the goal ⊢ Exists is_iso mean? Mathematically, I need to prove the isomorphism Hom(K[X], A) = abelian group of A. But I don't understand how this goal expresses that

#### Alex J. Best (May 14 2022 at 09:03):

The goal state after

-- DEFINING G_a
instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
refine ⟨opposite.op (Algebra.of K (K[X])), _⟩,

end,
}


might be more clear

Last updated: Dec 20 2023 at 11:08 UTC