-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M)
h' :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
this :
  Eq (α := Set ℤ)
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HSub.hSub (α := M) ((P.root : (a : ι) → M) k : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
    (image (α := ℤ) (⇑(OrderIso.addRight 1) : (a : ℤ) → ℤ)
      {n : ℤ |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)))})
bdd :
  BddAbove (α := ℤ)
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
a :
  sSup
      (image (α := ℤ) (⇑(OrderIso.addRight 1) : (a : ℤ) → ℤ)
        {n : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)))}) =
    HAdd.hAdd (α := ℤ)
      (sSup
        {k : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) k ((P.root : (a : ι) → M) i : M)))})
      1
a₁ :
  (OrderIso.addRight 1 : (a : ℤ) → ℤ)
      (sSup
        {z : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}) =
    HAdd.hAdd (α := ℤ)
      (sSup
        {k : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) k ((P.root : (a : ι) → M) i : M)))})
      1
⊢ sSup
      {k_1 : ℤ |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) k : M)
            (HSMul.hSMul (β := M) k_1 ((P.root : (a : ι) → M) i : M)))} =
    HAdd.hAdd (α := ℤ)
      (sSup
        {k : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) k ((P.root : (a : ι) → M) i : M)))})
      1
have a₂ : HAdd.hAdd (α := ℤ)
    (sSup
      {z : ℤ |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))})
    1 =
  HAdd.hAdd (α := ℤ)
    (sSup
      {k : ℤ |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) k ((P.root : (a : ι) → M) i : M)))})
    1
Tactic: rw [this, ← OrderIso.map_csSup' _ ⟨0, by simp⟩ bdd, OrderIso.addRight_apply]