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 ι
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
⊢ HPow.hPow (β := ℕ) lij 2 ≤ li * lj

Tactic:
exact (P.posRootForm S).posForm.apply_sq_le_of_symm (zero_le_posForm _ _ ·)
      (P.posRootForm S).isSymm_posForm ri rj

Premises used: RootPairing.RootPositiveForm.posForm, RootPairing.zero_le_posForm, RootPairing.posRootForm, RootPairing.RootPositiveForm.isSymm_posForm, LinearMap.BilinForm.apply_sq_le_of_symm
-- 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 ι
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
⊢ 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)

Tactic:
have cs : 4 * lij ^ 2 ≤ 4 * (li * lj) := by
    rw [mul_le_mul_iff_right₀ four_pos]
    exact (P.posRootForm S).posForm.apply_sq_le_of_symm (zero_le_posForm _ _ ·)
      (P.posRootForm S).isSymm_posForm ri rj
-- 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 ι
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)
a :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) (HSMul.hSMul («α» := ℕ) 4 (HPow.hPow (β := ℕ) lij 2)) : R)
    ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j • (li * lj)) : R)
⊢ HSMul.hSMul («α» := ℕ) 4 (HPow.hPow (β := ℕ) lij 2) = P.coxeterWeightIn S i j • (li * lj)

Tactic:
apply algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- 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 ι
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)
⊢ Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) (HSMul.hSMul («α» := ℕ) 4 (HPow.hPow (β := ℕ) lij 2)) : R)
    ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j • (li * lj)) : R)

Tactic:
simpa [map_ofNat, lij, posRootForm, ri, rj, li, lj] using
       P.four_smul_rootForm_sq_eq_coxeterWeight_smul i j

Premises used: map_ofNat, RootPairing.posRootForm, RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul
-- 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 ι
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)
⊢ 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
-- 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 ι
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)
⊢ 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

Premises used: Nat.cast_ofNat, nsmul_eq_mul, smul_eq_mul
-- 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 ι
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 : P.coxeterWeightIn S i j * (li * lj) ≤ 4 * (li * lj)
key : 4 * HPow.hPow (β := ℕ) lij 2 = P.coxeterWeightIn S i j * (li * lj)
⊢ 0 < li * lj

Tactic:
positivity
-- 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 ι
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
rwa₁ rwa₂ rwa₃ 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
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rwa [key, mul_le_mul_iff_left₀ (by positivity)] at cs

Premises used: mul_le_mul_iff_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
i j : ι
have : ∀ (this : Fintype ι), Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- 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 : ι
this : Fintype ι
⊢ 0 ≤ P.coxeterWeightIn ℤ i j

Tactic:
simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j

Premises used: RootPairing.coxeterWeight_nonneg, RootPairing.algebraMap_coxeterWeightIn, Int, RootPairing.posRootForm
-- 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 : ι
this : Fintype ι
⊢ 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
-- 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 : ι
this_1 : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
obtain : ∀ (n : ℕ) (hn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)), ∃ (n : ℕ), P.coxeterWeightIn ℤ i j = (↑n : ℤ)
⊢ ∃ (n : ℕ), P.coxeterWeightIn ℤ i j = (↑n : ℤ)

Tactic:
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this

Premises used: Int.eq_ofNat_of_zero_le
-- 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 : ι
this_1 : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
n : ℕ
hn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
⊢ P.coxeterWeightIn ℤ i j = (↑n : ℤ)

Tactic:
simp [hn]
-- 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 : ι
this_1 : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
n : ℕ
hn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
⊢ ∃ (n : ℕ), P.coxeterWeightIn ℤ i j = (↑n : ℤ)

Tactic:
exact ⟨n, by simp [hn]⟩
-- 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 : ι
this : Fintype ι
obtain :
  ∀ (n : ℕ) (hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)),
    Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
⊢ 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]⟩

Premises used: Int, RootPairing.coxeterWeightIn
-- 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 : ι
this : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
⊢ P.coxeterWeightIn ℤ i j ≤ 4

Tactic:
have : P.coxeterWeightIn ℤ i j ≤ 4 := P.coxeterWeightIn_le_four ℤ 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 : ι
this_1 : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
this : P.coxeterWeightIn ℤ i j ≤ 4
simp :
  ∀ (this : LE.le («α» := ℤ) (↑n : ℤ) 4),
    Eq («α» := ℤ) (↑n : ℤ) 0 ∨
      Eq («α» := ℤ) (↑n : ℤ) 1 ∨ Eq («α» := ℤ) (↑n : ℤ) 2 ∨ Eq («α» := ℤ) (↑n : ℤ) 3 ∨ Eq («α» := ℤ) (↑n : ℤ) 4
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)

Tactic:
simp only [hcn, mem_insert_iff, mem_singleton_iff] at this ⊢

Premises used: Set.mem_singleton_iff, 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
i j : ι
this_1 : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
this : LE.le («α» := ℤ) (↑n : ℤ) 4
norm_cast : ∀ (this : n ≤ 4), n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4
⊢ Eq («α» := ℤ) (↑n : ℤ) 0 ∨
    Eq («α» := ℤ) (↑n : ℤ) 1 ∨ Eq («α» := ℤ) (↑n : ℤ) 2 ∨ Eq («α» := ℤ) (↑n : ℤ) 3 ∨ Eq («α» := ℤ) (↑n : ℤ) 4

Tactic:
norm_cast at this ⊢
-- 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 : ι
this_1 : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = (↑n : ℤ)
this : n ≤ 4
⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4

Tactic:
lia
-- 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
⊢ 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:
(Int.mul_mem_zero_one_two_three_four_iff ?_).mp
    (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)

Premises used: RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic, Int.mul_mem_zero_one_two_three_four_iff, Iff.mp
-- 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
refine : P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0
⊢ 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:
refine (Int.mul_mem_zero_one_two_three_four_iff ?_).mp
    (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)

Premises used: RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic, Int.mul_mem_zero_one_two_three_four_iff, Iff.mp
-- 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
⊢ P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0

Tactic:
simpa [← P.algebraMap_pairingIn ℤ] using P.pairing_eq_zero_iff' (i := i) (j := j)

Premises used: RootPairing.pairing_eq_zero_iff', RootPairing.algebraMap_pairingIn, Int