awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
h₁ :
  2 * (x + 1) + -1 * y = -3 ∨
    2 * (x + 1) + -1 * y = -1 ∨ 2 * (x + 1) + -1 * y = 0 ∨ 2 * (x + 1) + -1 * y = 1 ∨ 2 * (x + 1) + -1 * y = 3
h₂ :
  2 * x + -1 * (y - 1) = -3 ∨
    2 * x + -1 * (y - 1) = -1 ∨ 2 * x + -1 * (y - 1) = 0 ∨ 2 * x + -1 * (y - 1) = 1 ∨ 2 * x + -1 * (y - 1) = 3
h₃ :
  2 * (x + 1) + -1 * (y - 1) = -3 ∨
    2 * (x + 1) + -1 * (y - 1) = -1 ∨
      2 * (x + 1) + -1 * (y - 1) = 0 ∨ 2 * (x + 1) + -1 * (y - 1) = 1 ∨ 2 * (x + 1) + -1 * (y - 1) = 3
hA : A = -1
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + 0 * y = -3 ∨ 2 * x + 0 * y = -1 ∨ 2 * x + 0 * y = 0 ∨ 2 * x + 0 * y = 1 ∨ 2 * x + 0 * y = 3
h₁ :
  2 * (x + 1) + 0 * y = -3 ∨
    2 * (x + 1) + 0 * y = -1 ∨ 2 * (x + 1) + 0 * y = 0 ∨ 2 * (x + 1) + 0 * y = 1 ∨ 2 * (x + 1) + 0 * y = 3
h₂ :
  2 * x + 0 * (y - 1) = -3 ∨
    2 * x + 0 * (y - 1) = -1 ∨ 2 * x + 0 * (y - 1) = 0 ∨ 2 * x + 0 * (y - 1) = 1 ∨ 2 * x + 0 * (y - 1) = 3
h₃ :
  2 * (x + 1) + 0 * (y - 1) = -3 ∨
    2 * (x + 1) + 0 * (y - 1) = -1 ∨
      2 * (x + 1) + 0 * (y - 1) = 0 ∨ 2 * (x + 1) + 0 * (y - 1) = 1 ∨ 2 * (x + 1) + 0 * (y - 1) = 3
hA : A = 0
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + 1 * y = -3 ∨ 2 * x + 1 * y = -1 ∨ 2 * x + 1 * y = 0 ∨ 2 * x + 1 * y = 1 ∨ 2 * x + 1 * y = 3
h₁ :
  2 * (x + 1) + 1 * y = -3 ∨
    2 * (x + 1) + 1 * y = -1 ∨ 2 * (x + 1) + 1 * y = 0 ∨ 2 * (x + 1) + 1 * y = 1 ∨ 2 * (x + 1) + 1 * y = 3
h₂ :
  2 * x + 1 * (y - 1) = -3 ∨
    2 * x + 1 * (y - 1) = -1 ∨ 2 * x + 1 * (y - 1) = 0 ∨ 2 * x + 1 * (y - 1) = 1 ∨ 2 * x + 1 * (y - 1) = 3
h₃ :
  2 * (x + 1) + 1 * (y - 1) = -3 ∨
    2 * (x + 1) + 1 * (y - 1) = -1 ∨
      2 * (x + 1) + 1 * (y - 1) = 0 ∨ 2 * (x + 1) + 1 * (y - 1) = 1 ∨ 2 * (x + 1) + 1 * (y - 1) = 3
hA : A = 1
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + 3 * y = -3 ∨ 2 * x + 3 * y = -1 ∨ 2 * x + 3 * y = 0 ∨ 2 * x + 3 * y = 1 ∨ 2 * x + 3 * y = 3
h₁ :
  2 * (x + 1) + 3 * y = -3 ∨
    2 * (x + 1) + 3 * y = -1 ∨ 2 * (x + 1) + 3 * y = 0 ∨ 2 * (x + 1) + 3 * y = 1 ∨ 2 * (x + 1) + 3 * y = 3
h₂ :
  2 * x + 3 * (y - 1) = -3 ∨
    2 * x + 3 * (y - 1) = -1 ∨ 2 * x + 3 * (y - 1) = 0 ∨ 2 * x + 3 * (y - 1) = 1 ∨ 2 * x + 3 * (y - 1) = 3
h₃ :
  2 * (x + 1) + 3 * (y - 1) = -3 ∨
    2 * (x + 1) + 3 * (y - 1) = -1 ∨
      2 * (x + 1) + 3 * (y - 1) = 0 ∨ 2 * (x + 1) + 3 * (y - 1) = 1 ∨ 2 * (x + 1) + 3 * (y - 1) = 3
hA : A = 3
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hki : P.pairingIn ℤ k i = 0
this : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
⊢ P.IsNotG2

Tactic:
have := chainBotCoeff_mul_chainTopCoeff.isNotG2 hi hj hij h₁ h₂ h₃
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
this_2 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
obtain :
  ∀ (n : ι)
    (hn :
      (P.root : (a : ι) → M) n =
        HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
          ((P.root : (a : ι) → M) j : M)),
    (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m + 1) *
        (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) + 1) =
      (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) + 1) *
        (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k + 1)
⊢ (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m + 1) *
      (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) + 1) =
    (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) + 1) *
      (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k + 1)

Tactic:
obtain ⟨n, hn⟩ := h₃
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
hki : P.pairingIn ℤ n i = 0
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-n) : M))
hn :
  (P.root : (a : ι) → M) n =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M)
⊢ False

Tactic:
simp [sub_eq_zero, hij, add_sub_assoc] at hn

Premises used: add_sub_assoc, sub_eq_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M)
⊢ n ≠ k

Tactic:
have hnk_ne : n ≠ k := by rintro rfl; simp [sub_eq_zero, hij, add_sub_assoc] at hn
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M)
hnk_ne : n ≠ k
⊢ k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
have hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j := (IsReduced.linearIndependent_iff _).mp <|
    P.linearIndependent_of_sub_mem_range_root <| h₂ ▸ mem_range_self m
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
⊢ HSub.hSub («α» := 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:
b.sub_notMem_range_root hi hj

Premises used: RootPairing.Base.sub_notMem_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
him_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) m : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
h :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)

Tactic:
convert! b.sub_notMem_range_root hi hj using 2

Premises used: RootPairing.Base.sub_notMem_range_root