From 73df7d24a7ec50399be54a47fbfc0e10a0a50967 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 17 Jul 2024 16:12:30 -0400 Subject: [PATCH] refactor: Lint --- .../SpaceTime/LorentzTensor/Real/Basic.lean | 29 +++++---- .../LorentzTensor/Real/Constructors.lean | 64 +++++-------------- .../LorentzTensor/Real/LorentzAction.lean | 45 ++++++------- .../LorentzTensor/Real/Multiplication.lean | 11 +--- 4 files changed, 53 insertions(+), 96 deletions(-) diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index f1249fb..00f48ff 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -49,7 +49,6 @@ instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTen /-- An `IndexValue` is a set of actual values an index can take. e.g. for a 3-tensor (0, 1, 2). -/ -@[simp] def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x) @@ -91,7 +90,7 @@ def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x /-- An equivalence of `ColorsIndex` types given an equality of a colors. -/ def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) : ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ := - Equiv.cast (by rw [h]) + Equiv.cast (congrArg (ColorsIndex d) h) /-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/ def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}: @@ -127,7 +126,7 @@ lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) : instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype -instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) := +instance [Fintype X] : DecidableEq (IndexValue d c) := Fintype.decidablePiFintype /-! @@ -136,6 +135,7 @@ instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) := -/ +/-- An isomorphism of the type of index values given an isomorphism of sets. -/ @[simps!] def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) : IndexValue d i ≃ IndexValue d j := @@ -155,12 +155,12 @@ lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color have h1 : ((indexValueIso d f h).trans (indexValueIso d g h')).symm = (indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)).symm := by subst h' h - ext x : 2 - rfl + exact Equiv.coe_inj.mp rfl simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1 lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : - (indexValueIso d f h).symm = indexValueIso d f.symm (by rw [h, Function.comp.assoc]; simp) := by + (indexValueIso d f h).symm = + indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h))) := by ext i : 1 rw [← Equiv.symm_apply_eq] funext y @@ -170,9 +170,10 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : rw [Equiv.apply_symm_apply] lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : - indexValueIso d f h = (indexValueIso d f.symm (by rw [h, Function.comp.assoc]; simp)).symm := by + indexValueIso d f h = + (indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h)))).symm := by rw [indexValueIso_symm] - congr + rfl @[simp] lemma indexValueIso_refl (d : ℕ) (i : X → Colors) : @@ -256,10 +257,9 @@ lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) : apply congrArg rw [← indexValueIso_trans] rfl - simp only [Function.comp.assoc, Equiv.symm_comp_self, CompTriple.comp_eq] + exact (Equiv.comp_symm_eq f (T.color ∘ ⇑f.symm) T.color).mp rfl -lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := by - rfl +lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := rfl lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl @@ -268,7 +268,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl ## Sums -/ - +/-- An equivalence splitting elements of `IndexValue d (Sum.elim TX TY)` into two components. -/ def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} : IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x)) @@ -330,10 +330,10 @@ instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue := def MarkedIndexValue (T : Marked d X n) : Type := IndexValue d T.markedColor -instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue := +instance (T : Marked d X n) : Fintype T.MarkedIndexValue := Pi.fintype -instance [Fintype X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue := +instance (T : Marked d X n) : DecidableEq T.MarkedIndexValue := Fintype.decidablePiFintype lemma color_eq_elim (T : Marked d X n) : @@ -341,6 +341,7 @@ lemma color_eq_elim (T : Marked d X n) : ext1 x cases' x <;> rfl +/-- An equivalence splitting elements of `IndexValue d T.color` into their two components. -/ def splitIndexValue {T : Marked d X n} : IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue := (indexValueIso d (Equiv.refl _) T.color_eq_elim).trans diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean index e661a9f..a349177 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean @@ -187,24 +187,16 @@ open Marked /-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/ lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by - refine ext ?_ ?_ + refine ext ?_ rfl · funext i exact Empty.elim i - · funext i - simp only [Fin.isValue, contr, IndexValue, Equiv.cast_apply, trace, diag_apply, ofReal, - Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton] - apply Finset.sum_congr rfl - intro x _ - rfl /-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by - refine ext ?_ ?_ + refine ext ?_ rfl · funext i exact Empty.elim i - · funext i - rfl /-! @@ -217,46 +209,38 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) : mapIso d (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum) (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by - refine ext ?_ ?_ + refine ext ?_ rfl · funext i exact Empty.elim i - · funext i - rfl /-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/ @[simp] lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) : mapIso d (Equiv.equivEmpty (Empty ⊕ Empty)) (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by - refine ext ?_ ?_ + refine ext ?_ rfl · funext i exact Empty.elim i - · funext i - rfl lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : Fin 1 ⊕ Fin d → ℝ) : mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)) (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by - refine ext ?_ ?_ + refine ext ?_ rfl · funext i simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm] fin_cases i rfl - · funext i - rfl lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : Fin 1 ⊕ Fin d → ℝ) : mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty) (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by - refine ext ?_ ?_ + refine ext ?_ rfl · funext i simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm] fin_cases i rfl - · funext i - rfl /-! @@ -290,7 +274,7 @@ lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) : intro i simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk] intro j _ - erw [toTensorRepMat_apply, Finset.prod_singleton] + simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl] rfl /-- The action of the Lorentz group on `ofVecDown v` is @@ -310,7 +294,7 @@ lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) : intro i simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk] intro j _ - erw [toTensorRepMat_apply, Finset.prod_singleton] + simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl] rfl @[simp] @@ -327,12 +311,8 @@ lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) refine Finset.sum_congr rfl (fun x _ => ?_) rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun y _ => ?_) - erw [toTensorRepMat_apply] - simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two, - Fin.isValue, one_mul, indexValueIso_refl, IndexValue] - simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk] - rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc] - congr + simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] + exact mul_right_comm _ _ _ @[simp] lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : @@ -348,12 +328,8 @@ lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d refine Finset.sum_congr rfl (fun x _ => ?_) rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun y _ => ?_) - erw [toTensorRepMat_apply] - simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two, - Fin.isValue, one_mul, lorentzGroupIsGroup_inv, indexValueIso_refl, IndexValue] - simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk] - rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc] - congr + simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] + exact mul_right_comm _ _ _ @[simp] lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : @@ -369,12 +345,8 @@ lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) refine Finset.sum_congr rfl (fun x _ => ?_) rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun y _ => ?_) - erw [toTensorRepMat_apply] - simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two, - Fin.isValue, one_mul, indexValueIso_refl, IndexValue, lorentzGroupIsGroup_inv] - simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk] - rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc] - congr + simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] + exact mul_right_comm _ _ _ @[simp] lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : @@ -391,12 +363,8 @@ lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) refine Finset.sum_congr rfl (fun x _ => ?_) rw [Finset.sum_mul] refine Finset.sum_congr rfl (fun y _ => ?_) - erw [toTensorRepMat_apply] - simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two, - Fin.isValue, one_mul, lorentzGroupIsGroup_inv, indexValueIso_refl, IndexValue] - simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk] - rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc] - congr + simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] + exact mul_right_comm _ _ _ end lorentzAction diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean index a565058..eee0dff 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean @@ -84,6 +84,7 @@ lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) : -/ +/-- The matrix representation of the Lorentz group given a color of index. -/ @[simps!] def toTensorRepMat {c : X → Colors} : LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where @@ -109,40 +110,33 @@ def toTensorRepMat {c : X → Colors} : ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by rw [Finset.prod_sum] simp only [Finset.prod_attach_univ, Finset.sum_univ_pi] - apply Finset.sum_congr - simp only [IndexValue, Fintype.piFinset_univ] - intro x _ rfl rw [h1] simp only [map_mul] - exact Finset.prod_congr rfl (fun x _ => rfl) + rfl refine Finset.sum_congr rfl (fun k _ => ?_) rw [Finset.prod_mul_distrib] lemma toTensorRepMat_mul' (i j : IndexValue d c) : toTensorRepMat (Λ * Λ') i j = ∑ (k : IndexValue d c), ∏ x, colorMatrix (c x) Λ (i x) (k x) * colorMatrix (c x) Λ' (k x) (j x) := by - simp [Matrix.mul_apply] + simp [Matrix.mul_apply, IndexValue] refine Finset.sum_congr rfl (fun k _ => ?_) rw [Finset.prod_mul_distrib] rfl -@[simp] lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors} (i j : IndexValue d (Sum.elim cX cY)) : toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 * - toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 := by - simp only [toTensorRepMat_apply] - rw [Fintype.prod_sum_type] - rfl + toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 := + Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ (i x) (j x) lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colors} (i j : IndexValue d cX) (k l : IndexValue d cY) : toTensorRepMat Λ i j * toTensorRepMat Λ k l = - toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) := by - simp only [toTensorRepMat_apply] - rw [Fintype.prod_sum_type] - rfl + toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) := + (Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ + (indexValueSumEquiv.symm (i, k) x) (indexValueSumEquiv.symm (j, l) x)).symm /-! @@ -153,10 +147,9 @@ lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colo lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n) (i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) : toTensorRepMat Λ i j * toTensorRepMat Λ k l = - toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) := by - simp only [toTensorRepMat_apply] - rw [Fintype.prod_sum_type] - rfl + toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) := + (Fintype.prod_sum_type fun x => + (colorMatrix (T.color x)) Λ (splitIndexValue.symm (i, k) x) (splitIndexValue.symm (j, l) x)).symm lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y 1) (h : T.markedColor 0 = τ (S.markedColor 0)) (x : ColorsIndex d (T.markedColor 0)) @@ -201,7 +194,7 @@ lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue) simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul] exact Finset.mem_univ k intro j _ hjk - simp [hjk] + simp [hjk, IndexValue] exact Or.inl (Matrix.one_apply_ne' hjk) /-! @@ -264,10 +257,8 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent erw [lorentzAction_smul_coord] simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul, Finset.sum_singleton, toTensorRepMat_apply] - erw [toTensorRepMat_apply] - simp only [IndexValue, toTensorRepMat, Unique.eq_default] - rw [@mul_left_eq_self₀] - exact Or.inl rfl + simp only [IndexValue, Unique.eq_default, Finset.univ_unique, Finset.sum_const, + Finset.card_singleton, one_smul] /-- The Lorentz action commutes with `mapIso`. -/ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) : @@ -277,7 +268,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT rw [mapIso_apply_coord] rw [lorentzAction_smul_coord', lorentzAction_smul_coord'] let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color := - indexValueIso d f (by funext x; simp) + indexValueIso d f ((Equiv.comp_symm_eq f ((mapIso d f) T).color T.color).mp rfl) rw [← Equiv.sum_comp is] refine Finset.sum_congr rfl (fun j _ => ?_) rw [mapIso_apply_coord] @@ -299,8 +290,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT congr exact Equiv.symm_apply_apply f x · apply congrArg - funext a - simp only [IndexValue, mapIso_apply_color, Equiv.symm_apply_apply, is] + exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueIso d f (mapIso.proof_1 d f T))).mp rfl /-! @@ -395,7 +385,10 @@ def unmarkedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where rw [Finset.prod_mul_distrib] rfl +/-- Notation for `markedLorentzAction.smul`. -/ scoped[RealLorentzTensor] infixr:73 " •ₘ " => markedLorentzAction.smul + +/-- Notation for `unmarkedLorentzAction.smul`. -/ scoped[RealLorentzTensor] infixr:73 " •ᵤₘ " => unmarkedLorentzAction.smul /-- Acting on unmarked and then marked indices is equivalent to acting on all indices. -/ diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean index fdd9fcb..0c1b5bb 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean @@ -72,15 +72,10 @@ lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃ rw [mapIso_apply_coord, mapIso_apply_coord] refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl · apply congrArg - ext1 r - cases r with - | inl val => rfl - | inr val_1 => rfl + simp only [IndexValue] + exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl · apply congrArg - ext1 r - cases r with - | inl val => rfl - | inr val_1 => rfl + exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl /-!