awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
this_1 : IsReflexive R M
this : IsTorsionFree S M
⊢ finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) ≤
    finrank.{u_5, u_4} S ↥(Submodule.map (M := ↥(P.rootSpan S)) (P.PolarizationIn S) ⊤)

Tactic:
Submodule.finrank_mono <| le_of_eq <| LinearMap.range_eq_map (P.PolarizationIn S)

Premises used: Set.Mem, RootPairing.PolarizationIn, Submodule.finrank_mono, LinearMap.range_eq_map, le_of_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
this_1 : IsReflexive R M
this : IsTorsionFree S M
⊢ finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) ≤
    finrank.{u_5, u_4} S ↥(Submodule.map (M := ↥(P.rootSpan S)) (P.PolarizationIn S) ⊤)

Tactic:
exact Submodule.finrank_mono <| le_of_eq <| LinearMap.range_eq_map (P.PolarizationIn S)

Premises used: RootPairing.PolarizationIn, Submodule.finrank_mono, LinearMap.range_eq_map, le_of_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
x : ↥(P.rootSpan S)
hx : x ≠ 0
⊢ Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)

Tactic:
have hI := P.polarizationIn_Injective S
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
x : ↥(P.rootSpan S)
hx : x ≠ 0
hI : Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
⊢ Ne.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) x : N) (0 : N)

Tactic:
have h := (map_ne_zero_iff (P.PolarizationIn S) hI).mpr hx
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
x : ↥(P.rootSpan S)
hx : x ≠ 0
hI : Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
h : Ne.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) x : N) (0 : N)
⊢ Ne.{u_4 + 1} (α := N)
    (∑ i : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) i : N))
    0

Tactic:
rw [PolarizationIn_apply] at h

Premises used: RootPairing.PolarizationIn_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
x : ↥(P.rootSpan S)
hx : x ≠ 0
hI : Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
h :
  Ne.{u_4 + 1} (α := N)
    (∑ i : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) i : N))
    0
contrapose! :
  ∀ (h : ∀ (i : ι), Eq.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)),
    Eq.{u_4 + 1} (α := N)
      (∑ i : ι,
        HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot : (a : ι) → N) i : N))
      0
⊢ ∃ (i : ι), Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
x : ↥(P.rootSpan S)
hx : x ≠ 0
hI : Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
h : ∀ (i : ι), Eq.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
i : ι
⊢ Eq.{u_4 + 1} (α := N)
    ((fun (a : ι) ↦
        HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S a : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot : (a : ι) → N) a : N))
      i)
    0

Tactic:
simp [h i]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
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.IsAnisotropic
x : ↥(P.rootSpan S)
hx : x ≠ 0
hI : Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
h : ∀ (i : ι), Eq.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
⊢ Eq.{u_4 + 1} (α := N)
    (∑ i : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) i : N))
    0

Tactic:
exact Fintype.sum_eq_zero (fun a ↦ (P.coroot'In S a) x • P.coroot a) fun i ↦ by simp [h i]

Premises used: Fintype.sum_eq_zero, HSMul.hSMul, RootPairing.coroot, DFunLike.coe, RootPairing.coroot'In
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
rw :
  LT.lt.{u_5} (α := S) 0
    (∑ 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) x : S))
⊢ LT.lt.{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:
rw [posRootForm_posForm_apply_apply]

Premises used: RootPairing.posRootForm_posForm_apply_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
⊢ P.IsAnisotropic

Tactic:
have := P.isAnisotropic_of_isValuedIn S
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
obtain :
  ∀ (i : ι) (hi : Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)),
    ∃ (i : ι),
      Membership.mem (γ := Finset ι) Finset.univ i ∧
        0 <
          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) x : S)
⊢ ∃ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i ∧
      0 <
        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) x : S)

Tactic:
obtain ⟨i, hi⟩ := P.exists_coroot_ne S hx

Premises used: RootPairing.exists_coroot_ne
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
i : ι
hi : Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
h :
  Membership.mem (γ := Finset ι) Finset.univ i ∧
    0 <
      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) x : S)
⊢ ∃ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i ∧
      0 <
        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) x : S)

Tactic:
use i
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
i : ι
hi : Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
⊢ Membership.mem (γ := Finset ι) Finset.univ i ∧
    0 <
      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) x : S)

Tactic:
⟨Finset.mem_univ i, mul_self_pos.mpr hi⟩

Premises used: Iff.mpr, Finset.mem_univ, mul_self_pos, And.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
i : ι
hi : Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
⊢ Membership.mem (γ := Finset ι) Finset.univ i ∧
    0 <
      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) x : S)

Tactic:
exact ⟨Finset.mem_univ i, mul_self_pos.mpr hi⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
⊢ ∃ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i ∧
      0 <
        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) x : S)

Tactic:
have : ∃ i ∈ Finset.univ, 0 < (P.coroot'In S i) x * (P.coroot'In S i) x := by
    obtain ⟨i, hi⟩ := P.exists_coroot_ne S hx
    use i
    exact ⟨Finset.mem_univ i, mul_self_pos.mpr hi⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this_1 : P.IsAnisotropic
this :
  ∃ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i ∧
      0 <
        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) x : S)
⊢ LT.lt.{u_5} (α := S) 0
    (∑ 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) x : S))

Tactic:
Finset.sum_pos' (fun i a ↦ mul_self_nonneg ((P.coroot'In S i) x)) this

Premises used: mul_self_nonneg, Finset.sum_pos', DFunLike.coe, RootPairing.coroot'In
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this_1 : P.IsAnisotropic
this :
  ∃ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i ∧
      0 <
        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) x : S)
⊢ LT.lt.{u_5} (α := S) 0
    (∑ 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) x : S))

Tactic:
exact Finset.sum_pos' (fun i a ↦ mul_self_nonneg ((P.coroot'In S i) x)) this

Premises used: mul_self_nonneg, Finset.sum_pos', DFunLike.coe, RootPairing.coroot'In
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
⊢ LT.lt.{u_5} (α := S) (0 : S) ((LinearMap.BilinMap.toQuadraticMap (P.RootFormIn S) : (a : ↥(P.rootSpan S)) → S) x : S)

Tactic:
simpa using P.posRootForm_posForm_pos_of_ne_zero S hx

Premises used: RootPairing.posRootForm_posForm_pos_of_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
⊢ QuadraticMap.Anisotropic (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap (RootPositiveForm.posForm (P.posRootForm S)))

Tactic:
fun _ hx ↦ Classical.byContradiction fun h ↦
    (ne_of_lt (posRootForm_posForm_pos_of_ne_zero P S h)).symm hx

Premises used: Classical.byContradiction, QuadraticMap.Anisotropic, RootPairing.posRootForm_posForm_pos_of_ne_zero, Ne.symm, ne_of_lt
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
left :
  LinearMap.SeparatingLeft (M₁ := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (RootPositiveForm.posForm (P.posRootForm S))
right :
  LinearMap.SeparatingRight (M₁ := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (RootPositiveForm.posForm (P.posRootForm S))
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (RootPositiveForm.posForm (P.posRootForm S))

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
left :
  x ≠ 0 →
    ∃ (y : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
      Ne.{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)
        (0 : S)
⊢ (∀ (y : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
      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)
        (0 : S)) →
    x = 0

Tactic:
contrapose!
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
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 : CommRing S
inst_7 : LinearOrder S
inst_8 : IsStrictOrderedRing S
inst_9 : IsDomain R
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : Module S M
inst_14 : IsScalarTower S R M
inst_15 : Module S N
inst_16 : IsScalarTower S R N
x : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ x ≠ 0 →
    ∃ (y : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
      Ne.{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)
        (0 : S)

Tactic:
fun hx ↦ ⟨x, (posRootForm_posForm_pos_of_ne_zero P S hx).ne'⟩

Premises used: RootPairing.posRootForm_posForm_pos_of_ne_zero, LT.lt.ne', Exists.intro