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 ι
S : Type u_5
inst_6 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : Module S M
inst_12 : IsScalarTower S R M
inst_13 : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) ⋯
rj : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) ⋯
li : S := RootPositiveForm.rootLength (P.posRootForm S) i
lj : S := RootPositiveForm.rootLength (P.posRootForm S) j
lij : S :=
  (((RootPositiveForm.posForm (P.posRootForm S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
          ri :
        LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
          (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
    rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)
⊢ P.coxeterWeightIn S i j ≤ 4
have key : HSMul.hSMul («α» := ℕ) 4 (HPow.hPow (β := ℕ) lij 2) = P.coxeterWeightIn S i j • (li * lj)
Tactic: have key : 4 • lij ^ 2 = P.coxeterWeightIn S i j • (li * lj) := by
    apply algebraMap_injective S R
    simpa [map_ofNat, lij, posRootForm, ri, rj, li, lj] using
       P.four_smul_rootForm_sq_eq_coxeterWeight_smul 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 ι
S : Type u_5
inst_6 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : Module S M
inst_12 : IsScalarTower S R M
inst_13 : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) ⋯
rj : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) ⋯
li : S := RootPositiveForm.rootLength (P.posRootForm S) i
lj : S := RootPositiveForm.rootLength (P.posRootForm S) j
lij : S :=
  (((RootPositiveForm.posForm (P.posRootForm S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
          ri :
        LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
          (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
    rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)
key : HSMul.hSMul («α» := ℕ) 4 (HPow.hPow (β := ℕ) lij 2) = P.coxeterWeightIn S i j • (li * lj)
⊢ P.coxeterWeightIn S i j ≤ 4
have key₁ : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)
Tactic: simp only [nsmul_eq_mul, smul_eq_mul, Nat.cast_ofNat] at key
Cleared hypotheses: key
-- 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 ι
S : Type u_5
inst_6 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : Module S M
inst_12 : IsScalarTower S R M
inst_13 : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) ⋯
rj : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) ⋯
li : S := RootPositiveForm.rootLength (P.posRootForm S) i
lj : S := RootPositiveForm.rootLength (P.posRootForm S) j
lij : S :=
  (((RootPositiveForm.posForm (P.posRootForm S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
          ri :
        LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
          (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
    rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)
key : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)
⊢ P.coxeterWeightIn S i j ≤ 4
have rwa : ∀ (cs : P.coxeterWeightIn S i j * (li * lj) ≤ 4 * (li * lj))
  (key : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)), P.coxeterWeightIn S i j ≤ 4
Tactic: rwa [key, mul_le_mul_iff_left₀ (by positivity)] at cs
Cleared hypotheses: cs, key
-- 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 ι
S : Type u_5
inst_6 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : Module S M
inst_12 : IsScalarTower S R M
inst_13 : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) ⋯
rj : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) ⋯
li : S := RootPositiveForm.rootLength (P.posRootForm S) i
lj : S := RootPositiveForm.rootLength (P.posRootForm S) j
lij : S :=
  (((RootPositiveForm.posForm (P.posRootForm S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
          ri :
        LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
          (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
    rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)
key : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)
rwa :
  ∀ (cs : P.coxeterWeightIn S i j * (li * lj) ≤ 4 * (li * lj))
    (key : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)), P.coxeterWeightIn S i j ≤ 4
⊢ P.coxeterWeightIn S i j ≤ 4
have rwa₁ : ∀ (cs : P.coxeterWeightIn S i j ≤ 4) (key : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)),
  P.coxeterWeightIn S i j ≤ 4
Tactic: rwa [key, mul_le_mul_iff_left₀ (by positivity)] at cs
Cleared hypotheses: cs, key
-- 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 : ι
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
have have : ∀ (this : Fintype ι), Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- 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 : ι
this : Fintype ι
⊢ ∃ (n : ℕ), P.coxeterWeightIn ℤ i j = (↑n : ℤ)
have this₁ : 0 ≤ P.coxeterWeightIn ℤ i j
Tactic: have : 0 ≤ P.coxeterWeightIn ℤ i j := by
      simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j
-- 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 : ι
this_1 : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
⊢ ∃ (n : ℕ), P.coxeterWeightIn ℤ i j = (↑n : ℤ)
have obtain : ∀ (n : ℕ) (hn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)), ∃ (n : ℕ), P.coxeterWeightIn ℤ i j = (↑n : ℤ)
Tactic: obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this
-- 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 : ι
this : Fintype ι
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
have obtain : ∀ (n : ℕ) (hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)),
  Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
Tactic: obtain ⟨n, hcn⟩ : ∃ n : ℕ, P.coxeterWeightIn ℤ i j = n := by
    have : 0 ≤ P.coxeterWeightIn ℤ i j := by
      simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j
    obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this
    exact ⟨n, by simp [hn]⟩
-- 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 : ι
this : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
have this₁ : P.coxeterWeightIn ℤ i j ≤ 4
Tactic: have : P.coxeterWeightIn ℤ i j ≤ 4 := P.coxeterWeightIn_le_four ℤ i j
-- 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 : ι
this_1 : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
this : P.coxeterWeightIn ℤ i j ≤ 4
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
have simp : ∀ (this : LE.le («α» := ℤ) (↑n : ℤ) 4),
  Eq («α» := ℤ) (↑n : ℤ) 0 ∨
    Eq («α» := ℤ) (↑n : ℤ) 1 ∨ Eq («α» := ℤ) (↑n : ℤ) 2 ∨ Eq («α» := ℤ) (↑n : ℤ) 3 ∨ Eq («α» := ℤ) (↑n : ℤ) 4
Tactic: simp only [hcn, mem_insert_iff, mem_singleton_iff] at this ⊢
Cleared hypotheses: this
-- 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 : ι
this_1 : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
this : LE.le («α» := ℤ) (↑n : ℤ) 4
⊢ Eq («α» := ℤ) (↑n : ℤ) 0 ∨
    Eq («α» := ℤ) (↑n : ℤ) 1 ∨ Eq («α» := ℤ) (↑n : ℤ) 2 ∨ Eq («α» := ℤ) (↑n : ℤ) 3 ∨ Eq («α» := ℤ) (↑n : ℤ) 4
have norm_cast : ∀ (this : n ≤ 4), n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4
Tactic: norm_cast at this ⊢
Cleared hypotheses: this
-- 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
⊢ 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)
have refine : P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0
Tactic: refine (Int.mul_mem_zero_one_two_three_four_iff ?_).mp
    (P.coxeterWeightIn_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
inst_9 : P.IsReduced
⊢ 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)
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 (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
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 j, P.pairingIn ℤ j i)
have 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)
Tactic: rcases eq_or_ne i j with rfl | h₁
Cleared hypotheses: j
-- 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
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne i j with rfl | 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 : 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
⊢ 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)
have 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)
Tactic: rcases eq_or_ne (α i) (-α j) with h₂ | 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 : 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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne (α i) (-α j) with h₂ | h₂
-- 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
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), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
have 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)
Tactic: have aux₁ := 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
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)
⊢ 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)
have aux₂ : 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₂
-- 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
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)
⊢ 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)
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
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)}
    (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), (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
-- 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 : ι
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)
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