awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (P.pairingIn ℤ (↑i : ι) (↑j : ι))
have 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 : ι))
Tactic: have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
-- 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_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 : ι))
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (P.pairingIn ℤ (↑i : ι) (↑j : ι))
have h₂ : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≤ 0
Tactic: have h₂ : P.pairingIn ℤ i j ≤ 0 := b.cartanMatrix_le_zero_of_ne i j hij
-- 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
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
⊢ Membership.mem (γ := Set ℤ) {-3, -2, -1, 0} (P.pairingIn ℤ (↑i : ι) (↑j : ι))
have suffices : P.pairingIn ℤ (↑i : ι) (↑j : ι) ≠ -4
Tactic: suffices P.pairingIn ℤ i j ≠ -4 by 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
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
⊢ False
have contra₁ : 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⟩
Cleared hypotheses: contra
-- 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_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
⊢ False
have contra₁ : (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
Cleared hypotheses: contra
-- 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
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
have 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
Tactic: refine (not_linearIndependent_iff.mpr ?_) b.linearIndepOn_root
-- 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
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)
⊢ ∃ (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
have refine : Eq.{u_3 + 1} (α := M)
    (∑ i_1 ∈ { val := {i, j}, nodup := sorry : 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 := sorry : 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: refine ⟨⟨{i, j}, by simpa⟩, Finsupp.single i (1 : R) + Finsupp.single j (2 : R), ?_⟩
-- 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
hij : i ≠ j
⊢ b.cartanMatrix i j =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
have rw : cartanMatrixIn ℤ b 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]
-- 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
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 : ι)) : ℤ)
⊢ b.cartanMatrix i j =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
have rw₁ : P.pairingIn ℤ (↑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]
-- 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
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 : ι)) : ℤ)
⊢ b.cartanMatrix i j =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
have rw₂ : -P.pairingIn ℤ (↑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]
-- 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
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 : ι)) : ℤ)
⊢ b.cartanMatrix i j =
    -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) (↑i : ι)) : ℤ)
have 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 : ι)) : ℤ)
Tactic: rw [cartanMatrix, cartanMatrixIn_def, ← neg_eq_iff_eq_neg, ← b.chainTopCoeff_eq_of_ne hij.symm]
-- 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
hij : i ≠ j
⊢ 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)
have 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)
Tactic: rw [b.cartanMatrix_eq_neg_chainTopCoeff hij, neg_eq_zero, Int.natCast_eq_zero,
    P.chainTopCoeff_eq_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
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) ∨
      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)
have hij₁ : 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
Cleared hypotheses: hij
-- 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
hij :
  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)
⊢ ¬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)
have mp : ¬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)
Tactic: tauto
-- 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
hij :
  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)
mp :
  ¬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)
⊢ ¬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)
have mpr : 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) →
  ¬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)
Tactic: tauto
-- 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
hij :
  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)
mp :
  ¬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)
mpr :
  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) →
    ¬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)
⊢ ¬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)
have mp₁ : ¬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)
Tactic: tauto
-- 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
hij :
  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)
mp :
  ¬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)
mpr :
  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) →
    ¬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)
mp₁ :
  ¬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)
⊢ ¬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)
have mp₂ : 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)
Tactic: tauto
-- 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 ι
inst_9 : DecidableEq ι
i j : ↥b.support
⊢ |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j
have inl : |b.cartanMatrix i i| = (if i = i then 4 else 0) - b.cartanMatrix i i
Tactic: rcases eq_or_ne i j with rfl | h
Cleared hypotheses: j