awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
⊢ B.rootLength j < B.rootLength i
have hij' : P.pairingIn ℤ i j = -3 ∨
  P.pairingIn ℤ i j = -2 ∨
    P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
Tactic: have hij' : P.pairingIn ℤ i j = -3 ∨ P.pairingIn ℤ i j = -2 ∨ P.pairingIn ℤ i j = 2 ∨
      P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4 := by
    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
    aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
⊢ P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
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.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
this : Module.IsReflexive R M
⊢ P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 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), (4, 1), (1, 4),
    (-4, -1), (-1, -4), (2, 2), (-2, -2)}
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
Tactic: have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i
have aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
Tactic: have aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1 := by
    have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
    aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
⊢ B.rootLength j < B.rootLength i
have aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
Tactic: have aux₂ := B.pairingIn_mul_eq_pairingIn_mul_swap i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
⊢ B.rootLength j < B.rootLength i
have hi : 0 < B.rootLength i
Tactic: have hi := B.rootLength_pos i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inl : ∀ (hji : P.pairingIn ℤ j i = -1), B.rootLength j < B.rootLength i
Tactic: rcases aux₁ with hji | hji
Cleared hypotheses: aux₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
inl : ∀ (hji : P.pairingIn ℤ j i = -1), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inr : ∀ (hji : P.pairingIn ℤ j i = 1), B.rootLength j < B.rootLength i
Tactic: rcases aux₁ with hji | hji
Cleared hypotheses: aux₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
⊢ B.rootLength j < B.rootLength i
have inl : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
inl : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inl₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
inl : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inl₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inl₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
inl : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inl₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
inl₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inl₃ : ∀ (hij' : P.pairingIn ℤ i j = 3), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
inl : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inl₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
inl₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
inl₃ : ∀ (hij' : P.pairingIn ℤ i j = 3), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inl₄ : ∀ (hij' : P.pairingIn ℤ i j = -4), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
inl : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inl₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
inl₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
inl₃ : ∀ (hij' : P.pairingIn ℤ i j = 3), B.rootLength j < B.rootLength i
inl₄ : ∀ (hij' : P.pairingIn ℤ i j = -4), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inl₅ : ∀ (hij' : P.pairingIn ℤ i j = 4), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
⊢ B.rootLength j < B.rootLength i
have inr : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
inr : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inr₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
inr : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inr₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inr₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
inr : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inr₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
inr₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inr₃ : ∀ (hij' : P.pairingIn ℤ i j = 3), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
inr : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inr₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
inr₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
inr₃ : ∀ (hij' : P.pairingIn ℤ i j = 3), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inr₄ : ∀ (hij' : P.pairingIn ℤ i j = -4), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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 : P.IsCrystallographic
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
inr : ∀ (hij' : P.pairingIn ℤ i j = -3), B.rootLength j < B.rootLength i
inr₁ : ∀ (hij' : P.pairingIn ℤ i j = -2), B.rootLength j < B.rootLength i
inr₂ : ∀ (hij' : P.pairingIn ℤ i j = 2), B.rootLength j < B.rootLength i
inr₃ : ∀ (hij' : P.pairingIn ℤ i j = 3), B.rootLength j < B.rootLength i
inr₄ : ∀ (hij' : P.pairingIn ℤ i j = -4), B.rootLength j < B.rootLength i
⊢ B.rootLength j < B.rootLength i
have inr₅ : ∀ (hij' : P.pairingIn ℤ i j = 4), B.rootLength j < B.rootLength i
Tactic: rcases hij' with hij' | hij' | hij' | hij' | hij' | hij'
Cleared hypotheses: hij'