Proof of cast with dependant equality

Stream: mathlib4

[Paradoxy]

I was wondering, whether it is possible to prove "problem" without introduction any new lemma:

import Mathlib.LinearAlgebra.PiTensorProduct


variable {ι : Type*} {S₁ S₂ : Set ι} (hdisj : Disjoint S₁ S₂) [∀ i, Decidable (i ∈ S₁)]
variable {V : ι → Type*} {R : Type*}
  [CommSemiring R] [∀ i, AddCommMonoid (V i)] [∀ i, Module R (V i)]


abbrev idxElim : S₁ ⊕ S₂ → ι := Sum.elim (↑) (↑)

def unionToSum (i : ↑(S₁ ∪ S₂)) : ↑S₁ ⊕ ↑S₂ :=
  if h: i.val ∈ S₁ then Sum.inl ⟨i.val, h⟩
  else Sum.inr ⟨i.val, by aesop⟩

lemma idxElim_unionToSum (i : ↑(S₁ ∪ S₂)) : idxElim (unionToSum i) = i := by
  aesop (add safe unfold [idxElim, unionToSum])


lemma problem {i : ↑(S₁ ∪ S₂)} (x : V i) (c : R) :
    (cast (by rw [(idxElim_unionToSum i)]) (c • x) : V (idxElim (unionToSum i)) )
    = c • cast (by rw [(idxElim_unionToSum i)]) x := by
  have h := (idxElim_unionToSum i).symm
  subst h

I have tried all tactics I am aware of, including erw, simp, subst, etc. I think the main reason all of them fail is because both sides of idxElim (unionToSum i) = i depends on i and therefore recursively substituting is not possible. I tried to give name to with set q := idxElim (unionToSum i) so that subst only sees q and replace it with i (or vice versa) but it also failed since it sees through q definition. Now, Of course I can prove this theorem by introduction an auxiliary lemma for a general equality and use it to prove this theorem. But it wouldn't make sense to prove many such small lemmas for something so trivial. Also I want to understand from educational purposes the limitations of Lean.

I will be thankful if you know any way of proving this without introduction separate lemmas.

[Aaron Liu]

easy:

import Mathlib.LinearAlgebra.PiTensorProduct


variable {ι : Type*} {S₁ S₂ : Set ι} (hdisj : Disjoint S₁ S₂) [∀ i, Decidable (i ∈ S₁)]
variable {V : ι → Type*} {R : Type*}
  [CommSemiring R] [∀ i, AddCommMonoid (V i)] [∀ i, Module R (V i)]


abbrev idxElim : S₁ ⊕ S₂ → ι := Sum.elim (↑) (↑)

def unionToSum (i : ↑(S₁ ∪ S₂)) : ↑S₁ ⊕ ↑S₂ :=
  if h: i.val ∈ S₁ then Sum.inl ⟨i.val, h⟩
  else Sum.inr ⟨i.val, by aesop⟩

lemma idxElim_unionToSum (i : ↑(S₁ ∪ S₂)) : idxElim (unionToSum i) = i := by
  aesop (add safe unfold [idxElim, unionToSum])


lemma problem {i : ↑(S₁ ∪ S₂)} (x : V i) (c : R) :
    (cast (by rw [(idxElim_unionToSum i)]) (c • x) : V (idxElim (unionToSum i)) )
    = c • cast (by rw [(idxElim_unionToSum i)]) x := by
  have h := idxElim_unionToSum i
  change cast (by rw [h]) (c • x) = c • cast (by rw [h]) x
  generalize idxElim (unionToSum i) = j at h
  subst h
  rfl

[Paradoxy]

@Aaron Liu Wow, thanks it is very helpful.