awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Module.IsReflexive R M
⊢ Module.IsReflexive R N

Tactic:
have : Module.IsReflexive R N := .of_isPerfPair P.flip.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
inst_8 : Finite ι
i j : ↥b.support
hij : i ≠ j
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
⊢ Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))

Tactic:
have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
-- 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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
⊢ P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0

Tactic:
have h₂ : P.pairingIn ℤ i j ≤ 0 := b.cartanMatrix_le_zero_of_ne i j hij
-- 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
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
this : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≠ -4
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (P.pairingIn ℤ (↑i : ι) (↑j : ι))

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
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_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
suffices : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≠ -4
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (P.pairingIn ℤ (↑i : ι) (↑j : ι))

Tactic:
suffices P.pairingIn ℤ i j ≠ -4 by 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
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_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
by_contra : ∀ (contra : P.pairingIn ℤ (↑i : ι) (↑j : ι) = -4), False
⊢ P.pairingIn ℤ (↑i : ι) (↑j : ι) ≠ -4

Tactic:
by_contra contra
-- 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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra : P.pairingIn ℤ (↑i : ι) (↑j : ι) = -4
⊢ P.pairingIn ℤ (↑j : ι) (↑i : ι) = -1

Tactic:
simp_all
-- 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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra : P.pairingIn ℤ (↑i : ι) (↑j : ι) = -4
⊢ P.pairingIn ℤ (↑j : ι) (↑i : ι) = -1 ∧ P.pairingIn ℤ (↑i : ι) (↑j : ι) = -4

Tactic:
replace contra : P.pairingIn ℤ j i = -1 ∧ P.pairingIn ℤ i j = -4 := ⟨by simp_all, contra⟩
-- 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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra : P.pairingIn ℤ (↑j : ι) (↑i : ι) = -1 ∧ P.pairingIn ℤ (↑i : ι) (↑j : ι) = -4
⊢ (P.root : (a : ι) → M) (↑i : ι) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) (↑j : ι) : M)

Tactic:
rw [pairingIn_neg_one_neg_four_iff] at contra

Premises used: RootPairing.pairingIn_neg_one_neg_four_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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ False

Tactic:
(not_linearIndependent_iff.mpr ?_) b.linearIndepOn_root

Premises used: Iff.mpr, RootPairing.Base.linearIndepOn_root, not_linearIndependent_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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) (↑j : ι) : M)
refine :
  ∃ (s : Finset (↑(↑b.support : Set ι) : Type u_1)) (g : (↑(↑b.support : Set ι) : Type u_1) → R),
    Eq.{u_3 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul (β := M) (g i) ((P.root : (a : ι) → M) (↑i : ι) : M)) 0 ∧
      ∃ i ∈ s, g i ≠ 0
⊢ False

Tactic:
refine (not_linearIndependent_iff.mpr ?_) b.linearIndepOn_root

Premises used: Iff.mpr, RootPairing.Base.linearIndepOn_root, not_linearIndependent_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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ Multiset.Nodup (α := (↑(↑b.support : Set ι) : Type u_1)) {i, j}

Tactic:
simpa
-- 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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) (↑j : ι) : M)
refine :
  Eq.{u_3 + 1} (α := M)
      (∑ i_1 ∈ { val := {i, j}, nodup := ⋯ : Finset (↑(↑b.support : Set ι) : Type u_1) },
        HSMul.hSMul (β := M)
          (HAdd.hAdd (α := (a : ↥b.support) → R) (β := (a : ↥b.support) → R)
            (⇑(Finsupp.single i 1) : (a : ↥b.support) → R) (⇑(Finsupp.single j 2) : (a : ↥b.support) → R) i_1)
          ((P.root : (a : ι) → M) (↑i_1 : ι) : M))
      0 ∧
    ∃ i_1 ∈ { val := {i, j}, nodup := ⋯ : Finset (↑(↑b.support : Set ι) : Type u_1) },
      HAdd.hAdd (α := (a : ↥b.support) → R) (β := (a : ↥b.support) → R) (⇑(Finsupp.single i 1) : (a : ↥b.support) → R)
          (⇑(Finsupp.single j 2) : (a : ↥b.support) → R) i_1 ≠
        0
⊢ ∃ (s : Finset (↑(↑b.support : Set ι) : Type u_1)) (g : (↑(↑b.support : Set ι) : Type u_1) → R),
    Eq.{u_3 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul (β := M) (g i) ((P.root : (a : ι) → M) (↑i : ι) : M)) 0 ∧
      ∃ i ∈ s, g i ≠ 0

Tactic:
refine ⟨⟨{i, j}, by simpa⟩, Finsupp.single i (1 : R) + Finsupp.single j (2 : R), ?_⟩
-- 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
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (↑i : ι) (↑j : ι), P.pairingIn ℤ (↑j : ι) (↑i : ι))
h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ Eq.{u_3 + 1} (α := M)
      (∑ i_1 ∈ { val := {i, j}, nodup := ⋯ : Finset (↑(↑b.support : Set ι) : Type u_1) },
        HSMul.hSMul (β := M)
          (HAdd.hAdd (α := (a : ↥b.support) → R) (β := (a : ↥b.support) → R)
            (⇑(Finsupp.single i 1) : (a : ↥b.support) → R) (⇑(Finsupp.single j 2) : (a : ↥b.support) → R) i_1)
          ((P.root : (a : ι) → M) (↑i_1 : ι) : M))
      0 ∧
    ∃ i_1 ∈ { val := {i, j}, nodup := ⋯ : Finset (↑(↑b.support : Set ι) : Type u_1) },
      HAdd.hAdd (α := (a : ↥b.support) → R) (β := (a : ↥b.support) → R) (⇑(Finsupp.single i 1) : (a : ↥b.support) → R)
          (⇑(Finsupp.single j 2) : (a : ↥b.support) → R) i_1 ≠
        0

Tactic:
simp [contra, hij, hij.symm]

Premises used: Ne.symm
-- 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
rw :
  cartanMatrixIn ℤ b i j =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
rw₁ :
  P.pairingIn ℤ (↑i : ι) (↑j : ι) =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
rw₂ :
  -P.pairingIn ℤ (↑i : ι) (↑j : ι) =
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
rw₃ rw₄ :
  Eq (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
⊢ b.cartanMatrix i j =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)

Tactic:
rw [cartanMatrix, cartanMatrixIn_def, ← neg_eq_iff_eq_neg, ← b.chainTopCoeff_eq_of_ne hij.symm]

Premises used: RootPairing.Base.cartanMatrixIn_def, neg_eq_iff_eq_neg, Ne.symm, RootPairing.Base.cartanMatrix, RootPairing.Base.chainTopCoeff_eq_of_ne
-- 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
rw :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
          (![(P.root : (a : ι) → M) (↑j : ι), (P.root : (a : ι) → M) (↑i : ι)] : Fin (Nat.succ 0).succ → M) ∨
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ↔
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ b.cartanMatrix i j = 0 ↔
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)

Tactic:
rw [b.cartanMatrix_eq_neg_chainTopCoeff hij, neg_eq_zero, Int.natCast_eq_zero,
    P.chainTopCoeff_eq_zero_iff]

Premises used: neg_eq_zero, RootPairing.chainTopCoeff_eq_zero_iff, Int.natCast_eq_zero, RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff
-- 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
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑j : ι), (P.root : (a : ι) → M) (↑i : ι)] : Fin (Nat.succ 0).succ → M)

Tactic:
replace hij := b.linearIndependent_pair_of_ne hij.symm
-- 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 ι
inst_9 : DecidableEq ι
i j : ↥b.support
inl : |b.cartanMatrix i i| = (if i = i then 4 else 0) - b.cartanMatrix i i
inr : ∀ (h : i ≠ j), |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j
⊢ |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j

Tactic:
rcases eq_or_ne i j with rfl | h

Premises used: eq_or_ne, 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
P : RootPairing ι R M N
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : DecidableEq ι
i : ↥b.support
⊢ |b.cartanMatrix i i| = (if i = i then 4 else 0) - b.cartanMatrix i i

Tactic:
simp
-- 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 ι
inst_9 : DecidableEq ι
i j : ↥b.support
h : i ≠ j
⊢ |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j

Tactic:
simpa [h] using b.cartanMatrix_le_zero_of_ne i j h

Premises used: RootPairing.Base.cartanMatrix_le_zero_of_ne
-- 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 ι
inst_9 : DecidableEq ι
a :
  ∀ (i j : ↥b.support),
    b.cartanMatrix.map abs i j = HSub.hSub (α := Matrix ↥b.support ↥b.support ℤ) 4 b.cartanMatrix i j
⊢ b.cartanMatrix.map abs = 4 - b.cartanMatrix

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
P : RootPairing ι R M N
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : DecidableEq ι
i j : ↥b.support
⊢ b.cartanMatrix.map abs i j = HSub.hSub (α := Matrix ↥b.support ↥b.support ℤ) 4 b.cartanMatrix i j

Tactic:
simp [abs_cartanMatrix_apply, Matrix.ofNat_apply]

Premises used: Matrix.ofNat_apply, RootPairing.Base.abs_cartanMatrix_apply
-- 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
⊢ b.cartanMatrix.Nondegenerate

Tactic:
let _i : Fintype ι := Fintype.ofFinite ι
  cartanMatrixIn_nondegenerate ℤ b

Premises used: Fintype.ofFinite, RootPairing.Base.cartanMatrixIn_nondegenerate, 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
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
let : p j
⊢ p j

Tactic:
let q : Submodule R M := span R (P.root ∘ (↑) '' {i | p i})
-- 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 ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Set M)
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
    ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
simpa
-- 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 ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
⊢ q ≠ ⊥

Tactic:
have hq₀ : q ≠ ⊥ := q.ne_bot_iff.mpr ⟨P.root i, subset_span <| by simpa, P.ne_zero i⟩