awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
inl :
  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 ℤ i i, P.pairingIn ℤ i i)
inr :
  ∀ (h₁ : i ≠ j),
    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 ℤ i j, P.pairingIn ℤ j i)
⊢ 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 ℤ i j, P.pairingIn ℤ j i)

Tactic:
rcases eq_or_ne i j with rfl | h₁

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
⊢ 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 ℤ i i, P.pairingIn ℤ i i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
inr :
  ∀ (h₂ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    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 ℤ i j, P.pairingIn ℤ j i)
inr₁ :
  ∀ (h₂ : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    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 ℤ i j, P.pairingIn ℤ j i)
⊢ 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 ℤ i j, P.pairingIn ℤ j i)

Tactic:
rcases eq_or_ne (α i) (-α j) with h₂ | h₂
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
h₂ : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ 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 ℤ i j, P.pairingIn ℤ j i)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
h₂ : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ 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 aux₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
h₂ : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
aux₁ :
  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)
⊢ P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4

Tactic:
have aux₂ : P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4 := P.coxeterWeightIn_ne_four ℤ h₁ h₂
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
h₂ : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
aux₁ :
  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)
aux₂ : P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4
⊢ 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 ℤ i j, P.pairingIn ℤ j i)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
hij : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hij' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
hij : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hij' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this : Module.IsReflexive R M
⊢ 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 ℤ i j, P.pairingIn ℤ j i)

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
hij : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hij' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this_1 : Module.IsReflexive R M
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 ℤ i j, P.pairingIn ℤ j i)
⊢ 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)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
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)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
have h : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
      ({(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)} : Set (ℤ × ℤ)) := by
    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
    aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h :
  Membership.mem (γ := Set (ℤ × ℤ)) {(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4

Tactic:
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at h

Premises used: Prod.mk_eq_one, Prod.mk_one_one, Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_insert_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h :
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4
⊢ P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j

Tactic:
have h' := B.pairingIn_mul_eq_pairingIn_mul_swap i j
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h :
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
⊢ 0 < B.rootLength i

Tactic:
have hi := B.rootLength_pos i
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h :
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
inl : ∀ (hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1), B.rootLength i ≤ B.rootLength j
inr : ∀ (hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2), B.rootLength i ≤ B.rootLength j
inr₁ : ∀ (hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3), B.rootLength i ≤ B.rootLength j
inr₂ : ∀ (hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4), B.rootLength i ≤ B.rootLength j
inr₃ : ∀ (hij' : P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1), B.rootLength i ≤ B.rootLength j
inr₄ : ∀ (hij' : P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2), B.rootLength i ≤ B.rootLength j
inr₅ : ∀ (hij' : P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3), B.rootLength i ≤ B.rootLength j
inr₆ : ∀ (hij' : P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4), B.rootLength i ≤ B.rootLength j
⊢ B.rootLength i ≤ B.rootLength j

Tactic:
rcases h with hij' | hij' | hij' | hij' | hij' | hij' | hij' | hij'
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1
⊢ 1 * B.rootLength i = 1 * B.rootLength j

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1
h'₁ : 1 * B.rootLength i = 1 * B.rootLength j
⊢ 0 < B.rootLength i

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1
h'₁ : 1 * B.rootLength i = 1 * B.rootLength j
hi₁ : 0 < B.rootLength i
⊢ P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2
⊢ 2 * B.rootLength i = 1 * B.rootLength j

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2
h'₁ : 2 * B.rootLength i = 1 * B.rootLength j
⊢ 0 < B.rootLength i

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2
h'₁ : 2 * B.rootLength i = 1 * B.rootLength j
hi₁ : 0 < B.rootLength i
⊢ P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3
⊢ 3 * B.rootLength i = 1 * B.rootLength j

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3
h'₁ : 3 * B.rootLength i = 1 * B.rootLength j
⊢ 0 < B.rootLength i

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3
h'₁ : 3 * B.rootLength i = 1 * B.rootLength j
hi₁ : 0 < B.rootLength i
⊢ P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4
⊢ 4 * B.rootLength i = 1 * B.rootLength j

Tactic:
rw [hij'.1, hij'.2] at h'

Premises used: And.right, And.left