awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (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 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
rw : Eq (α := Submodule ℤ M) (Submodule.span ℤ (image (α := ι) (⇑P.root : (a : ι) → M) {i, j})) (P.rootSpan ℤ)
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)
have rw₁ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑{i, j} : Set ι))) (P.rootSpan ℤ)
Tactic: rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (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 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
rw : Eq (α := Submodule ℤ M) (Submodule.span ℤ (image (α := ι) (⇑P.root : (a : ι) → M) {i, j})) (P.rootSpan ℤ)
rw₁ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑{i, j} : Set ι))) (P.rootSpan ℤ)
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)
have rw₂ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan ℤ)
Tactic: rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (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 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
rw : Eq (α := Submodule ℤ M) (Submodule.span ℤ (image (α := ι) (⇑P.root : (a : ι) → M) {i, j})) (P.rootSpan ℤ)
rw₁ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑{i, j} : Set ι))) (P.rootSpan ℤ)
rw₂ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan ℤ)
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)
have rw₃ : Eq (α := Submodule ℤ M) (Submodule.span ℤ (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) (P.rootSpan ℤ)
Tactic: rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (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 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)
have have : {i, j} ⊆ b.support
Tactic: classical
  have : {i, j} ⊆ b.support := by grind
  rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (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 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
have : {i, j} ⊆ b.support
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)
have have₁ : ∀ (this : {i, j} ⊆ b.support),
  Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)
Tactic: classical
  have : {i, j} ⊆ b.support := by grind
  rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]
-- 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 : ι
⊢ P.coxeterWeightIn S i j ≤ 4
have have : ∀ (this : Fintype ι), P.coxeterWeightIn S i j ≤ 4
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- 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
⊢ P.coxeterWeightIn S i j ≤ 4
have 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
Tactic: obtain ⟨si, hsi, hsi'⟩ := (P.posRootForm S).exists_pos_eq i
-- 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 : 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
have 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
Tactic: obtain ⟨sj, hsj, hsj'⟩ := (P.posRootForm S).exists_pos_eq 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 : 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)
⊢ P.coxeterWeightIn S i j ≤ 4
have hsi'₁ : si = li
Tactic: replace hsi' : si = li := algebraMap_injective S R <| by simpa [li] using hsi'
Cleared hypotheses: hsi'
-- 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 : 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
⊢ P.coxeterWeightIn S i j ≤ 4
have hsj'₁ : sj = lj
Tactic: replace hsj' : sj = lj := algebraMap_injective S R <| by simpa [lj] using hsj'
Cleared hypotheses: hsj'
-- 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 : si > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4
have rw : ∀ (hsi : li > 0) (sj : S) (hsj : sj > 0) (hsi' : si = li) (hsj' : sj = lj), P.coxeterWeightIn S i j ≤ 4
Tactic: rw [hsi'] at hsi
Cleared hypotheses: hsi, sj, hsj, hsi', hsj'
-- 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 : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4
have hsj₁ : lj > 0
Tactic: rw [hsj'] at hsj
Cleared hypotheses: hsj, hsi', hsj'
-- 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
⊢ 4 * HPow.hPow (β := ℕ) lij 2 ≤ 4 * (li * lj)
have rw : HPow.hPow (β := ℕ) lij 2 ≤ li * lj
Tactic: rw [mul_le_mul_iff_right₀ four_pos]
-- 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
⊢ P.coxeterWeightIn S i j ≤ 4
have cs : 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
-- 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)
⊢ HSMul.hSMul («α» := ℕ) 4 (HPow.hPow (β := ℕ) lij 2) = P.coxeterWeightIn S i j • (li * lj)
have 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)
Tactic: apply algebraMap_injective S R