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 : ι
have : ∀ (this : Fintype ι), P.coxeterWeightIn S i j ≤ 4
⊢ P.coxeterWeightIn S i j ≤ 4

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 ι
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
obtain :
  ∀ (si : S) (hsi : si > 0)
    (hsi' :
      Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) si : R)
        ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) :
              (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)),
    P.coxeterWeightIn S i j ≤ 4
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
obtain ⟨si, hsi, hsi'⟩ := (P.posRootForm S).exists_pos_eq i

Premises used: RootPairing.posRootForm, RootPairing.RootPositiveForm.exists_pos_eq
-- 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 : si > 0
hsi' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) si : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
obtain :
  ∀ (sj : S) (hsj : sj > 0)
    (hsj' :
      Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) sj : R)
        ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) :
              (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)),
    P.coxeterWeightIn S i j ≤ 4
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
obtain ⟨sj, hsj, hsj'⟩ := (P.posRootForm S).exists_pos_eq j

Premises used: RootPairing.posRootForm, RootPairing.RootPositiveForm.exists_pos_eq
-- 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 : si > 0
hsi' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) si : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
sj : S
hsj : sj > 0
hsj' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) sj : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) si : R) ((algebraMap S R : (a : S) → R) li : R)

Tactic:
simpa [li] using hsi'
-- 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 : si > 0
hsi' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) si : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
sj : S
hsj : sj > 0
hsj' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) sj : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ si = li

Tactic:
replace hsi' : si = li := algebraMap_injective S R <| by simpa [li] using hsi'
-- 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 : si > 0
sj : S
hsj : sj > 0
hsj' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) sj : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
hsi' : si = li
⊢ Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) sj : R) ((algebraMap S R : (a : S) → R) lj : R)

Tactic:
simpa [lj] using hsj'
-- 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 : si > 0
sj : S
hsj : sj > 0
hsj' :
  Eq.{u_2 + 1} («α» := R) ((algebraMap S R : (a : S) → R) sj : R)
    ((((RootPositiveForm.form (P.posRootForm S) : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
hsi' : si = li
⊢ sj = lj

Tactic:
replace hsj' : sj = lj := algebraMap_injective S R <| by simpa [lj] using hsj'
-- 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 : si > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
rw : ∀ (hsi : li > 0) (sj : S) (hsj : sj > 0) (hsi' : si = li) (hsj' : sj = lj), P.coxeterWeightIn S i j ≤ 4
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rw [hsi'] at hsi
-- 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 : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ lj > 0

Tactic:
rw [hsj'] at hsj
-- 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 : sj > 0
hsi' : si = li
hsj' : sj = lj
hsj₁ : lj > 0
⊢ si = li

Tactic:
rw [hsj'] at hsj
-- 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 : sj > 0
hsi' : si = li
hsj' : sj = lj
hsj₁ : lj > 0
hsi'₁ : si = li
⊢ sj = lj

Tactic:
rw [hsj'] at hsj
-- 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
rw : HPow.hPow (β := ℕ) lij 2 ≤ li * lj
⊢ 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)

Tactic:
rw [mul_le_mul_iff_right₀ four_pos]

Premises used: four_pos, mul_le_mul_iff_right₀
-- 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:
(P.posRootForm S).posForm.apply_sq_le_of_symm (zero_le_posForm _ _ ·)
      (P.posRootForm S).isSymm_posForm ri rj

Premises used: RootPairing.RootPositiveForm.rootLength, RootPairing.RootPositiveForm.posForm, RootPairing.zero_le_posForm, RootPairing.posRootForm, RootPairing.RootPositiveForm.isSymm_posForm, LinearMap.BilinForm.apply_sq_le_of_symm