MIL ch8.1 problem

Stream: new members

[Rado Kirov]

In the following MIL ch8.1 problem Lean struggles to find appropriate types:

This works

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
    have h1 := card_dvd_of_le (inf_le_left: H ⊓ K ≤ H)
  ...

but this doesn't with an error about SemilatticeInf

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  have h1 := card_dvd_of_le (@inf_le_left G H K)
  ...

Kinda surprising to me that what I think of the more explicit version, passing args is not accepted. Or maybe I am doing something wrong?

[suhr]

import Mathlib

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  have h1 := Subgroup.card_dvd_of_le (inf_le_left: H ⊓ K ≤ H)
  sorry

#print inf_bot_of_coprime  -- click on inf_le_left

lemma inf_bot_of_coprime' {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  have h1 := Subgroup.card_dvd_of_le (@inf_le_left (Subgroup G) Lattice.toSemilatticeInf H K)
  sorry

[Damiano Testa]

With @inf_le_left G H K you are filling in the arguments of inf_le_left in the order in which they appear.

The first argument should be the type where the implied infs are computed. This is not G, but rather the type of subgroups of G, called Subgroup G.

The next argument is an instance on Subgroup G, to make sure that it has a notion of inf.

Finally, you pass the two "subgroups".

So, you could do have h1 := card_dvd_of_le (@inf_le_left _ _ H K) to tell Lean: I want to use the theorem with H and K, please figure out the rest for me!

[Damiano Testa]

A slightly nicer way of achieving the same is by "calling out" the implicit arguments to be filled in:

have h1 := card_dvd_of_le (inf_le_left (a := H) (b := K))

[Rado Kirov]

That makes a lot of sense, thanks! Somehow in my mental model type class instances are not passes as parameters to @, but the Subgroup G instead of G is an obvious oversight on my part.