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
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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
⊢ B.rootLength j < B.rootLength k

Tactic:
have ⟨aux₃, aux₄⟩ : B.rootLength i = B.rootLength j ∧ B.rootLength j < B.rootLength k := by
    have hij_le : B.rootLength i ≤ B.rootLength j := B.rootLength_le_of_pairingIn_eq <| Or.inl aux₁
    have hjk_lt : B.rootLength j < B.rootLength k :=
      B.rootLength_lt_of_pairingIn_notMem (by grind) hkj_ne.2 <| by grind
    refine ⟨?_, hjk_lt⟩
    simpa [posForm, rootLength] using (B.toInvariantForm.apply_eq_or_of_apply_ne (i := j) (j := k)
      (by simpa [posForm, rootLength] using hjk_lt.ne) i).resolve_right
      (by simpa [posForm, rootLength] using (lt_of_le_of_lt hij_le hjk_lt).ne)
-- 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this_4 : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
this : P.pairingIn ℤ j i = -1
⊢ P.pairingIn ℤ k i = -1

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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
suffices : P.pairingIn ℤ j i = -1
⊢ P.pairingIn ℤ k i = -1

Tactic:
suffices P.pairingIn ℤ j i = -1 by 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
⊢ Eq.{u_2 + 1} («α» := R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)

Tactic:
simpa [posForm, rootLength] using aux₃

Premises used: RootPairing.RootPositiveForm.rootLength, RootPairing.RootPositiveForm.posForm
-- 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
⊢ Eq.{u_2 + 1} («α» := R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)

Tactic:
have aux : B.toInvariantForm.form (P.root i) (P.root i) =
        B.toInvariantForm.form (P.root j) (P.root j) := by simpa [posForm, rootLength] using aux₃
-- 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
aux :
  Eq.{u_2 + 1} («α» := R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_length_eq_of_ne aux hij (b.root_ne_neg_of_ne hi hj hij)
-- 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this_4 : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
aux :
  Eq.{u_2 + 1} («α» := R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.toInvariantForm.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
this : Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ P.pairingIn ℤ j i = -1

Tactic:
grind
-- 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
⊢ P.pairingIn ℤ k i = -1

Tactic:
have aux₅ : P.pairingIn ℤ k i = -1 := by
    suffices P.pairingIn ℤ j i = -1 by lia
    have aux : B.toInvariantForm.form (P.root i) (P.root i) =
        B.toInvariantForm.form (P.root j) (P.root j) := by simpa [posForm, rootLength] using aux₃
    have := P.pairingIn_pairingIn_mem_set_of_length_eq_of_ne aux hij (b.root_ne_neg_of_ne hi hj hij)
    grind
-- 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
hkj' : 0 < P.pairingIn ℤ k 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))
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 : InvolutiveNeg ι := P.indexNeg
this_3 : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hlj_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M))
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
aux₅ : P.pairingIn ℤ k i = -1
⊢ B.rootLength k ≤ B.rootLength i

Tactic:
have aux₆ : B.rootLength k ≤ B.rootLength i := B.rootLength_le_of_pairingIn_eq <| Or.inl aux₅