awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
⊢ IsSumSq.{u_5} (R := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            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)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)
have suffices : Eq.{u_5 + 1} (α := S)
  ((((RootPositiveForm.posForm (P.posRootForm S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
              hx) :
          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)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx) :
    S)
  (∑ i : ι, s i * s i : S)
Tactic: suffices (P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩ = ∑ i, s i * s i from
    this ▸ IsSumSq.sum_mul_self Finset.univ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
⊢ Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            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)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)
    (∑ i : ι, s i * s i : S)
have a : Eq.{u_2 + 1} (α := R)
  ((algebraMap S R : (a : S) → R)
      ((((RootPositiveForm.posForm (P.posRootForm S) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                    x)
                  x hx) :
              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)
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
            hx) :
        S) :
    R)
  ((algebraMap S R : (a : S) → R) (∑ i : ι, s i * s i) : R)
Tactic: apply FaithfulSMul.algebraMap_injective S R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
s : (i : ι) → S
hs : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((RootPositiveForm.posForm (P.posRootForm S) :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  (Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                      x)
                    x hx) :
                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)
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
              hx) :
          S) :
      R)
    ((algebraMap S R : (a : S) → R) (∑ i : ι, s i * s i) : R)
have a : Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
  (∑ x : ι,
      HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) (s x) : R)
        ((algebraMap S R : (a : S) → R) (s x) : R) :
    R)
Tactic: simp only [posRootForm, RootPositiveForm.algebraMap_posForm, map_sum, map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x y : ↥(P.rootSpan S)
⊢ Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            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)
        y :
      S)
    (∑ i : ι,
        HMul.hMul (α := S) (β := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S) :
      S)
have refine : Eq.{u_2 + 1} (α := R)
  ((algebraMap S R : (a : S) → R)
      ((((RootPositiveForm.posForm (P.posRootForm S) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                x :
              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)
          y :
        S) :
    R)
  ((algebraMap S R : (a : S) → R)
      (∑ i : ι,
        HMul.hMul (α := S) (β := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S)) :
    R)
Tactic: refine (FaithfulSMul.algebraMap_injective S R) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ LE.le.{u_5} (α := S) (0 : S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            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)
        x :
      S)
have obtain : ∀ s ≥ 0,
  ∀
    (hs :
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)),
    LE.le.{u_5} (α := S) (0 : S)
      ((((RootPositiveForm.posForm (P.posRootForm S) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                x :
              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)
          x :
        S)
Tactic: obtain ⟨s, _, hs⟩ := P.exists_ge_zero_eq_rootForm S x.1 x.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
s : S
left : s ≥ 0
hs :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
⊢ LE.le.{u_5} (α := S) (0 : S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            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)
        x :
      S)
have this : s =
  (((RootPositiveForm.posForm (P.posRootForm S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
          x :
        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)
    x
Tactic: have : s = (P.posRootForm S).posForm x x :=
    FaithfulSMul.algebraMap_injective S R <| (P.algebraMap_posRootForm_posForm S x x) ▸ hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
s : S
left : s ≥ 0
hs :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
this :
  s =
    (((RootPositiveForm.posForm (P.posRootForm S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
            x :
          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)
      x
⊢ LE.le.{u_5} (α := S) (0 : S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            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)
        x :
      S)
have rwa : 0 ≤ s
Tactic: rwa [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl : ∀ (hij : P.pairingIn S i j = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rcases eq_or_ne (P.pairingIn S i j) 0 with hij | hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
inl : ∀ (hij : P.pairingIn S i j = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inr : ∀ (hij : P.pairingIn S i j ≠ 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rcases eq_or_ne (P.pairingIn S i j) 0 with hij | hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl : ∀ (hji : P.pairingIn S j i = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
inl : ∀ (hji : P.pairingIn S j i = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl₁ : ∀ (hji : P.pairingIn S j i ≠ 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inr : ∀ (hji : P.pairingIn S j i = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
inr : ∀ (hji : P.pairingIn S j i = 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inr₁ : ∀ (hji : P.pairingIn S j i ≠ 0), P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl : LE.le.{u_5} (α := S) 0 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rw [hij, hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
inl : LE.le.{u_5} (α := S) 0 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl₁ : LE.le.{u_5} (α := S) 0 0 ↔ LE.le.{u_5} (α := S) 0 0
Tactic: rw [hij, hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl : LE.le.{u_5} (α := S) 0 0 ↔ P.pairingIn S j i ≤ 0
Tactic: rw [hij, P.pairingIn_eq_zero_iff.mp hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i ≠ 0
inl : LE.le.{u_5} (α := S) 0 0 ↔ P.pairingIn S j i ≤ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inl₁ : LE.le.{u_5} (α := S) 0 0 ↔ LE.le.{u_5} (α := S) 0 0
Tactic: rw [hij, P.pairingIn_eq_zero_iff.mp hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inr : P.pairingIn S i j ≤ 0 ↔ LE.le.{u_5} (α := S) 0 0
Tactic: rw [hji, P.pairingIn_eq_zero_iff.mp hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i = 0
inr : P.pairingIn S i j ≤ 0 ↔ LE.le.{u_5} (α := S) 0 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inr₁ : LE.le.{u_5} (α := S) 0 0 ↔ LE.le.{u_5} (α := S) 0 0
Tactic: rw [hji, P.pairingIn_eq_zero_iff.mp hji]