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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₄ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-shortAddLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- 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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₅ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (twoShortAddLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- 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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₆ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-twoShortAddLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- 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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₇ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (threeShortAddLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- 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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₈ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-threeShortAddLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- 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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₉ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (threeShortAddTwoLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- 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 : 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)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inr₁₀ : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-threeShortAddTwoLongRoot P)
Tactic: rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
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
⊢ P.pairingIn ℤ (short P) (long P) = -1
have 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))
Tactic: have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed (long P) (short 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
⊢ P.pairing (short P) (long P) = -1
have rw : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (-1) : R) (-1 : R)
Tactic: rw [← P.algebraMap_pairingIn ℤ, pairingIn_short_long]
-- 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
⊢ twoShortAddLongRoot P = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) + longRoot P
have 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
Tactic: simp [twoShortAddLongRoot, twoShortAddLong, reflection_apply_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
⊢ threeShortAddLongRoot P = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + longRoot P
have 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
Tactic: simp [threeShortAddLongRoot, threeShortAddLong, reflection_apply_root]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
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
⊢ LinearIndependent R ![shortRoot P, longRoot P]
have this : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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
⊢ Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
    (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)
have rw : LinearIndependent ℤ ![shortRoot P, longRoot P]
Tactic: rw [← linearIndependent_iff_injective_fintypeLinearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
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).Nodup
have hli : Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
  (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)
Tactic: have hli : Injective (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) := by
    rw [← linearIndependent_iff_injective_fintypeLinearCombination]
    exact (linearIndependent_short_long P).restrict_scalars' ℤ
-- 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
hli :
  Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
    (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)
⊢ (allRoots P).Nodup
have rw : allCoeffs.Nodup
Tactic: rw [allRoots_eq_map_allCoeffs, nodup_map_iff hli]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
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
x : M
hx : x ∈ allRoots P
⊢ Membership.mem (γ := Submodule ℤ M) (Submodule.span ℤ {longRoot P, shortRoot P}) x
have this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
Tactic: have : {longRoot P, shortRoot P} = range ![shortRoot P, longRoot P] := by simp
-- 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
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ Membership.mem (γ := Submodule ℤ M) (Submodule.span ℤ {longRoot P, shortRoot P}) x
have simp_rw : ∃ (c : Fin (Nat.succ 0).succ → ℤ),
  (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin (Nat.succ 0).succ → ℤ) → M) c = x
Tactic: simp_rw [this, Submodule.mem_span_range_iff_exists_fun, ← Fintype.linearCombination_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
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
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ ∃ (c : Fin (Nat.succ 0).succ → ℤ),
    (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin (Nat.succ 0).succ → ℤ) → M) c = x
have hx₁ : x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![0, 1] ∨
  x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![0, -1] ∨
    x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![1, 0] ∨
      x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-1, 0] ∨
        x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![1, 1] ∨
          x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-1, -1] ∨
            x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![2, 1] ∨
              x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-2, -1] ∨
                x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![3, 1] ∨
                  x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-3, -1] ∨
                    x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![3, 2] ∨
                      x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-3, -2]
Tactic: simp [allRoots_eq_map_allCoeffs] at hx
Cleared hypotheses: hx
-- 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 : ι
⊢ P.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
have rw : P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
Tactic: rw [pairingIn_eq_add_of_root_eq_add (shortAddLongRoot_eq 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 : ι
⊢ P.pairingIn ℤ i (shortAddLong P) = P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)
have suffices : P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
Tactic: suffices P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P) from
    algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
-- 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 : ι
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
have have : ∀ (this : Fintype ι), P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
Tactic: have : Fintype ι := Fintype.ofFinite ι