apply exact and ge

Stream: general

[MohanadAhmed]

Whilst looking at Possible bug with simpa and trying to understand for myself I came up with the following test cases but could not explain what is happening.

In the following code foo2, foo4, foo5 and foo6 produce errors whilst the remaining work fine.
The error message on 2 and 4 is

typeclass instance problem is stuck, it is often due to metavariables
  PartialOrder ?m.319

Whilst on 5 and 5 the error message is:

tactic 'apply' failed, failed to unify
  ∀ {b : ?α}, ?a ≤ b → b ≤ ?a → b = ?a
with
  ∀ {b : P}, a ≥ b → b ≥ a → a = b

P : Type u_1
inst✝ : PartialOrder P
a : P
⊢ ∀ {b : P}, a ≥ b → b ≥ a → a = b

Any thoughts on what is happening?

8 Cases Code

import Mathlib.Order.Basic

theorem foo1 (P : Type*) [PartialOrder P] (a : P): ∀ {b : P}, a ≥ b → b ≥ a → a = b := by
  exact ge_antisymm

theorem foo2 (P : Type*) [PartialOrder P] (a : P): ∀ (b : P), a ≥ b → b ≥ a → a = b := by
  exact ge_antisymm

theorem foo3 (P : Type*) [PartialOrder P] (b : P): ∀ {a : P}, a ≥ b → b ≥ a → a = b := by
  exact ge_antisymm

theorem foo4 (P : Type*) [PartialOrder P] (b : P): ∀ (a : P), a ≥ b → b ≥ a → a = b := by
  exact ge_antisymm

theorem foo5 (P : Type*) [PartialOrder P] (a : P): ∀ {b : P}, a ≥ b → b ≥ a → a = b := by
  apply ge_antisymm

theorem foo6 (P : Type*) [PartialOrder P] (a : P): ∀ (b : P), a ≥ b → b ≥ a → a = b := by
  apply ge_antisymm

theorem foo7 (P : Type*) [PartialOrder P] (b : P): ∀ {a : P}, a ≥ b → b ≥ a → a = b := by
  apply ge_antisymm

theorem foo8 (P : Type*) [PartialOrder P] (b : P): ∀ (a : P), a ≥ b → b ≥ a → a = b := by
  apply ge_antisymm

[Etienne Marion]

Here are fixes:

import Mathlib.Order.Basic

theorem foo1 (P : Type*) [PartialOrder P] (a : P): ∀ {b : P}, a ≥ b → b ≥ a → a = b := by
  exact ge_antisymm

theorem foo2 (P : Type*) [PartialOrder P] (a : P): ∀ (b : P), a ≥ b → b ≥ a → a = b := by
  exact fun _ ↦ ge_antisymm

theorem foo3 (P : Type*) [PartialOrder P] (b : P): ∀ {a : P}, a ≥ b → b ≥ a → a = b := by
  exact ge_antisymm

theorem foo4 (P : Type*) [PartialOrder P] (b : P): ∀ (a : P), a ≥ b → b ≥ a → a = b := by
  exact fun _ ↦ ge_antisymm

theorem foo5 (P : Type*) [PartialOrder P] (a : P): ∀ {b : P}, a ≥ b → b ≥ a → a = b := by
  intro b
  apply ge_antisymm

theorem foo6 (P : Type*) [PartialOrder P] (a : P): ∀ (b : P), a ≥ b → b ≥ a → a = b := by
  intro b
  apply ge_antisymm

theorem foo7 (P : Type*) [PartialOrder P] (b : P): ∀ {a : P}, a ≥ b → b ≥ a → a = b := by
  apply ge_antisymm

theorem foo8 (P : Type*) [PartialOrder P] (b : P): ∀ (a : P), a ≥ b → b ≥ a → a = b := by
  apply ge_antisymm

My guess is:
For foo2 and foo4 the goal you want to prove takes an explicit argument, while ge_antisymm does not, so exact can't unify them, that's why I add fun _ ↦ which means that first we introduce the argument.
For foo5 and foo6, it is because your goal introduces a and b in a different order compared to ge_antisymm, but the second argument is not introduced, so apply does not unify both. Does that make sense?

[MohanadAhmed]

Thanks @Etienne Marion
Let me start with foo2 and foo4. In both cases your opinion is that the rorr is related to the implicitness of the argument. Now unfortunately, the error report is about typeclass instance problem is stuck. Any thoughts on why the error message says this?

[Kevin Buzzard]

The error message is unhelpful, and means "I'm trying to unify ∀ (b : P), a ≥ b → b ≥ a → a = b with ∀ {a b : α}, a ≤ b → b ≤ a → b = a and I am so confused right now by the implicit/explicit error that I can't even figure out what P is"