Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
⊢ baseOf (⇑P.root) f ⊆ baseOf (⇑P.coroot) g

Tactic:
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

Goal state after: