awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
⊢ (cartanMatrixIn S b).Nondegenerate
have obtain : ∀ (B : P.InvariantForm) (hB : B.form.Nondegenerate), (cartanMatrixIn S b).Nondegenerate
Tactic: obtain ⟨B, hB⟩ : ∃ B : P.InvariantForm, B.form.Nondegenerate :=
    ⟨P.toInvariantForm, P.rootForm_nondegenerate⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
B : P.InvariantForm
hB : B.form.Nondegenerate
⊢ (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
have rwa : Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ↥b.support) (n := ↥b.support) (R := R)
  ((LinearMap.BilinForm.toMatrix b.toWeightBasis : (a : LinearMap.BilinForm R M) → Matrix (↥b.support) (↥b.support) R)
    B.form)
Tactic: rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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
B : P.InvariantForm
hB : B.form.Nondegenerate
⊢ (cartanMatrixIn S b).Nondegenerate
have 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
Tactic: replace hB : ((2 : R) • B.form.toMatrix b.toWeightBasis).Nondegenerate := by
    rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
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
⊢ 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))
have rw : ∀ (a : ↥b.support),
  Membership.mem (γ := Finset ↥b.support) Finset.univ a →
    Ne.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑a : ι)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (↑a : ι) : M) :
        R)
      (0 : R)
Tactic: rw [Matrix.nondegenerate_iff_det_ne_zero, Matrix.det_diagonal, Finset.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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
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
have 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))
Tactic: 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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
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
have hB₁ : ¬(cartanMatrixIn S b).det = 0
Tactic: 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
Cleared hypotheses: hB, aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
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
have rwa : (cartanMatrixIn S b).det ≠ 0
Tactic: rwa [Matrix.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
⊢ (cartanMatrixIn S b).Nondegenerate
have obtain : ∀ (B : P.InvariantForm) (hB : B.form.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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
⊢ (cartanMatrixIn S b).Nondegenerate
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
⊢ (cartanMatrixIn S b).Nondegenerate
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
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
⊢ (cartanMatrixIn S b).Nondegenerate
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
i j : ↥b.support
⊢ b.cartanMatrix i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
have rw : cartanMatrixIn ℤ b i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
Tactic: rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
i j : ↥b.support
rw : cartanMatrixIn ℤ b i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
⊢ b.cartanMatrix i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
have rw₁ : P.pairingIn ℤ (↑i : ι) (↑j : ι) = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
Tactic: rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
i j : ↥b.support
rw : cartanMatrixIn ℤ b i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
rw₁ : P.pairingIn ℤ (↑i : ι) (↑j : ι) = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
⊢ b.cartanMatrix i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
have rw₂ : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) 0 : R) ↔
  P.pairing (↑i : ι) (↑j : ι) = 0
Tactic: rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
i j : ↥b.support
rw : cartanMatrixIn ℤ b i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
rw₁ : P.pairingIn ℤ (↑i : ι) (↑j : ι) = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
rw₂ :
  Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
      ((algebraMap ℤ R : (a : ℤ) → R) 0 : R) ↔
    P.pairing (↑i : ι) (↑j : ι) = 0
⊢ b.cartanMatrix i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
have rw₃ : P.pairing (↑i : ι) (↑j : ι) = (algebraMap ℤ R : (a : ℤ) → R) 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
Tactic: rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
i j : ↥b.support
rw : cartanMatrixIn ℤ b i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
rw₁ : P.pairingIn ℤ (↑i : ι) (↑j : ι) = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
rw₂ :
  Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
      ((algebraMap ℤ R : (a : ℤ) → R) 0 : R) ↔
    P.pairing (↑i : ι) (↑j : ι) = 0
rw₃ : P.pairing (↑i : ι) (↑j : ι) = (algebraMap ℤ R : (a : ℤ) → R) 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
⊢ b.cartanMatrix i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
have rw₄ : P.pairing (↑i : ι) (↑j : ι) = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
Tactic: rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ↥b.support
⊢ b.cartanMatrix i j = 0 ↔ b.cartanMatrix j i = 0
have this : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
i j : ↥b.support
h : i ≠ j
⊢ (↑i : ι) ≠ (↑j : ι)
have rwa : ¬(↑i : ι) = (↑j : ι)
Tactic: rwa [ne_eq, ← Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
i j : ↥b.support
h : i ≠ j
rwa : ¬(↑i : ι) = (↑j : ι)
⊢ (↑i : ι) ≠ (↑j : ι)
have rwa₁ : ¬i = j
Tactic: rwa [ne_eq, ← Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (b.cartanMatrix i j)
have this : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
i j : ↥b.support
hij : i ≠ j
this : Module.IsReflexive R M
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (b.cartanMatrix i j)
have this₁ : Module.IsReflexive R N
Tactic: have : Module.IsReflexive R N := .of_isPerfPair P.flip.toLinearMap