awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
⊢ P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
have have : ∀ (B : P.InvariantForm), P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
Tactic: have B := (P.posRootForm ℤ).toInvariantForm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
have apply : HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
      R) =
  HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
      R)
Tactic: apply mul_right_cancel₀ (B.ne_zero <| threeShortAddTwoLong P)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R)
have calc_1 : HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
        (threeShortAddTwoLongRoot P) :
      R) =
  HMul.hMul (α := R) (β := R) (2 : R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        (threeShortAddTwoLongRoot P) :
      R)
Tactic: calc P.pairing i (threeShortAddTwoLong P) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddTwoLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * (2 * B.form (P.root i) (longRoot P)) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          2 * P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 2 * P.pairing i (long P)) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
calc_1 :
  HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)
⊢ HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R)
have calc_2 : HMul.hMul (α := R) (β := R) (2 : R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        (threeShortAddTwoLongRoot P) :
      R) =
  3 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
    2 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
Tactic: calc P.pairing i (threeShortAddTwoLong P) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddTwoLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * (2 * B.form (P.root i) (longRoot P)) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          2 * P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 2 * P.pairing i (long P)) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
calc_1 :
  HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)
calc_2 :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
⊢ HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R)
have calc_3 : 3 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
    2 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
  HMul.hMul (β := R) (P.pairing i (short P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
    HMul.hMul (β := R) (2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
Tactic: calc P.pairing i (threeShortAddTwoLong P) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddTwoLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * (2 * B.form (P.root i) (longRoot P)) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          2 * P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 2 * P.pairing i (long P)) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)
have calc_1 : HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
        (threeShortAddTwoLongRoot P) :
      R) =
  HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
      R)
Tactic: rw [B.two_mul_apply_root_root]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
have calc_2 : 2 *
      HMul.hMul (α := R) (β := R) (3 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
    2 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
  3 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
    2 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
Tactic: simp only [threeShortAddTwoLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
have calc_3 : 3 *
      HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (short P)) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) (short P) : M) :
          R) +
    2 *
      (P.pairing i (long P) *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)) =
  P.pairing i (short P) *
      HMul.hMul (α := R) (β := R) (3 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
    2 * P.pairing i (long P) *
      HMul.hMul (α := R) (β := R) (3 : R)
        ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)
Tactic: rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, long_eq_three_mul_short]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)
have calc_4 : HMul.hMul (β := R) (P.pairing i (short P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
    HMul.hMul (β := R) (2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
  HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
    ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
Tactic: rw [threeShortAddTwoLongRoot_longRoot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
⊢ a = 0 ∧ b = 0
have ha₁ : a = 0 ∧ a' = 0 ∨
  a = 1 ∧ a' = 1 ∨
    a = -1 ∧ a' = -1 ∨
      a = 1 ∧ a' = 2 ∨
        a = 2 ∧ a' = 1 ∨
          a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
Tactic: simp [S_def] at ha hb hc hd he hf
Cleared hypotheses: ha, hb, hc, hd, he, hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
⊢ a = 0 ∧ b = 0
have hb₁ : b = 0 ∧ b' = 0 ∨
  b = 1 ∧ b' = 1 ∨
    b = -1 ∧ b' = -1 ∨
      b = 1 ∧ b' = 2 ∨
        b = 2 ∧ b' = 1 ∨
          b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
Tactic: simp [S_def] at ha hb hc hd he hf
Cleared hypotheses: ha, hb, hc, hd, he, hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
⊢ a = 0 ∧ b = 0
have hc₁ : c = 0 ∧ c' = 0 ∨
  c = 1 ∧ c' = 1 ∨
    c = -1 ∧ c' = -1 ∨
      c = 1 ∧ c' = 2 ∨
        c = 2 ∧ c' = 1 ∨
          c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
Tactic: simp [S_def] at ha hb hc hd he hf
Cleared hypotheses: ha, hb, hc, hd, he, hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc₁ :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
⊢ a = 0 ∧ b = 0
have hd₁ : d = 0 ∧ d' = 0 ∨
  d = 1 ∧ d' = 1 ∨
    d = -1 ∧ d' = -1 ∨
      d = 1 ∧ d' = 2 ∨
        d = 2 ∧ d' = 1 ∨
          d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
Tactic: simp [S_def] at ha hb hc hd he hf
Cleared hypotheses: ha, hb, hc, hd, he, hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc₁ :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
hd₁ :
  d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
⊢ a = 0 ∧ b = 0
have he₁ : e = 0 ∧ e' = 0 ∨
  e = 1 ∧ e' = 1 ∨
    e = -1 ∧ e' = -1 ∨
      e = 1 ∧ e' = 2 ∨
        e = 2 ∧ e' = 1 ∨
          e = -1 ∧ e' = -2 ∨ e = -2 ∧ e' = -1 ∨ e = 1 ∧ e' = 3 ∨ e = 3 ∧ e' = 1 ∨ e = -1 ∧ e' = -3 ∨ e = -3 ∧ e' = -1
Tactic: simp [S_def] at ha hb hc hd he hf
Cleared hypotheses: ha, hb, hc, hd, he, hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc₁ :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
hd₁ :
  d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
he₁ :
  e = 0 ∧ e' = 0 ∨
    e = 1 ∧ e' = 1 ∨
      e = -1 ∧ e' = -1 ∨
        e = 1 ∧ e' = 2 ∨
          e = 2 ∧ e' = 1 ∨
            e = -1 ∧ e' = -2 ∨ e = -2 ∧ e' = -1 ∨ e = 1 ∧ e' = 3 ∨ e = 3 ∧ e' = 1 ∨ e = -1 ∧ e' = -3 ∨ e = -3 ∧ e' = -1
⊢ a = 0 ∧ b = 0
have hf₁ : f = 0 ∧ f' = 0 ∨
  f = 1 ∧ f' = 1 ∨
    f = -1 ∧ f' = -1 ∨
      f = 1 ∧ f' = 2 ∨
        f = 2 ∧ f' = 1 ∨
          f = -1 ∧ f' = -2 ∨ f = -2 ∧ f' = -1 ∨ f = 1 ∧ f' = 3 ∨ f = 3 ∧ f' = 1 ∨ f = -1 ∧ f' = -3 ∨ f = -3 ∧ f' = -1
Tactic: simp [S_def] at ha hb hc hd he hf
Cleared hypotheses: ha, hb, hc, hd, he, hf