From 7ff3ad03d7968ab887c1326495acbb16d2ee09de Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 31 Oct 2024 00:45:55 +0000
Subject: [PATCH 1/3] chore (FieldTheory) : lower priority of instance about
 IsScalarTower and subtype (#18436)

Lower the priority of instance `IntermediateField.instIsScalarTowerSubtypeMem` to `900`
Because it would cause trouble when synthize instance `IsScalarTower K L E` where `K < L` are `IntermediateField F E`
---
 Mathlib/FieldTheory/IntermediateField/Basic.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Mathlib/FieldTheory/IntermediateField/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Basic.lean
index 581e1e65e3e36..d1337b2dca3dc 100644
--- a/Mathlib/FieldTheory/IntermediateField/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Basic.lean
@@ -323,9 +323,12 @@ instance smulCommClass_right [SMul X Y] [SMul L Y] [SMulCommClass X L Y]
     (F : IntermediateField K L) : SMulCommClass X F Y :=
   inferInstanceAs (SMulCommClass X F.toSubfield Y)
 
+--note: setting this istance the default priority may trigger trouble to synthize instance
+--for field extension with more than one intermedaite field, example : in a field extension `F/E`,
+--`K₁ ≤ K₂` are of type `intermediatefield F E`, the instance `IsScalarTower K₁ K₂ E`
 /-- Note that this provides `IsScalarTower F K K` which is needed by `smul_mul_assoc`. -/
-instance [SMul X Y] [SMul L X] [SMul L Y] [IsScalarTower L X Y] (F : IntermediateField K L) :
-    IsScalarTower F X Y :=
+instance (priority := 900) [SMul X Y] [SMul L X] [SMul L Y] [IsScalarTower L X Y]
+    (F : IntermediateField K L) : IsScalarTower F X Y :=
   inferInstanceAs (IsScalarTower F.toSubfield X Y)
 
 instance [SMul L X] [FaithfulSMul L X] (F : IntermediateField K L) : FaithfulSMul F X :=

From 169ed0ac01e859ffb2ac01ad3db2bbf621da40fe Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Thu, 31 Oct 2024 02:17:54 +0000
Subject: [PATCH 2/3] feat (RootSystem/Hom): endomorphisms and automorphisms of
 root pairings (#18025)

This PR introduces the root pairing endomorphism monoid and automorphism group, and shows that the representations on weight and coweight spaces are injective.
---
 Mathlib/Algebra/Module/Equiv/Defs.lean    |  12 +
 Mathlib/LinearAlgebra/Dual.lean           |  22 +
 Mathlib/LinearAlgebra/RootSystem/Hom.lean | 507 +++++++++++++++++++++-
 3 files changed, 529 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Algebra/Module/Equiv/Defs.lean b/Mathlib/Algebra/Module/Equiv/Defs.lean
index 430a86911a3e0..cf3df68ab785c 100644
--- a/Mathlib/Algebra/Module/Equiv/Defs.lean
+++ b/Mathlib/Algebra/Module/Equiv/Defs.lean
@@ -391,6 +391,18 @@ theorem toLinearMap_symm_comp_eq (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ 
   · simp [← H, ← e₁₂.toEquiv.symm_comp_eq f g]
   · simp [H, e₁₂.toEquiv.symm_comp_eq f g]
 
+@[simp]
+theorem comp_toLinearMap_eq_iff (f g : M₃ →ₛₗ[σ₃₁] M₁) :
+    e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g := by
+  refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
+  rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]
+
+@[simp]
+theorem eq_comp_toLinearMap_iff (f g : M₂ →ₛₗ[σ₂₃] M₃) :
+    f.comp e₁₂.toLinearMap = g.comp e₁₂.toLinearMap ↔ f = g := by
+  refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
+  rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]
+
 @[simp]
 theorem refl_symm [Module R M] : (refl R M).symm = LinearEquiv.refl R M :=
   rfl
diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean
index 23b6f1f84347a..285e6bf70576b 100644
--- a/Mathlib/LinearAlgebra/Dual.lean
+++ b/Mathlib/LinearAlgebra/Dual.lean
@@ -604,6 +604,28 @@ def evalEquiv : M ≃ₗ[R] Dual R (Dual R M) :=
     (evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M) := by
   ext; simp
 
+@[simp] lemma Dual.eval_comp_comp_evalEquiv_eq
+    {M' : Type*} [AddCommGroup M'] [Module R M'] {f : M →ₗ[R] M'} :
+    Dual.eval R M' ∘ₗ f ∘ₗ (evalEquiv R M).symm = f.dualMap.dualMap := by
+  ext x g
+  simp only [dualMap_apply, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, Dual.eval_apply]
+  rw [← apply_evalEquiv_symm_apply, dualMap_apply]
+
+lemma dualMap_dualMap_eq_iff_of_injective
+    {M' : Type*} [AddCommGroup M'] [Module R M'] {f g : M →ₗ[R] M'}
+    (h : Injective (Dual.eval R M')) :
+    f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g := by
+  simp only [← Dual.eval_comp_comp_evalEquiv_eq]
+  refine ⟨ fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
+    (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap) ⟩
+  rw [propext (cancel_left h), LinearEquiv.eq_comp_toLinearMap_iff] at hfg
+  exact hfg
+
+@[simp] lemma dualMap_dualMap_eq_iff
+    {M' : Type*} [AddCommGroup M'] [Module R M'] [IsReflexive R M'] {f g : M →ₗ[R] M'} :
+    f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g :=
+  dualMap_dualMap_eq_iff_of_injective _ _ (bijective_dual_eval R M').injective
+
 /-- The dual of a reflexive module is reflexive. -/
 instance Dual.instIsReflecive : IsReflexive R (Dual R M) :=
   ⟨by simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective⟩
diff --git a/Mathlib/LinearAlgebra/RootSystem/Hom.lean b/Mathlib/LinearAlgebra/RootSystem/Hom.lean
index 5d58b28dabbf4..08f552e72ccc3 100644
--- a/Mathlib/LinearAlgebra/RootSystem/Hom.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/Hom.lean
@@ -11,13 +11,34 @@ This file defines morphisms of root pairings, following the definition of morphi
 given in SGA III Exp. 21 Section 6.
 
 ## Main definitions:
- * `Hom`: A morphism of root data is a linear map of weight spaces, its transverse on coweight
+ * `Hom`: A morphism of root pairings is a linear map of weight spaces, its transverse on coweight
    spaces, and a bijection on the set that indexes roots and coroots.
  * `Hom.id`: The identity morphism.
  * `Hom.comp`: The composite of two morphisms.
+ * `End`: The endomorphism monoid of a root pairing.
+ * `Hom.weightHom`: The homomorphism from the endomorphism monoid to linear endomorphisms on the
+   weight space.
+ * `Hom.coweightHom`: The homomorphism from the endomorphism monoid to the opposite monoid of linear
+   endomorphisms on the coweight space.
+ * `Equiv`: An equivalence of root pairings is a morphism for which the maps on weight spaces and
+   coweight spaces are bijective.
+ * `Equiv.toHom`: The morphism underlying an equivalence.
+ * `Equiv.weightEquiv`: The linear isomorphism on weight spaces given by an equivalence.
+ * `Equiv.coweightEquiv`: The linear isomorphism on coweight spaces given by an equivalence.
+ * `Equiv.id`: The identity equivalence.
+ * `Equiv.comp`: The composite of two equivalences.
+ * `Equiv.symm`: The inverse of an equivalence.
+ * `Aut`: The automorphism group of a root pairing.
+ * `Equiv.toEndUnit`: The group isomorphism between the automorphism group of a root pairing and the
+   group of invertible endomorphisms.
+ * `Equiv.weightHom`: The homomorphism from the automorphism group to linear automorphisms on the
+   weight space.
+ * `Equiv.coweightHom`: The homomorphism from the automorphism group to the opposite group of linear
+   automorphisms on the coweight space.
+ * `Equiv.reflection`: The automorphism of a root pairing given by reflection in a root and
+   coreflection in the corresponding coroot.
 
 ## TODO
-
  * Special types of morphisms: Isogenies, weight/coweight space embeddings
  * Weyl group reimplementation?
 
@@ -47,9 +68,29 @@ structure Hom {ι₂ M₂ N₂ : Type*}
   root_weightMap : weightMap ∘ P.root = Q.root ∘ indexEquiv
   coroot_coweightMap : coweightMap ∘ Q.coroot = P.coroot ∘ indexEquiv.symm
 
+namespace Hom
+
+lemma weight_coweight_transpose_apply {ι₂ M₂ N₂ : Type*}
+    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (x : N₂) (f : Hom P Q) :
+    f.weightMap.dualMap (Q.toDualRight x) = P.toDualRight (f.coweightMap x) :=
+  Eq.mp (propext LinearMap.ext_iff) f.weight_coweight_transpose x
+
+lemma root_weightMap_apply {ι₂ M₂ N₂ : Type*}
+    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι) (f : Hom P Q) :
+    f.weightMap (P.root i) = Q.root (f.indexEquiv i) :=
+  Eq.mp (propext funext_iff) f.root_weightMap i
+
+lemma coroot_coweightMap_apply {ι₂ M₂ N₂ : Type*}
+    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι₂) (f : Hom P Q) :
+    f.coweightMap (Q.coroot i) = P.coroot (f.indexEquiv.symm i) :=
+  Eq.mp (propext funext_iff) f.coroot_coweightMap i
+
 /-- The identity morphism of a root pairing. -/
 @[simps!]
-def Hom.id (P : RootPairing ι R M N) : Hom P P where
+def id (P : RootPairing ι R M N) : Hom P P where
   weightMap := LinearMap.id
   coweightMap := LinearMap.id
   indexEquiv := Equiv.refl ι
@@ -59,7 +100,7 @@ def Hom.id (P : RootPairing ι R M N) : Hom P P where
 
 /-- Composition of morphisms -/
 @[simps!]
-def Hom.comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁]
+def comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁]
     [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
     {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂}
     (g : Hom P₁ P₂) (f : Hom P P₁) : Hom P P₂ where
@@ -82,31 +123,451 @@ def Hom.comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Modu
     simp
 
 @[simp]
-lemma Hom.id_comp {ι₂ M₂ N₂ : Type*}
+lemma id_comp {ι₂ M₂ N₂ : Type*}
     [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
     (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : Hom P Q) :
-    Hom.comp f (Hom.id P) = f := by
+    comp f (id P) = f := by
   ext x <;> simp
 
 @[simp]
-lemma Hom.comp_id {ι₂ M₂ N₂ : Type*}
+lemma comp_id {ι₂ M₂ N₂ : Type*}
     [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
     (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : Hom P Q) :
-    Hom.comp (Hom.id Q) f = f := by
+    comp (id Q) f = f := by
   ext x <;> simp
 
 @[simp]
-lemma Hom.comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁]
+lemma comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁]
     [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
     [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N}
     {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃}
     (h : Hom P₂ P₃) (g : Hom P₁ P₂) (f : Hom P P₁) :
-    Hom.comp (Hom.comp h g) f = Hom.comp h (Hom.comp g f) := by
+    comp (comp h g) f = comp h (comp g f) := by
   ext <;> simp
 
-/-- The endomorphism of a root pairing given by a reflection. -/
+/-- The endomorphism monoid of a root pairing. -/
+instance (P : RootPairing ι R M N) : Monoid (Hom P P) where
+  mul := comp
+  mul_assoc := comp_assoc
+  one := id P
+  one_mul := id_comp P P
+  mul_one := comp_id P P
+
+@[simp]
+lemma weightMap_one (P : RootPairing ι R M N) :
+    weightMap (P := P) (Q := P) 1 = LinearMap.id (R := R) (M := M) :=
+  rfl
+
+@[simp]
+lemma coweightMap_one (P : RootPairing ι R M N) :
+    coweightMap (P := P) (Q := P) 1 = LinearMap.id (R := R) (M := N) :=
+  rfl
+
+@[simp]
+lemma indexEquiv_one (P : RootPairing ι R M N) :
+    indexEquiv (P := P) (Q := P) 1 = Equiv.refl ι :=
+  rfl
+
+@[simp]
+lemma weightMap_mul (P : RootPairing ι R M N) (x y : Hom P P) :
+    weightMap (x * y) = weightMap x ∘ₗ weightMap y :=
+  rfl
+
+@[simp]
+lemma coweightMap_mul (P : RootPairing ι R M N) (x y : Hom P P) :
+    coweightMap (x * y) = coweightMap y ∘ₗ coweightMap x :=
+  rfl
+
+@[simp]
+lemma indexEquiv_mul (P : RootPairing ι R M N) (x y : Hom P P) :
+    indexEquiv (x * y) = indexEquiv x ∘ indexEquiv y :=
+  rfl
+
+/-- The endomorphism monoid of a root pairing. -/
+abbrev _root_.RootPairing.End (P : RootPairing ι R M N) := Hom P P
+
+/-- The weight space representation of endomorphisms -/
+def weightHom (P : RootPairing ι R M N) : End P →* (Module.End R M) where
+  toFun g := Hom.weightMap (P := P) (Q := P) g
+  map_mul' g h := by ext; simp
+  map_one' := by ext; simp
+
+lemma weightHom_injective (P : RootPairing ι R M N) : Injective (weightHom P) := by
+  intro f g hfg
+  ext x
+  · exact LinearMap.congr_fun hfg x
+  · refine (LinearEquiv.injective P.toDualRight) ?_
+    simp_rw [← weight_coweight_transpose_apply]
+    exact congrFun (congrArg DFunLike.coe (congrArg LinearMap.dualMap hfg)) (P.toDualRight x)
+  · refine (Embedding.injective P.root) ?_
+    simp_rw [← root_weightMap_apply]
+    exact congrFun (congrArg DFunLike.coe hfg) (P.root x)
+
+/-- The coweight space representation of endomorphisms -/
+def coweightHom (P : RootPairing ι R M N) : End P →* (N →ₗ[R] N)ᵐᵒᵖ where
+  toFun g := MulOpposite.op (Hom.coweightMap (P := P) (Q := P) g)
+  map_mul' g h := by
+    simp only [← MulOpposite.op_mul, coweightMap_mul, LinearMap.mul_eq_comp]
+  map_one' := by
+    simp only [MulOpposite.op_eq_one_iff, coweightMap_one, LinearMap.one_eq_id]
+
+lemma coweightHom_injective (P : RootPairing ι R M N) : Injective (coweightHom P) := by
+  intro f g hfg
+  ext x
+  · dsimp [coweightHom] at hfg
+    rw [MulOpposite.op_inj] at hfg
+    have h := congrArg (LinearMap.comp (M₃ := Module.Dual R M)
+        (σ₂₃ := RingHom.id R) (P.toDualRight)) hfg
+    rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h
+    have : f.weightMap = g.weightMap := by
+      haveI : Module.IsReflexive R M := PerfectPairing.reflexive_left P.toPerfectPairing
+      refine (Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
+        ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))
+    exact congrFun (congrArg DFunLike.coe this) x
+  · dsimp [coweightHom] at hfg
+    simp_all only [MulOpposite.op_inj]
+  · dsimp [coweightHom] at hfg
+    rw [MulOpposite.op_inj] at hfg
+    set y := f.indexEquiv x with hy
+    have : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y) := by
+      exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)
+    rw [coroot_coweightMap_apply, coroot_coweightMap_apply, Embedding.apply_eq_iff_eq, hy] at this
+    rw [Equiv.symm_apply_apply] at this
+    rw [this, Equiv.apply_symm_apply]
+
+end Hom
+
+variable {ι₂ M₂ N₂ : Type*}
+    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂)
+
+/-- An equivalence of root pairings is a morphism where the maps of weight and coweight spaces are
+bijective.
+
+See also `RootPairing.Equiv.toEndUnit`. -/
+@[ext]
+protected structure Equiv extends Hom P Q where
+  bijective_weightMap : Bijective weightMap
+  bijective_coweightMap : Bijective coweightMap
+
+attribute [coe] Equiv.toHom
+
+/-- The root pairing homomorphism underlying an equivalence. -/
+add_decl_doc Equiv.toHom
+
+namespace Equiv
+
+/-- The linear equivalence of weight spaces given by an equivalence of root pairings. -/
+def weightEquiv (e : RootPairing.Equiv P Q) : M ≃ₗ[R] M₂ :=
+    LinearEquiv.ofBijective _ e.bijective_weightMap
+
+@[simp]
+lemma weightEquiv_apply (e : RootPairing.Equiv P Q) (m : M) :
+    weightEquiv P Q e m = e.toHom.weightMap m :=
+  rfl
+
+@[simp]
+lemma weightEquiv_symm_weightMap (e : RootPairing.Equiv P Q) (m : M) :
+    (weightEquiv P Q e).symm (e.toHom.weightMap m) = m :=
+  (LinearEquiv.symm_apply_eq (weightEquiv P Q e)).mpr rfl
+
+@[simp]
+lemma weightMap_weightEquiv_symm (e : RootPairing.Equiv P Q) (m : M₂) :
+    e.toHom.weightMap ((weightEquiv P Q e).symm m) = m := by
+  rw [← weightEquiv_apply]
+  exact LinearEquiv.apply_symm_apply (weightEquiv P Q e) m
+
+/-- The contravariant equivalence of coweight spaces given by an equivalence of root pairings. -/
+def coweightEquiv (e : RootPairing.Equiv P Q) : N₂ ≃ₗ[R] N :=
+  LinearEquiv.ofBijective _ e.bijective_coweightMap
+
+@[simp]
+lemma coweightEquiv_apply (e : RootPairing.Equiv P Q) (n : N₂) :
+    coweightEquiv P Q e n = e.toHom.coweightMap n :=
+  rfl
+
+@[simp]
+lemma coweightEquiv_symm_coweightMap (e : RootPairing.Equiv P Q) (n : N₂) :
+    (coweightEquiv P Q e).symm (e.toHom.coweightMap n) = n :=
+  (LinearEquiv.symm_apply_eq (coweightEquiv P Q e)).mpr rfl
+
+@[simp]
+lemma coweightMap_coweightEquiv_symm (e : RootPairing.Equiv P Q) (n : N) :
+    e.toHom.coweightMap ((coweightEquiv P Q e).symm n) = n := by
+  rw [← coweightEquiv_apply]
+  exact LinearEquiv.apply_symm_apply (coweightEquiv P Q e) n
+
+/-- The identity equivalence of a root pairing. -/
+@[simps!]
+def id (P : RootPairing ι R M N) : RootPairing.Equiv P P :=
+  { Hom.id P with
+    bijective_weightMap := _root_.id bijective_id
+    bijective_coweightMap := _root_.id bijective_id }
+
+/-- Composition of equivalences -/
 @[simps!]
-def Hom.reflection (P : RootPairing ι R M N) (i : ι) : Hom P P where
+def comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁]
+    [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂}
+    (g : RootPairing.Equiv P₁ P₂) (f : RootPairing.Equiv P P₁) : RootPairing.Equiv P P₂ :=
+  { Hom.comp g.toHom f.toHom with
+    bijective_weightMap := by
+      simp only [Hom.comp, LinearMap.coe_comp]
+      exact Bijective.comp g.bijective_weightMap f.bijective_weightMap
+    bijective_coweightMap := by
+      simp only [Hom.comp, LinearMap.coe_comp]
+      exact Bijective.comp f.bijective_coweightMap g.bijective_coweightMap }
+
+@[simp]
+lemma toHom_comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁]
+    [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂}
+    (g : RootPairing.Equiv P₁ P₂) (f : RootPairing.Equiv P P₁) :
+    (Equiv.comp g f).toHom = Hom.comp g.toHom f.toHom := by
+  rfl
+
+@[simp]
+lemma id_comp {ι₂ M₂ N₂ : Type*}
+    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) :
+    comp f (id P) = f := by
+  ext x <;> simp
+
+@[simp]
+lemma comp_id {ι₂ M₂ N₂ : Type*}
+    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) :
+    comp (id Q) f = f := by
+  ext x <;> simp
+
+@[simp]
+lemma comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁]
+    [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N}
+    {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃}
+    (h : RootPairing.Equiv P₂ P₃) (g : RootPairing.Equiv P₁ P₂) (f : RootPairing.Equiv P P₁) :
+    comp (comp h g) f = comp h (comp g f) := by
+  ext <;> simp
+
+/-- The endomorphism monoid of a root pairing. -/
+instance (P : RootPairing ι R M N) : Monoid (RootPairing.Equiv P P) where
+  mul := comp
+  mul_assoc := comp_assoc
+  one := id P
+  one_mul := id_comp P P
+  mul_one := comp_id P P
+
+@[simp]
+lemma weightEquiv_one (P : RootPairing ι R M N) :
+    weightEquiv (P := P) (Q := P) 1 = LinearMap.id (R := R) (M := M) :=
+  rfl
+
+@[simp]
+lemma coweightEquiv_one (P : RootPairing ι R M N) :
+    coweightEquiv (P := P) (Q := P) 1 = LinearMap.id (R := R) (M := N) :=
+  rfl
+
+@[simp]
+lemma toHom_one (P : RootPairing ι R M N) :
+    (1 : RootPairing.Equiv P P).toHom = (1 : RootPairing.Hom P P) :=
+  rfl
+
+@[simp]
+lemma mul_eq_comp {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
+    x * y = Equiv.comp x y :=
+  rfl
+
+@[simp]
+lemma weightEquiv_comp_toLin {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
+    weightEquiv P P (Equiv.comp x y) = weightEquiv P P y ≪≫ₗ weightEquiv P P x := by
+  ext; simp
+
+@[simp]
+lemma weightEquiv_mul {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
+    weightEquiv P P x * weightEquiv P P y = weightEquiv P P y ≪≫ₗ weightEquiv P P x := by
+  rfl
+
+@[simp]
+lemma coweightEquiv_comp_toLin {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
+    coweightEquiv P P (Equiv.comp x y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y := by
+  ext; simp
+
+@[simp]
+lemma coweightEquiv_mul {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
+    coweightEquiv P P x * coweightEquiv P P y = coweightEquiv P P y ≪≫ₗ coweightEquiv P P x := by
+  rfl
+
+/-- The inverse of a root pairing equivalence. -/
+def symm {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
+    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) :
+    RootPairing.Equiv Q P where
+  weightMap := (weightEquiv P Q f).symm
+  coweightMap := (coweightEquiv P Q f).symm
+  indexEquiv := f.indexEquiv.symm
+  weight_coweight_transpose := by
+    ext n m
+    nth_rw 2 [show m = (weightEquiv P Q f) ((weightEquiv P Q f).symm m) by
+      exact (LinearEquiv.symm_apply_eq (weightEquiv P Q f)).mp rfl]
+    nth_rw 1 [show n = (coweightEquiv P Q f) ((coweightEquiv P Q f).symm n) by
+      exact (LinearEquiv.symm_apply_eq (coweightEquiv P Q f)).mp rfl]
+    have := f.weight_coweight_transpose
+    rw [LinearMap.ext_iff₂] at this
+    exact Eq.symm (this ((coweightEquiv P Q f).symm n) ((weightEquiv P Q f).symm m))
+  root_weightMap := by
+    ext i
+    simp only [LinearEquiv.coe_coe, comp_apply]
+    have := f.root_weightMap
+    rw [funext_iff] at this
+    specialize this (f.indexEquiv.symm i)
+    simp only [comp_apply, Equiv.apply_symm_apply] at this
+    simp [← this]
+  coroot_coweightMap := by
+    ext i
+    simp only [LinearEquiv.coe_coe, comp_apply, Equiv.symm_symm]
+    have := f.coroot_coweightMap
+    rw [funext_iff] at this
+    specialize this (f.indexEquiv i)
+    simp only [comp_apply, Equiv.symm_apply_apply] at this
+    simp [← this]
+  bijective_weightMap := by
+    simp only [LinearEquiv.coe_coe]
+    exact LinearEquiv.bijective (weightEquiv P Q f).symm
+  bijective_coweightMap := by
+    simp only [LinearEquiv.coe_coe]
+    exact LinearEquiv.bijective (coweightEquiv P Q f).symm
+
+@[simp]
+lemma inv_weightMap {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂]
+    [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂)
+    (f : RootPairing.Equiv P Q) : (symm P Q f).weightMap = (weightEquiv P Q f).symm :=
+  rfl
+
+@[simp]
+lemma inv_coweightMap {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂]
+    [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂)
+    (f : RootPairing.Equiv P Q) : (symm P Q f).coweightMap = (coweightEquiv P Q f).symm :=
+  rfl
+
+@[simp]
+lemma inv_indexEquiv {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂]
+    [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂)
+    (f : RootPairing.Equiv P Q) : (symm P Q f).indexEquiv = (Hom.indexEquiv f.toHom).symm :=
+  rfl
+
+/-- The endomorphism monoid of a root pairing. -/
+instance (P : RootPairing ι R M N) : Group (RootPairing.Equiv P P) where
+  mul := comp
+  mul_assoc := comp_assoc
+  one := id P
+  one_mul := id_comp P P
+  mul_one := comp_id P P
+  inv := symm P P
+  inv_mul_cancel e := by
+    ext m
+    · rw [← weightEquiv_apply]
+      simp
+    · rw [← coweightEquiv_apply]
+      simp
+    · simp
+
+end Equiv
+
+/-- The automorphism group of a root pairing. -/
+abbrev Aut (P : RootPairing ι R M N) := (RootPairing.Equiv P P)
+
+namespace Equiv
+
+/-- The isomorphism between the automorphism group of a root pairing and the group of invertible
+endomorphisms. -/
+def toEndUnit (P : RootPairing ι R M N) : Aut P ≃* (End P)ˣ where
+  toFun f :=
+  { val :=  f.toHom
+    inv := (Equiv.symm P P f).toHom
+    val_inv := by ext <;> simp
+    inv_val := by ext <;> simp }
+  invFun f :=
+  { f.val with
+    bijective_weightMap := by
+      refine bijective_iff_has_inverse.mpr ?_
+      use f.inv.weightMap
+      constructor
+      · refine leftInverse_iff_comp.mpr ?_
+        simp only [← @LinearMap.coe_comp]
+        rw [← Hom.weightMap_mul, f.inv_val, Hom.weightMap_one, LinearMap.id_coe]
+      · refine rightInverse_iff_comp.mpr ?_
+        simp only [← @LinearMap.coe_comp]
+        rw [← Hom.weightMap_mul, f.val_inv, Hom.weightMap_one, LinearMap.id_coe]
+    bijective_coweightMap := by
+      refine bijective_iff_has_inverse.mpr ?_
+      use f.inv.coweightMap
+      constructor
+      · refine leftInverse_iff_comp.mpr ?_
+        simp only [← @LinearMap.coe_comp]
+        rw [← Hom.coweightMap_mul, f.val_inv, Hom.coweightMap_one, LinearMap.id_coe]
+      · refine rightInverse_iff_comp.mpr ?_
+        simp only [← @LinearMap.coe_comp]
+        rw [← Hom.coweightMap_mul, f.inv_val, Hom.coweightMap_one, LinearMap.id_coe] }
+  left_inv f := by simp
+  right_inv f := by simp
+  map_mul' f g := by
+    simp only [Equiv.mul_eq_comp, Equiv.toHom_comp]
+    ext <;> simp
+
+lemma toEndUnit_val (P : RootPairing ι R M N) (g : Aut P) : (toEndUnit P g).val = g.toHom :=
+  rfl
+
+lemma toEndUnit_inv (P : RootPairing ι R M N) (g : Aut P) :
+    (toEndUnit P g).inv = (symm P P g).toHom :=
+  rfl
+
+/-- The weight space representation of automorphisms -/
+@[simps]
+def weightHom (P : RootPairing ι R M N) : Aut P →* (M ≃ₗ[R] M) where
+  toFun := weightEquiv P P
+  map_one' := by ext; simp
+  map_mul' x y := by ext; simp
+
+lemma weightHom_toLinearMap {P : RootPairing ι R M N} (g : Aut P) :
+    ((weightHom P) g).toLinearMap = (Hom.weightHom P) g.toHom :=
+  rfl
+
+lemma weightHom_injective (P : RootPairing ι R M N) : Injective (Equiv.weightHom P) := by
+  refine Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_
+  let h : ((weightHom P) g).toLinearMap = ((weightHom P) g').toLinearMap := hgg' --`have` gets lint
+  rw [weightHom_toLinearMap, weightHom_toLinearMap] at h
+  suffices h' : g.toHom = g'.toHom by
+    exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')
+  exact Hom.weightHom_injective P hgg'
+
+/-- The coweight space representation of automorphisms -/
+@[simps]
+def coweightHom (P : RootPairing ι R M N) : Aut P →* (N ≃ₗ[R] N)ᵐᵒᵖ where
+  toFun g := MulOpposite.op ((coweightEquiv P P) g)
+  map_one' := by
+    simp only [MulOpposite.op_eq_one_iff]
+    exact LinearEquiv.toLinearMap_inj.mp rfl
+  map_mul' := by
+    simp only [mul_eq_comp, coweightEquiv_comp_toLin]
+    exact fun x y ↦ rfl
+
+lemma coweightHom_toLinearMap {P : RootPairing ι R M N} (g : Aut P) :
+    (MulOpposite.unop ((coweightHom P) g)).toLinearMap =
+      MulOpposite.unop ((Hom.coweightHom P) g.toHom) :=
+  rfl
+
+lemma coweightHom_injective (P : RootPairing ι R M N) : Injective (Equiv.coweightHom P) := by
+  refine Injective.of_comp (f := fun a => MulOpposite.op a) fun g g' hgg' => ?_
+  have h : (MulOpposite.unop ((coweightHom P) g)).toLinearMap =
+      (MulOpposite.unop ((coweightHom P) g')).toLinearMap := by
+    simp_all
+  rw [coweightHom_toLinearMap, coweightHom_toLinearMap] at h
+  suffices h' : g.toHom = g'.toHom by
+    exact Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')
+  apply Hom.coweightHom_injective P
+  exact MulOpposite.unop_inj.mp h
+
+/-- The automorphism of a root pairing given by a reflection. -/
+def reflection (P : RootPairing ι R M N) (i : ι) : Aut P where
   weightMap := P.reflection i
   coweightMap := P.coreflection i
   indexEquiv := P.reflection_perm i
@@ -121,5 +582,27 @@ def Hom.reflection (P : RootPairing ι R M N) (i : ι) : Hom P P where
     simp only [PerfectPairing.toLin_apply, PerfectPairing.flip_apply_apply, mul_comm]
   root_weightMap := by ext; simp
   coroot_coweightMap := by ext; simp
+  bijective_weightMap := by
+    simp only [LinearEquiv.coe_coe]
+    exact LinearEquiv.bijective (P.reflection i)
+  bijective_coweightMap := by
+    simp only [LinearEquiv.coe_coe]
+    exact LinearEquiv.bijective (P.coreflection i)
+
+@[simp]
+lemma reflection_weightEquiv (P : RootPairing ι R M N) (i : ι) :
+    (reflection P i).weightEquiv = P.reflection i :=
+  LinearEquiv.toLinearMap_inj.mp rfl
+
+@[simp]
+lemma reflection_coweightEquiv (P : RootPairing ι R M N) (i : ι) :
+    (reflection P i).coweightEquiv = P.coreflection i :=
+  LinearEquiv.toLinearMap_inj.mp rfl
+
+@[simp]
+lemma reflection_indexEquiv (P : RootPairing ι R M N) (i : ι) :
+    (reflection P i).indexEquiv = P.reflection_perm i := rfl
+
+end Equiv
 
 end RootPairing

From 422ea74d915b0260de8caceb10d189e3f054a09d Mon Sep 17 00:00:00 2001
From: Johannes Choo <jhanschoo@gmail.com>
Date: Thu, 31 Oct 2024 02:46:24 +0000
Subject: [PATCH 3/3] chore(Computability/TuringMachine): change uses of
 `get(?)` to `getElem(?)` (#18367)

Update `Computability/TuringMachine` to not use deprecated `List.get` and `List.get?` lemmas.

In addition, a couple missing lemmas were added to `Data/List/GetD` to
support this change.
---
 Mathlib/Computability/TuringMachine.lean | 69 +++++++++++-------------
 Mathlib/Data/List/GetD.lean              |  3 ++
 2 files changed, 33 insertions(+), 39 deletions(-)

diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
index a9037ff96e553..a75fdceac64eb 100644
--- a/Mathlib/Computability/TuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine.lean
@@ -60,12 +60,6 @@ Given these parameters, there are a few common structures for the model that ari
 
 assert_not_exists MonoidWithZero
 
--- After https://github.com/leanprover/lean4/pull/4400
--- the simp normal forms for `List` lookup use the `GetElem` typeclass, rather than `List.get?`.
--- This file has not been updated to reflect that change, so uses a number of deprecated lemmas.
--- Updating this file to allow restoring the deprecation linter would be much appreciated.
-set_option linter.deprecated false
-
 open Mathlib (Vector)
 open Relation
 
@@ -262,8 +256,7 @@ def ListBlank.nth {Γ} [Inhabited Γ] (l : ListBlank Γ) (n : ℕ) : Γ := by
   rw [List.getI_eq_default _ h]
   rcases le_or_lt _ n with h₂ | h₂
   · rw [List.getI_eq_default _ h₂]
-  rw [List.getI_eq_get _ h₂, List.get_eq_getElem, List.getElem_append_right h,
-    List.getElem_replicate]
+  rw [List.getI_eq_getElem _ h₂, List.getElem_append_right h, List.getElem_replicate]
 
 @[simp]
 theorem ListBlank.nth_mk {Γ} [Inhabited Γ] (l : List Γ) (n : ℕ) :
@@ -290,14 +283,13 @@ theorem ListBlank.ext {Γ} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} :
     intro
     rw [H]
   refine Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, ?_⟩)
-  refine List.ext_get ?_ fun i h h₂ ↦ Eq.symm ?_
+  refine List.ext_getElem ?_ fun i h h₂ ↦ Eq.symm ?_
   · simp only [Nat.add_sub_cancel' h, List.length_append, List.length_replicate]
   simp only [ListBlank.nth_mk] at H
   cases' lt_or_le i l₁.length with h' h'
-  · simp only [List.get_append _ h', List.get?_eq_get h, List.get?_eq_get h',
-      ← List.getI_eq_get _ h, ← List.getI_eq_get _ h', H]
-  · simp only [List.get_append_right' h', List.get_replicate, List.get?_eq_get h,
-      List.get?_len_le h', ← List.getI_eq_default _ h', H, List.getI_eq_get _ h]
+  · simp [h', List.getElem_append _ h₂, ← List.getI_eq_getElem _ h, ← List.getI_eq_getElem _ h', H]
+  · rw [List.getElem_append_right h', List.getElem_replicate,
+      ← List.getI_eq_default _ h', H, List.getI_eq_getElem _ h]
 
 /-- Apply a function to a value stored at the nth position of the list. -/
 @[simp]
@@ -380,10 +372,9 @@ theorem ListBlank.nth_map {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMa
   refine l.inductionOn fun l ↦ ?_
   -- Porting note: Added `suffices` to get `simp` to work.
   suffices ((mk l).map f).nth n = f ((mk l).nth n) by exact this
-  simp only [List.get?_map, ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_iget_get?]
-  cases l.get? n
-  · exact f.2.symm
-  · rfl
+  simp only [ListBlank.map_mk, ListBlank.nth_mk, ← List.getD_default_eq_getI]
+  rw [← List.getD_map _ _ f]
+  simp
 
 /-- The `i`-th projection as a pointed map. -/
 def proj {ι : Type*} {Γ : ι → Type*} [∀ i, Inhabited (Γ i)] (i : ι) :
@@ -425,10 +416,10 @@ def ListBlank.bind {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (l : ListBlank Γ) (f
     (hf : ∃ n, f default = List.replicate n default) : ListBlank Γ' := by
   apply l.liftOn (fun l ↦ ListBlank.mk (List.bind l f))
   rintro l _ ⟨i, rfl⟩; cases' hf with n e; refine Quotient.sound' (Or.inl ⟨i * n, ?_⟩)
-  rw [List.append_bind, mul_comm]; congr
+  rw [List.bind_append, mul_comm]; congr
   induction' i with i IH
   · rfl
-  simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ, List.cons_bind]
+  simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ, List.bind_cons]
 
 @[simp]
 theorem ListBlank.bind_mk {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (l : List Γ) (f : Γ → List Γ') (hf) :
@@ -441,7 +432,7 @@ theorem ListBlank.cons_bind {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (a : Γ) (l
   refine l.inductionOn fun l ↦ ?_
   -- Porting note: Added `suffices` to get `simp` to work.
   suffices ((mk l).cons a).bind f hf = ((mk l).bind f hf).append (f a) by exact this
-  simp only [ListBlank.append_mk, ListBlank.bind_mk, ListBlank.cons_mk, List.cons_bind]
+  simp only [ListBlank.append_mk, ListBlank.bind_mk, ListBlank.cons_mk, List.bind_cons]
 
 /-- The tape of a Turing machine is composed of a head element (which we imagine to be the
 current position of the head), together with two `ListBlank`s denoting the portions of the tape
@@ -2101,10 +2092,10 @@ namespace TM2to1
 -- A displaced lemma proved in unnecessary generality
 theorem stk_nth_val {K : Type*} {Γ : K → Type*} {L : ListBlank (∀ k, Option (Γ k))} {k S} (n)
     (hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse) :
-    L.nth n k = S.reverse.get? n := by
-  rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk, List.getI_eq_iget_get?,
-    List.get?_map]
-  cases S.reverse.get? n <;> rfl
+    L.nth n k = S.reverse[n]? := by
+  rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk,
+    List.getI_eq_iget_getElem?, List.getElem?_map]
+  cases S.reverse[n]? <;> rfl
 
 variable {K : Type*}
 variable {Γ : K → Type*}
@@ -2322,10 +2313,10 @@ theorem tr_respects_aux₂ [DecidableEq K] {k : K} {q : Stmt₂₁} {v : σ} {S
     · subst k'
       split_ifs with h
         <;> simp only [List.reverse_cons, Function.update_same, ListBlank.nth_mk, List.map]
-      -- Porting note: `le_refl` is required.
-      · rw [List.getI_eq_get, List.get_append_right'] <;>
-          simp only [List.length_singleton, h, List.length_reverse, List.length_map, Nat.sub_self,
-            Fin.zero_eta, List.get_cons_zero, le_refl, List.length_append, Nat.lt_succ_self]
+      · rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
+        simp only [List.length_append, List.length_reverse, List.length_map, ← h,
+          Nat.sub_self, List.length_singleton, List.getElem_singleton,
+          le_refl, Nat.lt_succ_self]
       rw [← proj_map_nth, hL, ListBlank.nth_mk]
       cases' lt_or_gt_of_ne h with h h
       · rw [List.getI_append]
@@ -2342,7 +2333,7 @@ theorem tr_respects_aux₂ [DecidableEq K] {k : K} {q : Stmt₂₁} {v : σ} {S
     cases e : S k; · rfl
     rw [List.length_cons, iterate_succ', Function.comp, Tape.move_right_left,
       Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hL k), e,
-      List.reverse_cons, ← List.length_reverse, List.get?_concat_length]
+      List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]
     rfl
   | pop f =>
     cases' e : S k with hd tl
@@ -2357,8 +2348,8 @@ theorem tr_respects_aux₂ [DecidableEq K] {k : K} {q : Stmt₂₁} {v : σ} {S
             Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k none),
             addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
             stk_nth_val _ (hL k), e,
-            show (List.cons hd tl).reverse.get? tl.length = some hd by
-              rw [List.reverse_cons, ← List.length_reverse, List.get?_concat_length],
+            show (List.cons hd tl).reverse[tl.length]? = some hd by
+              rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
             List.head?, List.tail]⟩
       refine ListBlank.ext fun i ↦ ?_
       rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
@@ -2411,7 +2402,7 @@ theorem tr_respects_aux₁ {k} (o q v) {S : List (Γ k)} {L : ListBlank (∀ k,
   rw [iterate_succ_apply']
   simp only [TM1.step, TM1.stepAux, tr, Tape.mk'_nth_nat, Tape.move_right_n_head,
     addBottom_nth_snd, Option.mem_def]
-  rw [stk_nth_val _ hL, List.get?_eq_get]
+  rw [stk_nth_val _ hL, List.getElem?_eq_getElem]
   · rfl
   · rwa [List.length_reverse]
 
@@ -2438,8 +2429,8 @@ theorem tr_respects_aux {q v T k} {S : ∀ k, List (Γ k)}
   obtain ⟨T', hT', hrun⟩ := tr_respects_aux₂ (Λ := Λ) hT o
   have := hgo.tail' rfl
   rw [tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd,
-    stk_nth_val _ (hT k), List.get?_len_le (le_of_eq (List.length_reverse _)), Option.isNone, cond,
-    hrun, TM1.stepAux] at this
+    stk_nth_val _ (hT k), List.getElem?_len_le (le_of_eq (List.length_reverse _)),
+    Option.isNone, cond, hrun, TM1.stepAux] at this
   obtain ⟨c, gc, rc⟩ := IH hT'
   refine ⟨c, gc, (this.to₀.trans (tr_respects_aux₃ M _) c (TransGen.head' rfl ?_)).to_reflTransGen⟩
   rw [tr, TM1.stepAux, Tape.mk'_head, addBottom_head_fst]
@@ -2474,18 +2465,18 @@ theorem trCfg_init (k) (L : List (Γ k)) : TrCfg (TM2.init k L) (TM1.init (trIni
   rw [(_ : TM1.init _ = _)]
   · refine ⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ ?_⟩
     refine ListBlank.ext fun i ↦ ?_
-    rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_iget_get?, List.map_map]
+    rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_iget_getElem?, List.map_map]
     have : ((proj k').f ∘ fun a => update (β := fun k => Option (Γ k)) default k (some a))
       = fun a => (proj k').f (update (β := fun k => Option (Γ k)) default k (some a)) := rfl
-    rw [this, List.get?_map, proj, PointedMap.mk_val]
+    rw [this, List.getElem?_map, proj, PointedMap.mk_val]
     simp only []
     by_cases h : k' = k
     · subst k'
       simp only [Function.update_same]
-      rw [ListBlank.nth_mk, List.getI_eq_iget_get?, ← List.map_reverse, List.get?_map]
+      rw [ListBlank.nth_mk, List.getI_eq_iget_getElem?, ← List.map_reverse, List.getElem?_map]
     · simp only [Function.update_noteq h]
-      rw [ListBlank.nth_mk, List.getI_eq_iget_get?, List.map, List.reverse_nil]
-      cases L.reverse.get? i <;> rfl
+      rw [ListBlank.nth_mk, List.getI_eq_iget_getElem?, List.map, List.reverse_nil]
+      cases L.reverse[i]? <;> rfl
   · rw [trInit, TM1.init]
     congr <;> cases L.reverse <;> try rfl
     simp only [List.map_map, List.tail_cons, List.map]
diff --git a/Mathlib/Data/List/GetD.lean b/Mathlib/Data/List/GetD.lean
index e16ce04be7e33..33af5b90cdb00 100644
--- a/Mathlib/Data/List/GetD.lean
+++ b/Mathlib/Data/List/GetD.lean
@@ -129,6 +129,9 @@ theorem getI_append_right (l l' : List α) (n : ℕ) (h : l.length ≤ n) :
 theorem getI_eq_iget_get? (n : ℕ) : l.getI n = (l.get? n).iget := by
   rw [← getD_default_eq_getI, getD_eq_getD_get?, Option.getD_default_eq_iget]
 
+theorem getI_eq_iget_getElem? (n : ℕ) : l.getI n = l[n]?.iget := by
+  rw [← getD_default_eq_getI, getD_eq_getElem?_getD, Option.getD_default_eq_iget]
+
 theorem getI_zero_eq_headI : l.getI 0 = l.headI := by cases l <;> rfl
 
 end getI