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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (P.pairingIn ℤ k i)

Tactic:
IsG2.pairingIn_mem_zero_one_three P k i hki hki'

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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : 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)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h : 2 * x + A * y = P.pairingIn ℤ k i
⊢ 2 * x + A * y ∈ s

Tactic:
convert! IsG2.pairingIn_mem_zero_one_three P k i hki hki'

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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : 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)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h : 2 * x + A * y = x * 2 + y * P.pairingIn ℤ j i
⊢ 2 * x + A * y = P.pairingIn ℤ k i

Tactic:
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (j := i) h₀.symm, pairingIn_same,
      Int.zsmul_eq_mul, Int.zsmul_eq_mul]

Premises used: RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul, Int.zsmul_eq_mul, Eq.symm, RootPairing.pairingIn_same
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ 2 * x + A * y = x * 2 + y * P.pairingIn ℤ j i

Tactic:
ring
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ 2 * x + A * y ∈ s

Tactic:
replace h₀ : 2 * x + A * y ∈ s := by
    convert! IsG2.pairingIn_mem_zero_one_three P k i hki hki'
    rw [pairingIn_eq_add_of_root_eq_smul_add_smul (j := i) h₀.symm, pairingIn_same,
      Int.zsmul_eq_mul, Int.zsmul_eq_mul]
    ring
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
⊢ A ∈ s

Tactic:
have hA : A ∈ s := IsG2.pairingIn_mem_zero_one_three P j i (P.root.injective.ne_iff.mpr hij.symm)
    (b.root_ne_neg_of_ne hj hi hij.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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
hA : A ∈ s
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)

Tactic:
subst s
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
hA : A ∈ s
h₄ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * (y - 1))

Tactic:
subst s
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
hA : A ∈ s
h₄ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)
h₅ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * (y - 1))
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * (y - 1))

Tactic:
subst s
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
hA : A ∈ s
h₄ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)
h₅ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * (y - 1))
h₆ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * (y - 1))
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * y)

Tactic:
subst s
-- 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 : ℤ
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 ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
hA : A ∈ s
h₄ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)
h₅ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * (y - 1))
h₆ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * (y - 1))
h₇ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * y)
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} A

Tactic:
subst s
-- 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₁ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)
h₂ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * (y - 1))
h₃ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * (y - 1))
h₀ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * y)
hA : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} A
⊢ 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3

Tactic:
simp only [mem_insert_iff, mem_singleton_iff] at h₀ h₁ h₂ h₃ hA

Premises used: Set.mem_singleton_iff, Set.mem_insert_iff
-- 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₁ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * y)
h₂ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * (y - 1))
h₃ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * (x + 1) + A * (y - 1))
h₀ : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (2 * x + A * y)
hA : Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} A
h₄ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
⊢ 2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3

Tactic:
simp only [mem_insert_iff, mem_singleton_iff] at h₀ h₁ h₂ h₃ hA

Premises used: Set.mem_singleton_iff, Set.mem_insert_iff