applying lemma that uses instance

Stream: mathlib4

[Paige Thomas]

I'm wondering, why does the simp only [List.nil_union] work in the first example, but not the second? I think List.union is the instance of the union notation?

import Mathlib


example
  {α β : Type}
  [DecidableEq α]
  [DecidableEq β]
  (f : α → β)
  (l1 l2 : List α)
  (h1 : Function.Injective f) :
  List.map f (l1 ∪ l2) = (List.map f l1) ∪ (List.map f l2) :=
  by
  induction l1
  case nil =>
    simp only [List.map_nil]
    simp only [List.nil_union]
  case cons hd tl ih =>
    sorry


example
  {α β : Type}
  [DecidableEq α]
  [DecidableEq β]
  (f : α → β)
  (l1 l2 : List α)
  (h1 : Function.Injective f) :
  List.map f (List.union l1 l2) = List.union (List.map f l1) (List.map f l2) :=
  by
  induction l1
  case nil =>
    simp only [List.map_nil]
    -- simp only [List.nil_union] <- fails
    sorry
  case cons hd tl ih =>
    sorry

[Paige Thomas]

Is there a way to convert between List.union and ∪?

[Ruben Van de Velde]

You should probably just avoid writing List.union in the first place

[Paige Thomas]

I'm not sure how to use ∪ when I need to use it as a function. That is, for example, when using it as the function in List.map.

[Paige Thomas]

That is List.map List.union xs, for example.

[Paige Thomas]

Although, maybe it isn't an issue for the cases where I use it as a function.

[Aaron Liu]

fun x => xs ∪ x, or (xs ∪ ·)

[Aaron Liu]

Or Union.union xs, but that's not very readable.

[Paige Thomas]

Thank you.