awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) j
hij :
  Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi ≠
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) j hj
⊢ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) i

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) j
hij :
  Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi ≠
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) j hj
⊢ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) j

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) j
hij :
  Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi ≠
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) j hj
⊢ i ≠ j

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) j
hij :
  Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi ≠
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) j hj
⊢ LE.le (α := S)
    ((algebraMap ℤ S : (a : ℤ) → S)
        (P.pairingIn ℤ
          (↑(Subtype.mk (p := fun (x : ι) ↦
                Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi) :
            ι)
          (↑(Subtype.mk (p := fun (x : ι) ↦
                Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) j hj) :
            ι)) :
      S)
    (0 : S)

Tactic:
simpa using P.baseOf_pairwise_pairing_le_zero _ hf (by simpa) (by simpa) (by aesop : i ≠ j)

Premises used: RootPairing.baseOf_pairwise_pairing_le_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
⊢ Pairwise fun (i j : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦
    LE.le.{u_6} (α := S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                (v i) :
              LinearMap.{u_6, u_6, u_3, u_6} (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)
          (v j) :
        S)
      (0 : S)

Tactic:
have hn : Pairwise fun (i j : baseOf P.root (f : M →+ S)) ↦ B.posForm (v i) (v j) ≤ 0 := by
    rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
    rw [B.posForm_apply_root_root_le_zero_iff, ← P.algebraMap_pairingIn' S ℤ]
    simpa using P.baseOf_pairwise_pairing_le_zero _ hf (by simpa) (by simpa) (by aesop : i ≠ j)
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
hn :
  Pairwise fun (i j : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦
    LE.le.{u_6} (α := S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                (v i) :
              LinearMap.{u_6, u_6, u_3, u_6} (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)
          (v j) :
        S)
      (0 : S)
⊢ LinearIndependent S v

Tactic:
LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero B.posForm hB f' v hp hn

Premises used: Set.Mem, RootPairing.RootPositiveForm.posForm, LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
hn :
  Pairwise fun (i j : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦
    LE.le.{u_6} (α := S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                (v i) :
              LinearMap.{u_6, u_6, u_3, u_6} (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)
          (v j) :
        S)
      (0 : S)
⊢ LinearIndependent S v

Tactic:
exact LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero B.posForm hB f' v hp hn

Premises used: RootPairing.RootPositiveForm.posForm, LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
rw :
  range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ⊆
    (↑(span R (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)) : Set M)
⊢ LE.le.{u_3} (α := Submodule R M) ⊤ (span R (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι)))

Tactic:
rw [← IsRootSystem.span_root_eq_top (P := P), span_le, ← span_span_of_tower (R := ℤ)]

Premises used: Submodule.span_span_of_tower, Int, RootPairing.IsRootSystem.span_root_eq_top, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
a :
  Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M)
    (↑(span R (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)) : Set M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
apply subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
a :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M)),
    Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
      ((P.root : (a : ι) → M) i : M)
a₁ :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)),
    Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
      ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
rcases hsp i with hi | hi
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
simpa [SetLike.mem_coe, ← Submodule.mem_toAddSubgroup, span_int_eq_addSubgroupClosure,
        ← image_eq_range] using AddSubgroup.le_closure_toAddSubmonoid (P.root '' s) hi

Premises used: Set.image_eq_range, Submodule.mem_toAddSubgroup, Submodule.span_int_eq_addSubgroupClosure, RootPairing.root, SetLike.mem_coe, Set.image, AddSubgroup.le_closure_toAddSubmonoid, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    (-(P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
simpa [SetLike.mem_coe, ← Submodule.mem_toAddSubgroup, span_int_eq_addSubgroupClosure,
        ← image_eq_range] using AddSubgroup.le_closure_toAddSubmonoid (P.root '' s) hi

Premises used: Set.image_eq_range, Submodule.mem_toAddSubgroup, Submodule.span_int_eq_addSubgroupClosure, RootPairing.root, SetLike.mem_coe, Set.image, AddSubgroup.le_closure_toAddSubmonoid, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
b : Basis.{u_1, u_2, u_3} (↑s : Type u_1) R M := Basis.mk hli ⋯
have : ∀ (_i : Fintype (↑s : Type u_1)), s.ncard = finrank R M
⊢ s.ncard = finrank R M

Tactic:
have _i : Fintype s := Fintype.ofFinite s
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
b : Basis.{u_1, u_2, u_3} (↑s : Type u_1) R M := Basis.mk hli ⋯
_i : Fintype (↑s : Type u_1)
rw : ⋯.toFinset (s := s).card = finrank R M
⊢ s.ncard = finrank R M

Tactic:
rw [ncard_eq_toFinset_card]

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
b : Basis.{u_1, u_2, u_3} (↑s : Type u_1) R M := Basis.mk hli ⋯
_i : Fintype (↑s : Type u_1)
⊢ ⋯.toFinset (s := s).card = finrank R M

Tactic:
simpa using (finrank_eq_card_basis b).symm

Premises used: Module.finrank_eq_card_basis, Eq.symm