awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
letI letI₁ letI₂ : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
letI₃ :
  ∀
    (aux₁ :
      ∀ (x : ι),
        Membership.mem (γ := Finset ι) Finset.univ x →
          ¬((P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
              k = j ∧ x = (↑j : ι))),
    ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
letI₄ :
  let this := P.indexNeg;
  ∀
    (aux₁ :
      ∀ (x : ι),
        Membership.mem (γ := Finset ι) Finset.univ x →
          ¬((P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
              k = j ∧ x = (↑j : ι)))
    (aux₂ :
      ∀ (x : ι),
        Membership.mem (γ := Finset ι) Finset.univ x →
          ¬((P.root : (a : ι) → M) x =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              k = i ∧ x = -(↑i : ι))),
    ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0

Tactic:
classical
  letI := P.indexNeg
  have aux₁ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root i + P.root l ∧ k = j ∧ x = j) := by
    rintro x - ⟨hl, -, rfl⟩
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  have aux₂ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root l - P.root j ∧ k = i ∧ x = -i) := by
    rintro x - ⟨hl, -, rfl⟩
    replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  simp [e, f, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux₁, Finset.sum_ite_of_false aux₂]

Premises used: RootPairing.GeckConstruction.f, ite_and, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
⊢ (↑i : ι) ≠ (↑j : ι)

Tactic:
have hij' : (i : ι) ≠ (j : ι) := hij ∘ SetLike.coe_eq_coe.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)
h₁ : ∀ (k : ι), ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) = 0

Tactic:
ext (k | k)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (↑j : ι)) = 0 (Sum.inl k)
h₁ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inl k))
h₂ h₃ : Eq.{u_2 + 1} (α := R) 0 0
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)

Tactic:
rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]

Premises used: Pi.zero_apply, _private.0.RootPairing.GeckConstruction.lie_e_f_ne_aux₀, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this_1 : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
⊢ (↑j : ι) ≠ -(↑i : ι)

Tactic:
simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm

Premises used: Ne.symm, RootPairing.Base.root_ne_neg_of_ne, Subtype.property
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this_1 : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
⊢ (↑j : ι) ≠ -(↑i : ι)

Tactic:
have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij_1 : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this_1 : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
hij : (↑j : ι) ≠ -(↑i : ι)
⊢ ∀ (x : ↥b.support),
    Membership.mem (γ := Finset ↥b.support) Finset.univ x →
      x ≠ j → Eq.{u_2 + 1} (α := R) (if x = j ∧ k = (↑i : ι) then (↑|b.cartanMatrix i x| : R) else 0) 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij_1 : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this_1 : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
hij : (↑j : ι) ≠ -(↑i : ι)
⊢ ∀ (x : ↥b.support),
    Membership.mem (γ := Finset ↥b.support) Finset.univ x →
      x ≠ j → Eq.{u_2 + 1} (α := R) (if x = j ∧ k = (↑i : ι) then (↑|b.cartanMatrix i x| : R) else 0) 0

Tactic:
have aux : ∀ x ∈ Finset.univ,
        x ≠ j → (if x = j ∧ k = i then ↑|b.cartanMatrix i x| else 0) = (0 : R) := by aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij_1 : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this_1 : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
hij : (↑j : ι) ≠ -(↑i : ι)
aux :
  ∀ (x : ↥b.support),
    Membership.mem (γ := Finset ↥b.support) Finset.univ x →
      x ≠ j → Eq.{u_2 + 1} (α := R) (if x = j ∧ k = (↑i : ι) then (↑|b.cartanMatrix i x| : R) else 0) 0
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
simpa [e, f, P.ne_zero, hij, -indexNeg_neg, -Finset.univ_eq_attach, ← ite_and,
        Finset.sum_eq_single_of_mem j (Finset.mem_univ _) aux]

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem, RootPairing.GeckConstruction.f, RootPairing.ne_zero, Finset.univ_eq_attach, ite_and, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
h :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
suffices ((if k = i then ↑|b.cartanMatrix i j| else (0 : R)) -
        ∑ x, if P.root x = P.root i + P.root j ∧ P.root k = P.root x - P.root j then
          (P.chainTopCoeff j x : R) + 1 else 0) = 0 by
      have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm
      have aux : ∀ x ∈ Finset.univ,
        x ≠ j → (if x = j ∧ k = i then ↑|b.cartanMatrix i x| else 0) = (0 : R) := by aesop
      simpa [e, f, P.ne_zero, hij, -indexNeg_neg, -Finset.univ_eq_attach, ← ite_and,
        Finset.sum_eq_single_of_mem j (Finset.mem_univ _) aux]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
h :
  HSub.hSub (α := R) (if (↑i : ι) = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) (↑i : ι) =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
h₁ :
  ∀ (hk : k ≠ (↑i : ι)),
    HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        (∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                    ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
                (P.root : (a : ι) → M) k =
                  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R) 1
          else 0) =
      0
⊢ HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0

Tactic:
rcases eq_or_ne k i with rfl | hk

Premises used: eq_or_ne, Subtype.val, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
hk : k ≠ (↑i : ι)
⊢ ¬k = (↑i : ι)

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
hk : k ≠ (↑i : ι)
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬((P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
          (P.root : (a : ι) → M) k =
            HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M))

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
hk : k ≠ (↑i : ι)
h : HSub.hSub (α := R) 0 (∑ x : ι, 0) = 0
⊢ HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0

Tactic:
rw [if_neg (by tauto), Finset.sum_ite_of_false (by aesop)]

Premises used: Finset.sum_ite_of_false, if_neg
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
hk : k ≠ (↑i : ι)
⊢ HSub.hSub (α := R) 0 (∑ x : ι, 0) = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
pos :
  ∀
    (hij_mem :
      Membership.mem (γ := Set 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))),
    HSub.hSub (α := R) (if (↑i : ι) = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        (∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                    ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
                (P.root : (a : ι) → M) (↑i : ι) =
                  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R) 1
          else 0) =
      0
neg :
  ∀
    (hij_mem :
      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)),
    HSub.hSub (α := R) (if (↑i : ι) = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        (∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                    ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
                (P.root : (a : ι) → M) (↑i : ι) =
                  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R) 1
          else 0) =
      0
⊢ HSub.hSub (α := R) (if (↑i : ι) = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) (↑i : ι) =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0

Tactic:
by_cases hij_mem : P.root i + P.root j ∈ range P.root

Premises used: RootPairing.root, Set.range, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
hij_mem :
  Membership.mem (γ := Set 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))
pos :
  ∀ (m : ι)
    (hm :
      (P.root : (a : ι) → M) m =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M)),
    HSub.hSub (α := R) (if (↑i : ι) = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        (∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                    ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
                (P.root : (a : ι) → M) (↑i : ι) =
                  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R) 1
          else 0) =
      0
⊢ HSub.hSub (α := R) (if (↑i : ι) = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) (↑i : ι) =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0

Tactic:
obtain ⟨m, hm⟩ := hij_mem