-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz :
  Eq.{u_1 + 1} (α := ι)
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'))
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
rwa :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
rwa₁ :
  (P.root : (a : ι) → M)
      (Exists.choose (p := fun (y : ι) ↦
        (P.root : (a : ι) → M) y =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))
        hz) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
rwa₂ :
  Eq.{u_3 + 1} (α := M)
    ((P.root : (a : ι) → M)
        (Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))
          hz) :
      M)
    ((P.root : (a : ι) → M)
        (Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)))
          hz') :
      M)
rwa₃ rwa₄ rwa₅ rwa₆ :
  Exists.choose (p := fun (y : ι) ↦
      (P.root : (a : ι) → M) y =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))
      hz =
    Exists.choose (p := fun (y : ι) ↦
      (P.root : (a : ι) → M) y =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)))
      hz'
⊢ HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)

Tactic:
rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]

Premises used: Exists.choose_spec, Function.Injective.eq_iff, RootPairing.root, Function.Embedding.injective, DFunLike.coe, add_right_inj