ModelTheory.Fraisse #4565

Stream: mathlib4

[Xavier Roblot]

I think there is a max universe problem in the port of this file:

application type mismatch
  @Embedding L ?m.69491 (G j)
argument
  G j
has type
  ↑K : Type (max (max u v) (w + 1))
but is expected to have type
  Type ?u.69486 : Type (?u.69486 + 1)

If I understand correctly UnivLE is supposed to help with this but I could not figure out how to use it.

[Scott Morrison]

That doesn't look like a problem looking for a UnivLE solution to me.

[Johan Commelin]

I have a mysterious situation here:

/-- Sufficient conditions for a class to be the age of a countably-generated structure. -/
theorem exists_cg_is_age_of (hn : K.Nonempty)
    (h : ∀ M N : Bundled.{w} L.Structure, Nonempty (M ≃[L] N) → (M ∈ K ↔ N ∈ K))
    (hc : (Quotient.mk' '' K).Countable)
    (fg : ∀ M : Bundled.{w} L.Structure, M ∈ K → Structure.FG L M) (hp : Hereditary K)
    (jep : JointEmbedding K) : ∃ M : Bundled.{w} L.Structure, Structure.CG L M ∧ L.age M = K := by
  obtain ⟨F, hF⟩ := hc.exists_eq_range (hn.image _)
  -- <snip>
    cases' n with n
    · dsimp; exact Embedding.refl _ _
    · -- dsimp -- Porting note: uncomment this and lots of stuff ↑ ↑ ↑ will break
      exact (hFP _ n).some

[Johan Commelin]

The tactic state looks all reasonable, but if you add a dsimp at the end of the proof, then suddenly many other subproofs start giving errors.

[Johan Commelin]

Is this hinting at a buggy tactic?

[Johan Commelin]

This is now the only remaining error in this file

[Matthew Ballard]

Can you use ?_ on RHS of obtain?

[Matthew Ballard]

:check:

[Matthew Ballard]

Matthew Ballard said:

Can you use ?_ on RHS of obtain?

More precisely, this line

obtain ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, ?_⟩

did not create a new goal and only errored when all other obligations were discharged

[Johan Commelin]

aha, thanks for debugging

[Johan Commelin]

I didn't realize that was the problem

[Matthew Ballard]

Compare to let. This

let ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, ?_⟩

creates a new goal as does have

[Matthew Ballard]

We probably don't want that behavior for obtain

[Ruben Van de Velde]

Matthew Ballard said:

Can you use ?_ on RHS of obtain?

https://github.com/leanprover-community/mathlib4/issues/5732

Wasn't there a porting note with that link?

[Matthew Ballard]

Which link?

[Ruben Van de Velde]

The link in the exact message you're responding to

[Matthew Ballard]

Ok you mean in #4707. Yes.