-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
have :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
have₁ :
  ∀
    (this :
      Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
        ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
            (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
          h)
        (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
          comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))),
    LinearIndependent (ι := ↥b.support) R h
have₂ :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
have₃ have₄ :
  ∀
    (this :
      Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
        ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
            (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
          h)
        (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
          comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))),
    LinearIndependent (ι := ↥b.support) R h
⊢ LinearIndependent (ι := ↥b.support) R h
have have₅ : ∀
  (this :
    Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
      ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
          (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
        h)
      (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
        comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))),
  LinearIndependent (ι := ↥b.support) R (M := ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
Tactic: classical
  have : Matrix.diagLinearMap (b.support ⊕ ι) R R ∘ h =
      Sum.elimZeroLeft ∘ fun i : b.support ↦ algebraMap ℤ R ∘ (P.pairingIn ℤ · i) := by
    ext; rw [comp_apply, h_def]; aesop
  apply LinearIndependent.of_comp (Matrix.diagLinearMap _ _ _)
  rw [this, LinearMap.linearIndependent_iff_of_injOn _ Sum.elim_injective'.injOn,
    linearIndependent_algebraMap_comp_iff]
  suffices LinearIndependent ℤ (fun i j : b.support ↦ P.pairingIn ℤ j i) from
    this.of_linearIndependent_subset b.support
  apply b.cartanMatrix.transpose.linearIndependent_rows_of_det_ne_zero
  rw [Matrix.det_transpose, ← Matrix.nondegenerate_iff_det_ne_zero]
  exact b.cartanMatrix_nondegenerate