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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
h₃ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M)
rw : HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = 0
rw₁ : HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) j : M) = 0
rw₂ rw₃ : Eq.{u_3 + 1} («α» := M) 0 0
⊢ Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (0 : M)

Tactic:
rw [← h₂, h₃, sub_self]

Premises used: sub_self
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
h₃ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (0 : M)

Tactic:
replace h₂ : P.root m = 0 := by rw [← h₂, h₃, sub_self]
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
h₃ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M)
h₂ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (0 : M)
⊢ False

Tactic:
P.ne_zero _ h₂

Premises used: RootPairing.ne_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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
h₃ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M)
h₂ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (0 : M)
⊢ False

Tactic:
exact P.ne_zero _ h₂

Premises used: RootPairing.ne_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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ :
  (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)
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
⊢ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)

Tactic:
have hni : P.root n ≠ P.root i := fun contra ↦ by
    replace h₃ : P.root k = P.root j := by
      rwa [contra, add_comm, add_sub_assoc, left_eq_add, sub_eq_zero] at h₃
    replace h₂ : P.root m = 0 := by rw [← h₂, h₃, sub_self]
    exact P.ne_zero _ 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
h₃ :
  (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)
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul («α» := ℕ) (β := M) 2 ((P.root : (a : ι) → M) n : M) = (P.root : (a : ι) → M) m

Tactic:
replace h₃ : 2 • P.root n = P.root m := by
      rwa [← neg_eq_iff_eq_neg.mpr contra, add_comm, add_sub_assoc, eq_neg_add_iff_add_eq,
        ← two_nsmul, h₂] at 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₃ : HSMul.hSMul («α» := ℕ) (β := M) 2 ((P.root : (a : ι) → M) n : M) = (P.root : (a : ι) → M) m
⊢ False

Tactic:
P.nsmul_notMem_range_root ⟨_, h₃.symm⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root, Eq.symm
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₃ : HSMul.hSMul («α» := ℕ) (β := M) 2 ((P.root : (a : ι) → M) n : M) = (P.root : (a : ι) → M) m
⊢ False

Tactic:
exact P.nsmul_notMem_range_root ⟨_, h₃.symm⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root, Eq.symm
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ :
  (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)
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
⊢ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
have hni' : P.root n ≠ -P.root i := fun contra ↦ by
    replace h₃ : 2 • P.root n = P.root m := by
      rwa [← neg_eq_iff_eq_neg.mpr contra, add_comm, add_sub_assoc, eq_neg_add_iff_add_eq,
        ← two_nsmul, h₂] at h₃
    exact P.nsmul_notMem_range_root ⟨_, h₃.symm⟩
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ :
  (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)
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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)
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (P.pairingIn ℤ l i)

Tactic:
IsG2.pairingIn_mem_zero_one_three P l i hli hli'

Premises used: RootPairing.IsG2.pairingIn_mem_zero_one_three
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ :
  (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)
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
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) + A * y = P.pairingIn ℤ l i
⊢ 2 * (x + 1) + A * y ∈ s

Tactic:
convert! IsG2.pairingIn_mem_zero_one_three P l i hli hli'

Premises used: RootPairing.IsG2.pairingIn_mem_zero_one_three