Elements of Pi types with specific values

Stream: new members

[Jonas van der Schaaf]

I'm trying to construct an element of a Pi type which has specific values as in the example below. I don't know how to do this case distinction as lean doesn't understand that i=j in this case in my if/else statement. I hope there's an easy way to do this, but I'm not sure.

import Mathlib

example {J : Type*} [DecidableEq J] {types : J → Type*} (nonempty : ∀j, Nonempty (types j))
    (i : J) (t : types i) : ∃ (p : (Π(j : J), types j)), p i = t :=
  ⟨
    fun j ↦  (
      if i = j then
        t
      else
        Classical.choice (nonempty j)
    ),
    by
      rfl
  ⟩

[Ruben Van de Velde]

For example:

import Mathlib

example {J : Type*} [DecidableEq J] {types : J → Type*} (nonempty : ∀j, Nonempty (types j))
    (i : J) (t : types i) : ∃ (p : (Π(j : J), types j)), p i = t :=
  ⟨
    fun j ↦  (
      if hij : i = j then
        hij ▸ t
      else
        Classical.choice (nonempty j)
    ),
    by
      simp
  ⟩

[Jonas van der Schaaf]

Thank you. Unfortunately, I realized my problem is slightly more complicated than what I wrote here and I simplified slightly too much. How would one fill in the sorry in the code below?

import Mathlib

example {J : Type*} {A : Type*} [DecidableEq J] {types : J → Type*}
    (nonempty : ∀j, Nonempty (types j)) (f : (j : J) → types j → A)
    (i : J) (t : types i) : ∃ (p : (Π(j : J), types j)), ∀ j, i = j → f j (p j) = f i t :=
  ⟨
    fun j ↦  (
      if hij : i = j then
        hij ▸ t
      else
        Classical.choice (nonempty j)
    ),
    by
      intro j h
      simp [dif_pos h]
      sorry
  ⟩

[Aaron Liu]

subst h (that's a tactic), then rfl

[Etienne Marion]

This is the usual way:

import Mathlib

example {J : Type*} {A : Type*} [DecidableEq J] {types : J → Type*}
    (nonempty : ∀j, Nonempty (types j)) (f : (j : J) → types j → A)
    (i : J) (t : types i) : ∃ (p : (Π(j : J), types j)), ∀ j, i = j → f j (p j) = f i t :=
  ⟨
    fun j ↦  (
      if hij : i = j then
        hij ▸ t
      else
        Classical.choice (nonempty j)
    ),
    by
      intro j h
      simp [dif_pos h]
      cases h; rfl
  ⟩

[Jonas van der Schaaf]

Thank you, that works great! Is there a place I can read up on this kind of "type magic" in Lean? This isn't the first time I've run into issues like this.

[Kenny Lau]

@Jonas van der Schaaf This is called "dependent type hell", and the way to avoid it is to minimize the use of ▸. For example, currently if m = n, then there is a function called Fin.cast : Fin m -> Fin n, so that you can use Fin.cast instead of the evil ▸.