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
S : Type u_5
inst_6 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
⊢ (fun (i j : ι) ↦
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    i j

Tactic:
have := IsAddIndecomposable.pairwise_baseOf_sub_notMem P.root (by simp) f hf hi hj hne
-- 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
S : Type u_5
inst_6 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
this :
  (fun (i j : ι) ↦
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    i j
contrapose! :
  ∀ (this : 0 < P.pairingIn ℤ i j),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ P.pairingIn ℤ i j ≤ 0

Tactic:
contrapose! this
-- 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
S : Type u_5
inst_6 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
this : 0 < P.pairingIn ℤ i j
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))

Tactic:
P.root_sub_root_mem_of_pairingIn_pos this hne

Premises used: RootPairing.root_sub_root_mem_of_pairingIn_pos
-- 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
S : Type u_5
inst_6 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
this : 0 < P.pairingIn ℤ i j
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))

Tactic:
exact P.root_sub_root_mem_of_pairingIn_pos this hne

Premises used: RootPairing.root_sub_root_mem_of_pairingIn_pos
-- 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)
⊢ CharZero R

Tactic:
have : CharZero R := Algebra.charZero_of_charZero S R
-- 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 : CharZero R
have :
  ∀ (this : Fintype ι),
    LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
      (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))
⊢ LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
    (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- 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 : ι)
change : LinearIndependent S (M := M) ((⇑M₀.subtype : (a : ↥M₀) → M) ∘ v)
⊢ LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
    (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))

Tactic:
change LinearIndependent S (M₀.subtype ∘ v)

Premises used: Function.comp, LinearIndependent, Submodule.subtype, 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 : 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_2 : 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 : ι)
this : LinearIndependent S v
⊢ Disjoint (span S (range v)) M₀.subtype.ker

Tactic:
simp
-- 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_2 : 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 : ι)
this : LinearIndependent S v
rwa rwa₁ rwa₂ rwa₃ : LinearIndependent S v
⊢ LinearIndependent S (M := M) ((⇑M₀.subtype : (a : ↥M₀) → M) ∘ v)

Tactic:
rwa [LinearMap.linearIndependent_iff_of_disjoint M₀.subtype (by simp)]

Premises used: LinearMap.linearIndependent_iff_of_disjoint, Submodule.subtype
-- 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 : ι)
suffices : LinearIndependent S v
⊢ LinearIndependent S (M := M) ((⇑M₀.subtype : (a : ↥M₀) → M) ∘ v)

Tactic:
suffices LinearIndependent S v by
    rwa [LinearMap.linearIndependent_iff_of_disjoint M₀.subtype (by simp)]
-- 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
⊢ QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap (RootPositiveForm.posForm (P.posRootForm S)))

Tactic:
simpa using P.posRootForm_rootFormIn_posDef S

Premises used: RootPairing.posRootForm_rootFormIn_posDef
-- 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
obtain :
  ∀ (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)),
    LinearIndependent S v
⊢ LinearIndependent S v

Tactic:
obtain ⟨B, hB⟩ : ∃ B : P.RootPositiveForm S, B.posForm.toQuadraticMap.PosDef :=
    ⟨P.posRootForm S, by simpa using P.posRootForm_rootFormIn_posDef S⟩

Premises used: RootPairing.RootPositiveForm
-- 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)
i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)
obtain :
  ∀ (i : ι)
    (left :
      Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)} i)
    (hi :
      ∀ (j : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)}
            j →
          ∀ (k : ι),
            Membership.mem (γ := Set ι)
                {i : ι |
                  LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)}
                k →
              (P.root : (a : ι) → M) i =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M) →
                Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
                  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)),
    LT.lt.{u_6} (α := S) (0 : S)
      ((f' : (a : ↥M₀) → S)
          (v
            (Subtype.mk (p := fun (x : ι) ↦
              Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i ⋯)) :
        S)
⊢ LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)

Tactic:
obtain ⟨i, -, hi⟩ := i
-- 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)
i : ι
left :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)} i
hi :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)}
            k →
          (P.root : (a : ι) → M) i =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M) →
            Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
              Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
⊢ LT.lt.{u_6} (α := S) (0 : S)
    ((f' : (a : ↥M₀) → S)
        (v
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x)
            i ⋯)) :
      S)

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)
⊢ ∀ (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)

Tactic:
have hp (i : baseOf P.root (f : M →+ S)) : 0 < f' (v i) := by obtain ⟨i, -, hi⟩ := i; 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
rw :
  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)
⊢ 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
                (Subtype.mk (p := fun (x : ι) ↦
                  Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi)) :
            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
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x)
            j hj)) :
      S)
    (0 : S)

Tactic:
rw [B.posForm_apply_root_root_le_zero_iff, ← P.algebraMap_pairingIn' S ℤ]

Premises used: Set.mem_range_self, RootPairing.RootPositiveForm.posForm_apply_root_root_le_zero_iff, Int, RootPairing.algebraMap_pairingIn', Submodule.subset_span