-- 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) : ℚ)
have have₁ have₂ have₃ have₄ :
  ∀ (_i : Fintype ι), Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)
have₅ :
  ∀ (_i : Fintype ι) (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)),
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) j : N) (0 : N) ∨
      Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N) (0 : N)
have₆ :
  ∀ (_i : Fintype ι) (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)),
    i = j
⊢ Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)
have have₇ : ∀ (_i : Fintype ι),
  let _i : Module ℚ M := compHom M (algebraMap ℚ R);
  ∀ (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)
    (huv :
      (P.root : (a : ι) → M) i =
        HSMul.hSMul (β := M) u ((P.root : (a : ι) → M) j : M) + HSMul.hSMul (β := M) v ((P.root : (a : ι) → M) k : M)),
    i = j
Tactic: classical
  have _i : Fintype ι := Fintype.ofFinite _
  let _i : Module ℚ M := Module.compHom M (algebraMap ℚ R)
  let s := baseOf P.root f
  refine fun i hi ↦ ⟨by obtain ⟨hi, -⟩ := hi; aesop, fun j hj k hk contra ↦ ?_⟩
  suffices i = j by grind
  obtain ⟨u, hu, v, hv, huv⟩ : ∃ᵉ (u > (0 : ℚ)) (v > (0 : ℚ)),
      P.root i = u • P.root j + v • P.root k := by
    let l (i : ι) := P.RootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i)
    have hl (i : ι) : 0 < l i := by
      simpa only [l, ← posRootForm_eq] using RootPositiveForm.zero_lt_posForm_apply_root _ _
    refine ⟨l i / l j, by simp [hl], l i / l k, by simp [hl], ?_⟩
    simp only [P.coroot_eq_polarizationEquiv_apply_root, ← map_smul, ← map_add,
      P.PolarizationEquiv.injective.eq_iff] at contra
    let l' (i : ι) := P.RootForm (P.root i) (P.root i)
    have hll' (i : ι) : l i = l' i := P.algebraMap_rootFormIn ℚ _ _
    change (2 / l' i) • P.root i = (2 / l' j) • P.root j + (2 / l' k) • P.root k at contra
    replace contra := congr_arg ((2 / l' i)⁻¹ • ·) contra
    have aux₁ : 2 / l' i ≠ 0 := by simpa using IsAnisotropic.rootForm_root_ne_zero i
    have aux₂ (j : ι) : (2 / l' i)⁻¹ * (2 / l' j) = l i / l j := by ring_nf; simp [hll']
    simp only [smul_add, smul_smul, inv_mul_cancel₀ aux₁, aux₂, one_smul] at contra
    rw [contra]
    module
  have hjk {l : ι} (hl : 0 < g (P.coroot l)) :
      ∃ c : P.root '' s → ℕ, ∑ x, c x • (x : M) = P.root l := by
    rwa [← Submodule.mem_span_iff_of_fintype, ← mem_toAddSubmonoid, span_nat_eq_addSubmonoidClosure,
      AddSubmonoid.closure_image_isAddIndecomposable_baseOf,
      AddSubmonoid.mem_closure_image_pos_iff P.root f _ (P.ne_zero _), hfg]
  obtain ⟨a, ha⟩ : ∃ c : P.root '' s → ℕ, ∑ x, c x • (x : M) = P.root j := hjk hj
  obtain ⟨b, hb⟩ : ∃ d : P.root '' s → ℕ, ∑ x, d x • (x : M) = P.root k := hjk hk
  let ri : P.root '' s := ⟨P.root i, mem_image_of_mem _ hi⟩
  replace huv : u • (Nat.cast ∘ a) + v • (Nat.cast (R := ℚ) ∘ b) = Pi.single ri 1 := by
    simp_rw [← ha, ← hb, Finset.smul_sum, ← Finset.sum_add_distrib, ← Nat.cast_smul_eq_nsmul ℚ,
      smul_smul, ← add_smul] at huv
    have aux : P.root i = ∑ x, Pi.single (M := fun x : P.root '' s ↦ ℚ) ri 1 x • (x : M) := by
      simp [ri]
    rw [eq_comm, aux] at huv
    have hli : LinearIndepOn ℚ id (P.root '' s) := by
      rw [← linearIndepOn_iff_image P.root.injective.injOn]
      exact (linearIndepOn_root_baseOf P f hf).restrict_scalars' ℚ
    rw [← linearIndependent_subtype_iff] at hli
    exact linearIndependent_iff_injective_fintypeLinearCombination.mp hli huv
  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]
  have hij : ¬ LinearIndependent R ![P.root i, P.root j] := by
    simp_rw [LinearIndependent.pair_iff, not_forall]
    exact ⟨q, -1, by simp [Rat.cast_smul_eq_qsmul, hq'], by simp⟩
  rcases IsReduced.eq_or_eq_neg i j hij with hij | hij
  · simpa using hij
  · grind