Function giving type mismatch on output

Stream: general

[Tarun Nair]

I'm proving Lagrange's theorem as part of a Lean coursework for a college module. In particular, I have implemented cosets and I would like to define a bijection f:H → coset H g between these cosets. Here's a MWE of what I'm trying to do:

import Mathlib.Tactic

variable {G : Type} [Group G]
variable (H : Subgroup G)

def R (g k : G) : Prop := ∃ h : H, k = g * ↑h

def coset : G → Set G := fun g ↦ { k : G | R H g k }

def f (g : G) : H → coset H g := fun h ↦ g * h

But then I get the error:

Type mismatch
  g * ↑h
has type
  G
but is expected to have type
  ↑(coset H g)

How do I coerce g*h into being in ↑(coset H g)?

[Kevin Buzzard]

Firstly you should probably use ∃ h ∈ H because otherwise you're unnecessarily coercing H from a subgroup (a term) to a group (a type).

But if you really want to set up functions between cosets then you really are treating them as types, so what you need to know is how to make a term of type ↑(coset H g) where the arrow means "I'm coercing a set to a type", and the way to do this is to understand that to make a term of type ↑(coset H g) is to give a pair consisting of a term of type G and a proof that it's in the coset. So it's like this

def f (g : G) : H → coset H g := fun h ↦ ⟨g * h, sorry⟩

where you have to fill in the sorry.

[Tarun Nair]

It works now, thanks Kevin. However, now I'm having trouble with the ⟨_, _⟩ syntax. During proofs, is there a way of extracting the element from the bracket? For instance, if my goal looks like

⊢ f H g ⟨h, ph1⟩ = ⟨k, ⋯⟩

then how would I get the elements h and k out?

[Ruben Van de Velde]

generalize_proofs perhaps

[Aaron Liu]

what exactly do you mean "get them out"

[Tarun Nair]

Aaron Liu said:

what exactly do you mean "get them out"

As in, getting rid of the angled brackets. I can't do much with the brackets in the goal.

Ruben Van de Velde said:

generalize_proofs perhaps

That's added the subtype proof for k as a hypothesis, but the brackets remain.

[Aaron Liu]

you can't get rid of the brackets

[Aaron Liu]

that wouldn't be type correct

[Tarun Nair]

I see. The problem is that the usual tactics, simp etc, don't seem to be working.

[Aaron Liu]

if you have ↑⟨h, ⋯⟩ in your goal then they cancel out and it's just equal to h

[Aaron Liu]

but you can't just get rid of the brackets directly

[Tarun Nair]

I see, so coercing the element into belonging to the superset?

[Aaron Liu]

you can start by introducing ↑s into your goal (in this case it's docs#Subtype.val) using docs#Subtype.ext or with the ext tactic