-- 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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
intro intro₁ intro₂ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)),
    i = j
intro₃ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f : ι → ℤ)
    (hf :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)),
    i = j
intro₄ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f : ι → ℤ)
    (hf :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
    (g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    i = j
intro₅ intro₆ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f : ι → ℤ)
    (hf :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
    (g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    i = j
intro₇ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f : ι → ℤ)
    (hf :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
    (g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    f' = g'
intro₈ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    ∀ (hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix), f' = g'
intro₉ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f g : ι → ℤ),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    ∀ (hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix)
      (hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix), f' = g'
intro₁₀ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f g : ι → ℤ),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    ∀ (hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix)
      (hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix),
      Injective (β := ↥b.support → ℤ) fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix
intro₁₁ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f g : ι → ℤ),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    ∀ (hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix)
      (hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix),
      LinearIndependent ℤ b.cartanMatrix.row
hA :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f g : ι → ℤ),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    ∀ (hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix)
      (hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix), Matrix.det b.cartanMatrix.row ≠ 0
hA₁ :
  ∀ ⦃i j : ι⦄
    (hij :
      Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
        ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j))
    (f g : ι → ℤ),
    let f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    let g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support);
    ∀ (hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix)
      (hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix),
      Matrix.Nondegenerate b.cartanMatrix.row
⊢ Injective (β := (k : ↥b.support) → ℤ) fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)

Tactic:
classical
  intro i j hij
  obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i
  obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j
  let f' : b.support → ℤ := f ∘ (↑)
  let g' : b.support → ℤ := g ∘ (↑)
  suffices f' = g' by
    rw [← P.root.apply_eq_iff_eq, hf, hg]
    refine Finset.sum_congr rfl fun k hk ↦ ?_
    replace this : f k = g k := congr_fun this ⟨k, hk⟩
    rw [this]
  replace hf : (fun k : b.support ↦ P.pairingIn ℤ i k) = f' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k by
      ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hf]
  replace hg : (fun k : b.support ↦ P.pairingIn ℤ j k) = g' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k by
      ext; simp [g', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hg]
  suffices Injective fun v ↦ v ᵥ* b.cartanMatrix from this <| by simpa [← hf, ← hg]
  rw [Matrix.vecMul_injective_iff]
  apply Matrix.linearIndependent_rows_of_det_ne_zero
  rw [← Matrix.nondegenerate_iff_det_ne_zero]
  exact b.cartanMatrix_nondegenerate

Premises used: RootPairing.Base.cartanMatrix_nondegenerate, Matrix.linearIndependent_rows_of_det_ne_zero, Matrix.vecMul_injective_iff, Matrix.nondegenerate_iff_det_ne_zero