-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
hij :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
zero :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) 0 ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
succ :
  ∀ (w : ℕ)
    (hw :
      ∀ {i k : ι} (hi : b.IsPos i)
        (hk :
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
        (hij :
          LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
            (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
        b.IsPos k)
    {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
pred :
  ∀ (w : ℕ)
    (hw :
      ∀ {i k : ι} (hi : b.IsPos i)
        (hk :
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
        (hij :
          LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
            (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
        b.IsPos k)
    {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
⊢ b.IsPos k

Tactic:
induction z generalizing i k with
  | zero => simp_all
  | succ w hw =>
    obtain ⟨l, hl⟩ : P.root i + (w : ℤ) • P.root j ∈ range P.root := by
      replace hk : P.root i + (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
      simp only [natCast_zsmul, root_add_nsmul_mem_range_iff_le_chainTopCoeff hij] at hk ⊢
      lia
    replace hk : P.root k = P.root l + P.root j := by rw [hk, hl]; module
    exact (hw hi hl hij).add (b.isPos_of_mem_support hj) hk
  | pred w hw =>
    obtain ⟨l, hl⟩ : P.root i + (-w : ℤ) • P.root j ∈ range P.root := by
      replace hk : P.root i - (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
      rw [neg_smul, ← sub_eq_add_neg, natCast_zsmul]
      simp only [root_sub_nsmul_mem_range_iff_le_chainBotCoeff hij] at hk ⊢
      lia
    replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module
    exact (hw hi hl hij).sub hj hk

Premises used: RootPairing.root, Submodule.zero, Set.range, DFunLike.coe