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}
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
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i
have aux₃ : -1 * B.rootLength i = -3 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i
have aux₃ : -1 * B.rootLength i = -2 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i
have aux₃ : -1 * B.rootLength i = 2 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i
have aux₃ : -1 * B.rootLength i = 3 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i
have aux₃ : -1 * B.rootLength i = -4 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i
have aux₃ : -1 * B.rootLength i = 4 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i
have aux₃ : 1 * B.rootLength i = -3 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i
have aux₃ : 1 * B.rootLength i = -2 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i
have aux₃ : 1 * B.rootLength i = 2 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i
have aux₃ : 1 * B.rootLength i = 3 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i
have aux₃ : 1 * B.rootLength i = -4 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, hij'
-- 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}
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
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i
have aux₃ : 1 * B.rootLength i = 4 * B.rootLength j
Tactic: rw [hji, hij'] at aux₂
Cleared hypotheses: aux₂, hi, hji, 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
i j : ι
inst_8 : IsDomain R
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ P.pairingIn ℤ i j = P.pairingIn ℤ j i
have simp : P.pairing i j = P.pairing j i
Tactic: simp only [← (FaithfulSMul.algebraMap_injective ℤ R).eq_iff, algebraMap_pairingIn]
-- 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
i j : ι
inst_8 : IsDomain R
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
have len_eq₁ : P.pairingIn ℤ i j = P.pairingIn ℤ j i
Tactic: replace len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i := by
    simp only [← (FaithfulSMul.algebraMap_injective ℤ R).eq_iff, algebraMap_pairingIn]
    exact mul_right_cancel₀ (B.ne_zero j) (len_eq ▸ B.pairing_mul_eq_pairing_mul_swap j i)
Cleared hypotheses: len_eq
-- 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
i j : ι
inst_8 : IsDomain R
B : P.InvariantForm
len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
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
i j : ι
inst_8 : IsDomain R
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
ne : i ≠ j
ne' : 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)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
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
i j : ι
inst_8 : IsDomain R
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
ne : i ≠ j
ne' : 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)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
have this₁ : Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
Tactic: have := P.pairingIn_pairingIn_mem_set_of_length_eq len_eq
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.pairingIn ℤ i j = 0
⊢ P.coxeterWeightIn ℤ i j = 0
have rw : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 0
Tactic: rw [coxeterWeightIn, h, zero_mul]
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.pairingIn ℤ i j = 0
rw : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 0
⊢ P.coxeterWeightIn ℤ i j = 0
have rw₁ : 0 * P.pairingIn ℤ j i = 0
Tactic: rw [coxeterWeightIn, h, zero_mul]
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.pairingIn ℤ i j = 0
rw : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 0
rw₁ : 0 * P.pairingIn ℤ j i = 0
⊢ P.coxeterWeightIn ℤ i j = 0
have rw₂ : Eq («α» := ℤ) 0 0
Tactic: rw [coxeterWeightIn, h, zero_mul]
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
⊢ P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0
have refine : ∀ (h : P.coxeterWeightIn ℤ i j = 0), P.pairingIn ℤ i j = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [coxeterWeightIn, h, zero_mul]⟩
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa : ∀
  (h :
    Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
      ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
  P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₁ : ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₄ : ∀ (h : P.pairing i j = 0 ∧ P.pairing j i = 0), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h