how to define a function with already exist one

Stream: new members

[ZOE]

I want to define y i with x i , but their domains are different, how to deal with it?
x : Finset.Icc 1 n → ℕ,

let y : Finset.Icc 1 (k+1) → ℕ := λ i=> if i<k+1 then x i else k+1

but it report an error:
application type mismatch
x i
argument
i
has type
{ x // x ∈ Finset.Icc 1 (k + 1) } : Type
but is expected to have type
{ x // x ∈ Finset.Icc 1 k } : Type

[ZOE]

import Mathlib
theorem nt :
    IsLeast {n : ℕ | ∃ x : Finset.Icc 1 n → ℕ,
                  (∀ i, 1 ≤ x i ∧ x i ≤ n) ∧
                  (∑ i, x i = n * (n + 1) / 2) ∧
                  (∏ i, x i = Nat.factorial n) ∧
                  Set.range x ≠ Set.range (fun i => i + 1)} 9 := by
    let satisfy (n : ℕ) : Prop := ∃ x : Finset.Icc 1 n → ℕ,
        (∀ i, 1 ≤ x i ∧ x i ≤ n) ∧
        (∑ i, x i = n * (n + 1) / 2) ∧
        (∏ i, x i = Nat.factorial n) ∧
        Set.range x ≠ Set.range (fun i => i + 1)
    have h1 : ∀ k : ℕ , satisfy k → satisfy (k+1) := by
        intro k hk
        rcases hk with ⟨x, ⟨hx1, ⟨hx2, ⟨hx3, hx4⟩⟩⟩⟩
        let y : Finset.Icc 1 (k+1) → ℕ := λ i=> if i∈Finset.Icc 1 k  then x i else k+1

[ZOE]

I have tried to fix it by

        let y : Finset.Icc 1 (k+1) → ℕ := λ i=> if i∈Finset.Icc 1 k  then x i else k+1

it report an error:
failed to synthesize
Membership { x // x ∈ Finset.Icc 1 (k + 1) } (Finset ℕ)

Additional diagnostic information may be available using the set_option diagnostics true command.

[Ruben Van de Velde]

Please don't double post

[ZOE]

sorry for that, I thought that different channels are independent of each other. Should I delete one?

[ZOE]

I didn't find where to delete a topic, I have marked another one as resolved. Sorry for that :face_holding_back_tears: