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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
h₂ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) a : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0 ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0

Tactic:
exact ⟨P.chainBotCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₁ x <| by simp [hx],
           P.chainTopCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₂ x <| by simp [hx]⟩
-- 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 : InvolutiveNeg ι := P.indexNeg
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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 : Module.IsReflexive R M
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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
a : ∀ (k l : ↥b.support), ⁅e i, f i⁆ (Sum.inl k) (Sum.inl l) = h i (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f i⁆ (Sum.inr k) (Sum.inl l) = h i (Sum.inr k) (Sum.inl l)
a₃ : ∀ (k l : ι), ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
⊢ ⁅e i, f i⁆ = h i

Tactic:
ext (k | k) (l | l)
-- 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 : ↥b.support
⊢ ⁅e i, f i⁆ (Sum.inl k) (Sum.inl l) = h i (Sum.inl k) (Sum.inl l)

Tactic:
simp [e, f, h]

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
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l x : ι
simp :
  (P.root : (a : ι) → M) x =
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) →
    k = i → ¬x = -(↑i : ι)
⊢ ¬((P.root : (a : ι) → M) x =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
      k = i ∧ x = -(↑i : ι))

Tactic:
simp only [not_and]

Premises used: not_and
-- 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 ι
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
contra :
  (P.root : (a : ι) → M) (-(↑k : ι)) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑k : ι) : M)
⊢ False

Tactic:
simp [P.ne_zero, sub_eq_add_neg] at contra

Premises used: RootPairing.ne_zero, sub_eq_add_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 : ↥b.support
l : ι
⊢ ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        k = i ∧ x = -(↑i : ι))

Tactic:
have h₁ (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra
-- 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 : ↥b.support
l : ι
h₁ :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        k = i ∧ x = -(↑i : ι))
x : ι
simp :
  (P.root : (a : ι) → M) x =
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) →
    k = i → ¬x = (↑i : ι)
⊢ ¬((P.root : (a : ι) → M) x =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
      k = i ∧ x = (↑i : ι))

Tactic:
simp only [not_and]

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

Tactic:
simp [P.ne_zero] at contra

Premises used: RootPairing.ne_zero
-- 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 : ↥b.support
l : ι
h₁ :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        k = i ∧ x = -(↑i : ι))
⊢ ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        k = i ∧ x = (↑i : ι))

Tactic:
have h₂ (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ k = i ∧ x = i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra
-- 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 : ↥b.support
l : ι
h₁ :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
        k = i ∧ x = -(↑i : ι))
h₂ :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        k = i ∧ x = (↑i : ι))
⊢ ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)

Tactic:
simp [e, f, h, h₁, h₂, -indexNeg_neg, ← ite_and]

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

Tactic:
simp [e, f, h]

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
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
a : ⁅e i, f i⁆ (Sum.inr (↑i : ι)) (Sum.inr l) = h i (Sum.inr (↑i : ι)) (Sum.inr l)
a₁ : ∀ (hki : k ≠ (↑i : ι)), ⁅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 i with rfl | hki

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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
l x : ι
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ False

Tactic:
P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root
-- 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 x : ι
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
refine : (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ False

Tactic:
refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root
-- 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 x : ι
contra :
  (P.root : (a : ι) → M) (↑i : ι) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
rwa :
  ∀
    (contra :
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑i : ι) : M) =
        (P.root : (a : ι) → M) x),
    (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)
rwa₁ :
  ∀ (contra : HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M) = (P.root : (a : ι) → M) x),
    (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (contra : (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)),
    (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra

Premises used: eq_sub_iff_add_eq, two_smul, eq_comm, Nat
-- 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 : ι
⊢ ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        (P.root : (a : ι) → M) (↑i : ι) =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M))

Tactic:
have hx (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
-- 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 : ι
hx :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        (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 →
        (if True then
            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' =
                        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M)
                          ((P.root : (a : ι) → M) (↑i : ι) : M) then
                    HAdd.hAdd (α := R)
                      (↑(chainTopCoeff.{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))
          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 : ↥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 : ι)
a : ∀ (hki : -(↑i : ι) ≠ (↑i : ι)), ⁅e i, f i⁆ (Sum.inr (-(↑i : ι))) (Sum.inr l) = h i (Sum.inr (-(↑i : ι))) (Sum.inr l)
a₁ : ∀ (hki' : k ≠ -(↑i : ι)), ⁅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 (-i) with rfl | hki'

Premises used: eq_or_ne, Subtype.val, Neg.neg, 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
l : ι
hki : -(↑i : ι) ≠ (↑i : ι)
x : ι
contra :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
⊢ False

Tactic:
P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root
-- 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) (-(↑i : ι)) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
refine : (P.root : (a : ι) → M) x = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (-(↑i : ι)) : M)
⊢ False

Tactic:
refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root
-- 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) (-(↑i : ι)) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
⊢ (P.root : (a : ι) → M) x =
    -HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra

Premises used: add_eq_zero_iff_eq_neg', neg_eq_iff_add_eq_zero, add_assoc
-- 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) (-(↑i : ι)) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
⊢ (P.root : (a : ι) → M) x =
    -HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
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