exact? double boom

Stream: lean4

[Julian Berman]

Should I expect exact? to not find Fintype.ofEquiv in:

import Mathlib
  example {A B : Type*} [Group A] [Group B] [Fintype A] (heq : A ≃* B) : Fintype B := by exact? -- fails
  example {A B : Type*} [Group A] [Group B] [Fintype A] (heq : A ≃* B) : Fintype B := Fintype.ofEquiv A heq

And what's with the second error message that talks about 'linearIndependentFintypeOfLeSpanFintype'?

[Kevin Buzzard]

I guess there's an implicit coercion. Does it work if heq is the bare Equiv?

[Kyle Miller]

On a version of mathlib from today, I just see a single error message, in the first example. Where are you seeing anything about linearIndependentFintypeOfLeSpanFintype?

[Julian Berman]

I'm probably a few days behind on this gitpod, let me update.

[Kyle Miller]

This succeeds:

example {A B : Type*} [Group A] [Group B] [Fintype A] (heq : A ≃ B) : Fintype B := by exact?

Maybe exact? could put all the projections to parent structures in context before searching? (@Scott Morrison Would that be feasible?)

[Julian Berman]

(Indeed upgrading from 4310b5835 which is what I was on to HEAD now makes that linear independent error message go away)

[Junyan Xu]

That's because I changed the Fintype to Finite

[Julian Berman]

But what I didn't understand is what it had anything to do with that example that exact? was finding it (and then complaining about it)

[Kim Morrison]

Kyle Miller said:

This succeeds:

example {A B : Type*} [Group A] [Group B] [Fintype A] (heq : A ≃ B) : Fintype B := by exact?

Maybe exact? could put all the projections to parent structures in context before searching? (Scott Morrison Would that be feasible?)

Presumably this would be a change to solve_by_elim rather than exact?. If I'm understanding right, exact? would be applying Fintype.ofEquiv here successfully, but then failing to fill in the subgoals.

[Kim Morrison]

If someone wants to implement a saturate_parents tactic we could easily try hooking that in.