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 : 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))
aux₁ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
aux₂ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i ≤
    2
⊢ 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i
have rwa : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (α := ℕ) (β := M) 1 ((P.root : (a : ι) → M) j : M)))
Tactic: rwa [← root_add_nsmul_mem_range_iff_le_chainTopCoeff aux₁, one_smul]
-- 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 : 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))
aux₁ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
aux₂ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i ≤
    2
⊢ P.pairingIn ℤ i j ≤ 0
have aux₃ : 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i
Tactic: have aux₃ : 1 ≤ P.chainTopCoeff j i := by
    rwa [← root_add_nsmul_mem_range_iff_le_chainTopCoeff aux₁, one_smul]
-- 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 : 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))
aux₁ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
aux₂ :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i ≤
    2
aux₃ : 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i
⊢ P.pairingIn ℤ i j ≤ 0
have rw : HSub.hSub (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i) : ℤ)
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i) : ℤ) ≤
  0
Tactic: rw [← P.chainBotCoeff_sub_chainTopCoeff aux₁]
-- 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 : 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))
⊢ 0 ≤ P.pairingIn ℤ i j
have 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) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M))
Tactic: replace h : P.root i + P.root (P.reflectionPerm j j) ∈ range P.root := by simpa [← sub_eq_add_neg]
Cleared hypotheses: h
-- 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 : 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))
⊢ chainBotCoeff.{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
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 (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 : 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
⊢ chainBotCoeff.{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
have 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)
Tactic: have aux₁ := P.linearIndependent_of_add_mem_range_root' h
-- 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 : 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)
⊢ chainBotCoeff.{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
have 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
Tactic: have aux₂ := P.chainBotCoeff_add_chainTopCoeff_le_two i j
-- 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 : 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
⊢ chainBotCoeff.{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
have aux₃ : 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
Tactic: have aux₃ : 1 ≤ P.chainTopCoeff i j := P.one_le_chainTopCoeff_of_root_add_mem h
-- 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 : 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
⊢ chainBotCoeff.{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
have inl : ∀
  (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 = if P.pairingIn ℤ i j = 0 then 1 else 0
Tactic: rcases eq_or_ne (P.chainBotCoeff i j) (P.chainTopCoeff i j) with aux₄ | aux₄
-- 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 : 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
inl :
  ∀
    (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 = if P.pairingIn ℤ i j = 0 then 1 else 0
⊢ chainBotCoeff.{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
have inr : ∀
  (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 = if P.pairingIn ℤ i j = 0 then 1 else 0
Tactic: rcases eq_or_ne (P.chainBotCoeff i j) (P.chainTopCoeff i j) with aux₄ | aux₄
-- 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 : 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 = if P.pairingIn ℤ i j = 0 then 1 else 0
have inl : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 1
Tactic: simp_rw [P.pairingIn_eq_zero_iff (i := i) (j := j), ← P.chainBotCoeff_sub_chainTopCoeff aux₁,
    sub_eq_zero, Nat.cast_inj, aux₄, reduceIte]
-- 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 : 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 = if P.pairingIn ℤ i j = 0 then 1 else 0
have inr : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0
Tactic: simp_rw [P.pairingIn_eq_zero_iff (i := i) (j := j), ← P.chainBotCoeff_sub_chainTopCoeff aux₁,
    sub_eq_zero, Nat.cast_inj, aux₄, reduceIte]
-- 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 : 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
⊢ 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
have 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))
Tactic: replace h : P.root i + P.root (-j) ∈ range P.root := by simpa [← sub_eq_add_neg] using h
Cleared hypotheses: h
-- 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
⊢ P.pairing (long P) (short P) = -3
have rw : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (-3) : R) (-3 : R)
Tactic: rw [← P.algebraMap_pairingIn ℤ, pairingIn_long_short]
-- 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 : DecidableEq M
x : M
hx : x ∈ (↑(allRoots P).toFinset : Set M)
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have 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
Tactic: simp only [toFinset_cons, toFinset_nil, insert_empty_eq, Finset.coe_insert,
    Finset.coe_singleton, mem_insert_iff, mem_singleton_iff] 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 : 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
⊢ Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have inl : Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (longRoot 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)
⊢ 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)) (-longRoot 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)
⊢ 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)) (shortRoot 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)
⊢ 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)) (-shortRoot 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)
⊢ 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