awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
this : Module.IsReflexive R M
aux₁ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
aux₂ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
aux₃ : 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
aux₄ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
this : Module.IsReflexive R M
aux₁ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
aux₂ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
aux₃ : 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
aux₄ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≠
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
this : InvolutiveNeg ι := P.indexNeg
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (-j) : M))

Tactic:
simpa [← sub_eq_add_neg] using h

Premises used: sub_eq_add_neg
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
this : InvolutiveNeg ι := P.indexNeg
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (-j) : M))

Tactic:
replace h : P.root i + P.root (-j) ∈ range P.root := by simpa [← sub_eq_add_neg] using h
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (-j) : M))
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = if P.pairingIn ℤ i j = 0 then 1 else 0

Tactic:
simpa using P.chainBotCoeff_if_one_zero h

Premises used: RootPairing.chainBotCoeff_if_one_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : CharZero R
inst_6 : P.IsCrystallographic
inst_7 : P.IsReduced
long short : ι
h : P.pairingIn ℤ long short = 3
⊢ P.pairingIn ℤ ((P.reflectionPerm long : (a : ι) → ι) long) short = -3

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : P.IsIrreducible
⊢ P.pairingIn ℤ (long P) (short P) = -3

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
rw : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (-3) : R) (-3 : R)
⊢ P.pairing (long P) (short P) = -3

Tactic:
rw [← P.algebraMap_pairingIn ℤ, pairingIn_long_short]

Premises used: RootPairing.algebraMap_pairingIn, Int, RootPairing.EmbeddedG2.pairingIn_long_short
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (-3) : R) (-3 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
x : M
hx : x ∈ (↑(allRoots P).toFinset : Set M)
⊢ x = longRoot P ∨
    x = -longRoot P ∨
      x = shortRoot P ∨
        x = -shortRoot P ∨
          x = shortAddLongRoot P ∨
            x = -shortAddLongRoot P ∨
              x = twoShortAddLongRoot P ∨
                x = -twoShortAddLongRoot P ∨
                  x = threeShortAddLongRoot P ∨
                    x = -threeShortAddLongRoot P ∨ x = threeShortAddTwoLongRoot P ∨ x = -threeShortAddTwoLongRoot P

Tactic:
simp only [toFinset_cons, toFinset_nil, insert_empty_eq, Finset.coe_insert,
    Finset.coe_singleton, mem_insert_iff, mem_singleton_iff] at hx

Premises used: Finset.coe_singleton, Set.mem_singleton_iff, LawfulSingleton.insert_empty_eq, List.toFinset_cons, Set.mem_insert_iff, Finset.coe_insert, List.toFinset_nil
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
x : M
hx :
  x = longRoot P ∨
    x = -longRoot P ∨
      x = shortRoot P ∨
        x = -shortRoot P ∨
          x = shortAddLongRoot P ∨
            x = -shortAddLongRoot P ∨
              x = twoShortAddLongRoot P ∨
                x = -twoShortAddLongRoot P ∨
                  x = threeShortAddLongRoot P ∨
                    x = -threeShortAddLongRoot P ∨ x = threeShortAddTwoLongRoot P ∨ x = -threeShortAddTwoLongRoot P
inl : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (longRoot P)
inr : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-longRoot P)
inr₁ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (shortRoot P)
inr₂ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-shortRoot P)
inr₃ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (shortAddLongRoot P)
inr₄ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-shortAddLongRoot P)
inr₅ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (twoShortAddLongRoot P)
inr₆ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-twoShortAddLongRoot P)
inr₇ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (threeShortAddLongRoot P)
inr₈ :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-threeShortAddLongRoot P)
inr₉ :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (threeShortAddTwoLongRoot P)
inr₁₀ :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-threeShortAddTwoLongRoot P)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x

Tactic:
rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (longRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-longRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (shortRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-shortRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (shortAddLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-shortAddLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (twoShortAddLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-twoShortAddLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (threeShortAddLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-threeShortAddLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (threeShortAddTwoLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 : DecidableEq M
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-threeShortAddTwoLongRoot P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (long P) (short P), P.pairingIn ℤ (short P) (long P))

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed (long P) (short P)
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
this :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
    (P.pairingIn ℤ (long P) (short P), P.pairingIn ℤ (short P) (long P))
⊢ P.pairingIn ℤ (short P) (long P) = -1

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
rw : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (-1) : R) (-1 : R)
⊢ P.pairing (short P) (long P) = -1

Tactic:
rw [← P.algebraMap_pairingIn ℤ, pairingIn_short_long]

Premises used: RootPairing.algebraMap_pairingIn, Int, RootPairing.EmbeddedG2.pairingIn_short_long
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (-1) : R) (-1 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ shortAddLongRoot P = shortRoot P + longRoot P

Tactic:
simp [shortAddLongRoot, shortAddLong, reflection_apply_root]

Premises used: RootPairing.EmbeddedG2.shortAddLongRoot, RootPairing.EmbeddedG2.shortAddLong, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
simp :
  HAdd.hAdd (α := M) (-(P.root : (a : ι) → M) (short P) : M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (long P) : M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M))) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) + longRoot P
⊢ twoShortAddLongRoot P = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) + longRoot P

Tactic:
simp [twoShortAddLongRoot, twoShortAddLong, reflection_apply_root]

Premises used: RootPairing.EmbeddedG2.twoShortAddLong, RootPairing.EmbeddedG2.twoShortAddLongRoot, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ HAdd.hAdd (α := M) (-(P.root : (a : ι) → M) (short P) : M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (long P) : M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M))) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) + longRoot P

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
simp :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (long P) : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + longRoot P
⊢ threeShortAddLongRoot P = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + longRoot P

Tactic:
simp [threeShortAddLongRoot, threeShortAddLong, reflection_apply_root]

Premises used: RootPairing.EmbeddedG2.threeShortAddLong, RootPairing.EmbeddedG2.threeShortAddLongRoot, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (long P) : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + longRoot P

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ HAdd.hAdd (α := M) (-(P.root : (a : ι) → M) (long P) : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 3 ((P.root : (a : ι) → M) (long P) : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (longRoot P)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
this : Module.IsReflexive R M
⊢ LinearIndependent R ![shortRoot P, longRoot P]

Tactic:
simp [P.linearIndependent_iff_coxeterWeightIn_ne_four ℤ, coxeterWeightIn]

Premises used: RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four, Int, RootPairing.coxeterWeightIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ allRoots P =
    List.map (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M) allCoeffs

Tactic:
simp [Fintype.linearCombination_apply, neg_add, -neg_add_rev, shortAddLongRoot_eq,
    twoShortAddLongRoot_eq, threeShortAddLongRoot_eq, threeShortAddTwoLongRoot_eq,
    ← Int.cast_smul_eq_zsmul R]

Premises used: neg_add_rev, RootPairing.EmbeddedG2.twoShortAddLongRoot_eq, neg_add, RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_eq, Fintype.linearCombination_apply, Int.cast_smul_eq_zsmul, RootPairing.EmbeddedG2.threeShortAddLongRoot_eq, RootPairing.EmbeddedG2.shortAddLongRoot_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
rw : LinearIndependent ℤ ![shortRoot P, longRoot P]
⊢ Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
    (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)

Tactic:
rw [← linearIndependent_iff_injective_fintypeLinearCombination]

Premises used: linearIndependent_iff_injective_fintypeLinearCombination