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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
x : ι
contra :
  (P.root : (a : ι) → M) x =
    -HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (-(↑i : ι)) : M)

Tactic:
simp [contra, two_smul]

Premises used: two_smul
-- 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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
⊢ ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        (P.root : (a : ι) → M) (-(↑i : ι)) =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))

Tactic:
have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
-- 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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
hx :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        (P.root : (a : ι) → M) (-(↑i : ι)) =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
x : ι
⊢ ¬(P.root : (a : ι) → M) (-(↑i : ι)) =
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
simp [P.ne_zero x, eq_comm]

Premises used: RootPairing.ne_zero, eq_comm
-- 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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
hx :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        (P.root : (a : ι) → M) (-(↑i : ι)) =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
⊢ ∀ (x : ι),
    ¬(P.root : (a : ι) → M) (-(↑i : ι)) =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
-- 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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
hx :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        (P.root : (a : ι) → M) (-(↑i : ι)) =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
aux :
  ∀ (x : ι),
    ¬(P.root : (a : ι) → M) (-(↑i : ι)) =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ ∀ (b_1 : ↥b.support),
    Membership.mem (γ := Finset ↥b.support) Finset.univ b_1 →
      b_1 ≠ i →
        HMul.hMul (α := R) (↑|b.cartanMatrix i b_1| : R)
            (Matrix.fromBlocks (l := ↥b.support) (o := ι) 0
              ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
                if i' = i ∧ j = -(↑i : ι) then 1 else 0)
              ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
                if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
              ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
                if
                    (P.root : (a : ι) → M) i' =
                      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                        ((P.root : (a : ι) → M) j : M) then
                  HAdd.hAdd (α := R)
                    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
                else 0)
              (Sum.inl b_1) (Sum.inr l)) =
          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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
hx :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        (P.root : (a : ι) → M) (-(↑i : ι)) =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
aux :
  ∀ (x : ι),
    ¬(P.root : (a : ι) → M) (-(↑i : ι)) =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ -(HMul.hMul (α := R) (↑|b.cartanMatrix i i| : R)
          (Matrix.fromBlocks (l := ↥b.support) (o := ι) 0
            ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
              if i' = i ∧ j = -(↑i : ι) then 1 else 0)
            ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
              if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
            ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
              if
                  (P.root : (a : ι) → M) i' =
                    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                      ((P.root : (a : ι) → M) j : M) then
                HAdd.hAdd (α := R)
                  (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
              else 0)
            (Sum.inl i) (Sum.inr l)) +
        ∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
            0
          else 0) =
    if -(↑i : ι) = l then (↑(P.pairingIn ℤ (-(↑i : ι)) (↑i : ι)) : R) else 0

Tactic:
simp [eq_comm, apply_ite ((-·) : R → R)]

Premises used: apply_ite, eq_comm, Neg.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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ -(↑i : ι)
a : ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
a₁ : ∀ (hkl : k ≠ l), ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
rcases eq_or_ne k l with rfl | hkl

Premises used: eq_or_ne, 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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ -(↑i : ι)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)

Tactic:
lie_e_f_same_aux i k hki hki'

Premises used: _private.0.RootPairing.GeckConstruction.lie_e_f_same_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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ -(↑i : ι)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)

Tactic:
exact lie_e_f_same_aux i k hki hki'

Premises used: _private.0.RootPairing.GeckConstruction.lie_e_f_same_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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ -(↑i : ι)
hkl : k ≠ l
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
simp_all [h, e, f]

Premises used: RootPairing.GeckConstruction.f, RootPairing.GeckConstruction.h, 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 : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
contra : h i = 0
⊢ False

Tactic:
simpa [h] using congr_fun₂ contra (.inr i) (.inr i)

Premises used: RootPairing.GeckConstruction.h, congr_fun₂, Sum.inr, Subtype.val
-- 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 : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
rw rw₁ : h i = h i
⊢ ⁅e i, f i⁆ = h i

Tactic:
rw [lie_e_f_same]

Premises used: RootPairing.GeckConstruction.lie_e_f_same
-- 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 : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
rw : b.cartanMatrix i i • e i = HSMul.hSMul (α := ℕ) 2 (e i)
⊢ ⁅h i, e i⁆ = HSMul.hSMul (α := ℕ) 2 (e i)

Tactic:
rw [lie_h_e]

Premises used: RootPairing.GeckConstruction.lie_h_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 : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
⊢ b.cartanMatrix i i • e i = HSMul.hSMul (α := ℕ) 2 (e i)

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 : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
rw : -b.cartanMatrix i i • f i = -HSMul.hSMul (α := ℕ) 2 (f i)
⊢ ⁅h i, f i⁆ = -HSMul.hSMul (α := ℕ) 2 (f i)

Tactic:
rw [lie_h_f]

Premises used: RootPairing.GeckConstruction.lie_h_f
-- 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 : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
⊢ -b.cartanMatrix i i • f i = -HSMul.hSMul (α := ℕ) 2 (f i)

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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
hl :
  (P.root : (a : ι) → M) (↑j : ι) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M)
⊢ (P.root : (a : ι) → M) (-l) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M)

Tactic:
simp [hl]
-- 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 : ι
this : InvolutiveNeg ι := P.indexNeg
hl :
  (P.root : (a : ι) → M) (↑j : ι) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M)
⊢ False

Tactic:
exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩

Premises used: Exists.intro, RootPairing.Base.sub_notMem_range_root, Neg.neg, 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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ ∀ (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 : ι))

Tactic:
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]⟩
-- 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 : ι
this : InvolutiveNeg ι := 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 : ι))
hl :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑j : ι) : M) ((P.root : (a : ι) → M) l : M)

Tactic:
simpa [neg_eq_iff_eq_neg] using hl

Premises used: neg_eq_iff_eq_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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := 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 : ι))
hl :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑j : ι) : M) ((P.root : (a : ι) → M) l : M)

Tactic:
replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
-- 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 : ι
this : InvolutiveNeg ι := 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 : ι))
hl :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑j : ι) : M) ((P.root : (a : ι) → M) l : M)
⊢ (P.root : (a : ι) → M) (-l) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M)

Tactic:
simp [hl]
-- 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 : ι
this : InvolutiveNeg ι := 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 : ι))
hl :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑j : ι) : M) ((P.root : (a : ι) → M) l : M)
⊢ False

Tactic:
exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩

Premises used: Exists.intro, RootPairing.Base.sub_notMem_range_root, Neg.neg, 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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := 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 : ι))
⊢ ∀ (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 : ι))

Tactic:
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]⟩
-- 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 : ι
this : InvolutiveNeg ι := 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

Tactic:
simp [e, f, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux₁, Finset.sum_ite_of_false aux₂]

Premises used: RootPairing.GeckConstruction.f, Finset.sum_ite_of_false, ite_and, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e