-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : IsDomain R
inst_8 : NeZero.{u_2} (R := R) 2
inst_9 : FaithfulSMul S R
inst_10 : IsDomain S
P : RootPairing ι R M N
inst_11 : P.IsRootSystem
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
inst_14 : P.IsAnisotropic
b : P.Base
obtain : ∀ (B : P.InvariantForm) (hB : B.form.Nondegenerate), (cartanMatrixIn S b).Nondegenerate
obtain₁ :
  ∀ (B : P.InvariantForm)
    (hB :
      (HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) 2
          ((LinearMap.BilinForm.toMatrix b.toWeightBasis :
                (a : LinearMap.BilinForm R M) → Matrix (↥b.support) (↥b.support) R)
              B.form :
            Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R)).Nondegenerate),
    (cartanMatrixIn S b).Nondegenerate
obtain₂ :
  ∀ (B : P.InvariantForm)
    (hB :
      (HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) 2
          ((LinearMap.BilinForm.toMatrix b.toWeightBasis :
                (a : LinearMap.BilinForm R M) → Matrix (↥b.support) (↥b.support) R)
              B.form :
            Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R)).Nondegenerate)
    (aux :
      Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ↥b.support) (R := R)
        (Matrix.diagonal fun (i : ↥b.support) ↦
          (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑i : ι)) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) (↑i : ι) : M))),
    (cartanMatrixIn S b).Nondegenerate
obtain₃ :
  ∀ (B : P.InvariantForm) (hB : ¬(cartanMatrixIn S b).det = 0)
    (aux :
      Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ↥b.support) (R := R)
        (Matrix.diagonal fun (i : ↥b.support) ↦
          (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑i : ι)) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) (↑i : ι) : M))),
    (cartanMatrixIn S b).Nondegenerate
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
classical
  obtain ⟨B, hB⟩ : ∃ B : P.InvariantForm, B.form.Nondegenerate :=
    ⟨P.toInvariantForm, P.rootForm_nondegenerate⟩
  replace hB : ((2 : R) • B.form.toMatrix b.toWeightBasis).Nondegenerate := by
    rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]
  have aux : (Matrix.diagonal fun i : b.support ↦ B.form (P.root i) (P.root i)).Nondegenerate := by
    rw [Matrix.nondegenerate_iff_det_ne_zero, Matrix.det_diagonal, Finset.prod_ne_zero_iff]
    aesop
  rw [← cartanMatrixIn_mul_diagonal_eq (S := S), Matrix.Nondegenerate.mul_iff_right aux,
    Matrix.nondegenerate_iff_det_ne_zero, ← (algebraMap S R).mapMatrix_apply,
    ← RingHom.map_det, ne_eq, FaithfulSMul.algebraMap_eq_zero_iff] at hB
  rwa [Matrix.nondegenerate_iff_det_ne_zero]

Premises used: RingHom.mapMatrix_apply, Algebra.algebraMap, RootPairing.InvariantForm, ne_eq, RingHom.map_det, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Matrix.nondegenerate_iff_det_ne_zero, FaithfulSMul.algebraMap_eq_zero_iff