-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
⊢ i = j
have obtain : ∀ (q : ℚ) (hq : q > 0) (hq' : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) q ((P.root : (a : ι) → M) i : M)), i = j
Tactic: obtain ⟨q, hq, hq'⟩ : ∃ q > (0 : ℚ), P.root j = q • P.root i := by
    suffices P.root j = (a ri : ℚ) • P.root i by
      refine ⟨a ri, ?_, this⟩
      by_contra contra
      replace contra : a ri = 0 := by simpa using contra
      simp [contra, P.ne_zero j] at this
    have (x : P.root '' s) (hx : x ≠ ri) : a x = 0 := by
      replace huv : u * ↑(a x) + v * ↑(b x) = 0 := by simpa [hx] using congr($huv x)
      suffices u * (a x) = 0 by simpa [hu.ne'] using this
      have : 0 ≤ u * (a x) := by positivity
      have : 0 ≤ v * (b x) := by positivity
      grind
    replace this (x : P.root '' s) (hx : a x • (x : M) ≠ 0) :  x ∈ ({ri} : Finset _) := by
      rw [Finset.mem_singleton]
      by_contra! contra
      simp [this x contra] at hx
    simp [← ha, ← Fintype.sum_subset this, ri, Nat.cast_smul_eq_nsmul]