awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : Finite ι
inst_6 : P.IsRootSystem
k : Type u_5
inst_7 : Field k
inst_8 : CharZero k
inst_9 : Module k M
inst_10 : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst_11 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := k)
      ((((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i) : N →ₗ[k] k) : (a : N) → k) ((coroot : (a : ι) → N) i : N) :
        k)
      (2 : k)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[k] k) ((coroot : (a : ι) → N) i)) : End k M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule k M) (span k (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j : ι
⊢ Eq (α := N) ((coroot : (a : ι) → N) sorry : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i)) : End k N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)

Tactic:
(coroot_eq_coreflection_of_root_eq_of_span_eq_top p root coroot hp hs hsp ?_)

Premises used: _private.0.RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : Finite ι
inst_6 : P.IsRootSystem
k : Type u_5
inst_7 : Field k
inst_8 : CharZero k
inst_9 : Module k M
inst_10 : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst_11 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := k)
      ((((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i) : N →ₗ[k] k) : (a : N) → k) ((coroot : (a : ι) → N) i : N) :
        k)
      (2 : k)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[k] k) ((coroot : (a : ι) → N) i)) : End k M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule k M) (span k (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j : ι
h :
  Eq (α := M) ((root : (a : ι) → M) sorry : M)
    (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[k] k) ((coroot : (a : ι) → N) i)) : End k M) :
          (a : M) → M)
        ((root : (a : ι) → M) j : M) :
      M)
⊢ Eq (α := N) ((coroot : (a : ι) → N) sorry : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i)) : End k N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)

Tactic:
refine (coroot_eq_coreflection_of_root_eq_of_span_eq_top p root coroot hp hs hsp ?_)

Premises used: _private.0.RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top
-- 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
P : RootPairing ι R M N
inst_7 : P.IsValuedIn S
b : P.Base
i j : ↥b.support
⊢ cartanMatrixIn S b i j = P.pairingIn S (↑i : ι) (↑j : ι)

Tactic:
rfl

Premises used: RootPairing.Base.cartanMatrixIn, RootPairing.pairingIn, Classical.choose, rfl
-- 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
P : RootPairing ι R M N
inst_7 : P.IsValuedIn S
b : P.Base
i j : ↥b.support
⊢ (algebraMap S R : (a : S) → R) (cartanMatrixIn S b i j) = P.pairing (↑i : ι) (↑j : ι)

Tactic:
simp [cartanMatrixIn_def]

Premises used: RootPairing.Base.cartanMatrixIn_def
-- 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
P : RootPairing ι R M N
inst_7 : P.IsValuedIn S
b : P.Base
inst_8 : FaithfulSMul S R
i : ↥b.support
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (cartanMatrixIn S b i i) : R)
    ((algebraMap S R : (a : S) → R) 2 : R)

Tactic:
simp [cartanMatrixIn_def, map_ofNat]

Premises used: RootPairing.Base.cartanMatrixIn_def, map_ofNat
-- 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
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsValuedIn S
B : P.InvariantForm
b : P.Base
inst_9 : DecidableEq ι
a :
  ∀ (i j : ↥b.support),
    HMul.hMul (α := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) (β :=
        Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) ((cartanMatrixIn S b).map (⇑(algebraMap S R) : (a : S) → 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))
        i j =
      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)
        i j
⊢ HMul.hMul (α := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R)
      ((cartanMatrixIn S b).map (⇑(algebraMap S R) : (a : S) → 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)) =
    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)

Tactic:
ext
-- 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
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsValuedIn S
B : P.InvariantForm
b : P.Base
inst_9 : DecidableEq ι
i j : ↥b.support
⊢ HMul.hMul (α := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) (β :=
      Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) ((cartanMatrixIn S b).map (⇑(algebraMap S R) : (a : S) → 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))
      i j =
    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)
      i j

Tactic:
simp [B.two_mul_apply_root_root]

Premises used: RootPairing.InvariantForm.two_mul_apply_root_root
-- 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
⊢ ∃ (B : P.InvariantForm), B.form.Nondegenerate

Tactic:
⟨P.toInvariantForm, P.rootForm_nondegenerate⟩

Premises used: RootPairing.toInvariantForm, Exists.intro, RootPairing.rootForm_nondegenerate
-- 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
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
obtain ⟨B, hB⟩ : ∃ B : P.InvariantForm, B.form.Nondegenerate :=
    ⟨P.toInvariantForm, P.rootForm_nondegenerate⟩

Premises used: RootPairing.InvariantForm
-- 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
B : P.InvariantForm
hB : B.form.Nondegenerate
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)
rwa₁ rwa₂ rwa₃ rwa₄ : 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

Tactic:
rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]

Premises used: Matrix.Nondegenerate.smul_iff, LinearMap.BilinForm.nondegenerate_toMatrix_iff, two_ne_zero
-- 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
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

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]
-- 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
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
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)
⊢ 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:
rw [Matrix.nondegenerate_iff_det_ne_zero, Matrix.det_diagonal, Finset.prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff, Matrix.det_diagonal, Matrix.nondegenerate_iff_det_ne_zero
-- 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
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
⊢ ∀ (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:
aesop
-- 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
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))

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
-- 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
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).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

Premises used: RingHom.mapMatrix_apply, Algebra.algebraMap, ne_eq, Matrix.Nondegenerate.mul_iff_right, RingHom.map_det, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Matrix.nondegenerate_iff_det_ne_zero, FaithfulSMul.algebraMap_eq_zero_iff
-- 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
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))
hB₁ : ¬(cartanMatrixIn S b).det = 0
⊢ 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:
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

Premises used: RingHom.mapMatrix_apply, Algebra.algebraMap, ne_eq, Matrix.Nondegenerate.mul_iff_right, RingHom.map_det, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Matrix.nondegenerate_iff_det_ne_zero, FaithfulSMul.algebraMap_eq_zero_iff
-- 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
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))
rwa rwa₁ rwa₂ rwa₃ : (cartanMatrixIn S b).det ≠ 0
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
rwa [Matrix.nondegenerate_iff_det_ne_zero]

Premises used: Matrix.nondegenerate_iff_det_ne_zero
-- 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
P : RootPairing ι R M N
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
i : ↥b.support
⊢ b.cartanMatrix i i = 2

Tactic:
b.cartanMatrixIn_apply_same ℤ i

Premises used: RootPairing.Base.cartanMatrixIn_apply_same, Int
-- 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
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
rw₄ rw₅ : P.pairing (↑i : ι) (↑j : ι) = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0
⊢ b.cartanMatrix i j = 0 ↔ P.pairing (↑i : ι) (↑j : ι) = 0

Tactic:
rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]

Premises used: RootPairing.Base.cartanMatrixIn_def, Function.Injective.eq_iff, map_zero, RootPairing.algebraMap_pairingIn, Int, RootPairing.Base.cartanMatrix, FaithfulSMul.algebraMap_injective
-- 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
P : RootPairing ι R M N
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ↥b.support
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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
P : RootPairing ι R M N
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ↥b.support
this : Module.IsReflexive R M
⊢ b.cartanMatrix i j = 0 ↔ b.cartanMatrix j i = 0

Tactic:
simp only [cartanMatrix_apply_eq_zero_iff_pairing, P.pairing_eq_zero_iff]

Premises used: RootPairing.pairing_eq_zero_iff, RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing
-- 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
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 : ι)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬i = j
⊢ (↑i : ι) ≠ (↑j : ι)

Tactic:
rwa [ne_eq, ← Subtype.ext_iff]

Premises used: ne_eq, Subtype.ext_iff
-- 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
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
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap