coercions and lambda-terms

Stream: new members

[Antoine Chambert-Loir]

I managed (god knows how…) to pass around the problem, but I had the following issue :
Instead of having to prove something like x ∈ s, as I expected, Lean wanted me to prove x ∈ λ (x : α), x ∈ s
and nothing had me change this to what I wanted.
I tried change… and set_like.mem_set_of_eq for example.

[Kyle Miller]

That usually indicates you took a wrong term somewhere -- for example using apply with a lemma that expects a predicate but everything is in terms of sets. Sometimes this is a problem with mathlib's lemmas (in which case you sharing a #mwe could be helpful).

I'm surprised change x ∈ s didn't work to get things back to normal.

[Antoine Chambert-Loir]

something like that , except that H was defined as a stabilizer…:

example (G : Type*) [group G] (K H : subgroup G) (h : K ≤ H) (x : G) (hx : x ∈ K)
: x ∈ H :=
begin
  apply set.mem_of_subset_of_mem h,
  --- oops
end

[Antoine Chambert-Loir]

In that case, change x ∈ K makes the job, so I suspect that the formula for the stabilizer, while looking the same when rendered by VSCode, was not definably equal.

[Ruben Van de Velde]

Looks like the problem is that your ∈'s are for subgroups and not sets

[Ruben Van de Velde]

import group_theory.subgroup.basic

example (G : Type) [group G] (K H : subgroup G) (h : K ≤ H) (x : G) (hx : x ∈ K)
: x ∈ H :=
begin
  rw set_like.le_def at h,
  simp_rw ←set_like.mem_coe at h hx ⊢,
  apply set.mem_of_subset_of_mem h,
  -- ⊢ x ∈ ↑K
end

[Kyle Miller]

I'm not sure if this constitutes "subverting the API", but h itself is the lemma:

example (G : Type*) [group G] (K H : subgroup G) (h : K ≤ H) (x : G) (hx : x ∈ K)
: x ∈ H :=
begin
  apply h,
  exact hx
end

[Kyle Miller]

@Ruben Van de Velde What are the coercion rewrites doing? Any reason not do do this?

example (G : Type) [group G] (K H : subgroup G) (h : K ≤ H) (x : G) (hx : x ∈ K)
: x ∈ H :=
begin
  rw set_like.le_def at h,
  apply h,
  exact hx,
end

[Ruben Van de Velde]

Oh, good point - I was trying to get to the point where set.mem_of_subset_of_mem made sense, but there is no need for that

[Antoine Chambert-Loir]

Removing these set.mem_of_subset_of_mem improved many other lines of my code ! Thanks !