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 : 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:
exact fun hx ↦ ⟨x, (posRootForm_posForm_pos_of_ne_zero P S hx).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 : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
right :
  x ≠ 0 →
    ∃ (x_1 : ↥(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_1 :
                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)
        (0 : S)
⊢ (∀ (x_1 : ↥(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_1 :
                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)
        (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 →
    ∃ (x_1 : ↥(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_1 :
                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)
        (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
-- 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 →
    ∃ (x_1 : ↥(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_1 :
                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)
        (0 : S)

Tactic:
exact fun hx ↦ ⟨x, (posRootForm_posForm_pos_of_ne_zero P S hx).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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
rw :
  finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) =
    finrank.{u_2, u_4} R ↥(LinearMap.range (M := ↥(P.rootSpan R)) (P.PolarizationIn R))
rw₁ rw₂ :
  finrank.{u_2, u_4} R ↥(LinearMap.range (M := ↥(P.rootSpan R)) (P.PolarizationIn R)) =
    finrank.{u_2, u_4} R ↥(LinearMap.range (M := ↥(P.rootSpan R)) (P.PolarizationIn R))
⊢ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) = finrank.{u_2, u_4} R ↥(P.corootSpan R)

Tactic:
rw [← P.finrank_range_polarization_eq_finrank_span_coroot R, range_polarizationIn]

Premises used: RootPairing.finrank_range_polarization_eq_finrank_span_coroot, RootPairing.range_polarizationIn
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
rw : finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)

Tactic:
rw [← finrank_rootSpan_map_polarization_eq_finrank_corootSpan]

Premises used: RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
⊢ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)

Tactic:
Submodule.finrank_map_le P.Polarization (P.rootSpan R)

Premises used: Submodule.finrank_map_le, RootPairing.rootSpan, RootPairing.Polarization
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
⊢ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)

Tactic:
exact Submodule.finrank_map_le P.Polarization (P.rootSpan R)

Premises used: Submodule.finrank_map_le, RootPairing.rootSpan, RootPairing.Polarization
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank.{u_2, u_3} R ↥(P.rootSpan R)

Tactic:
le_antisymm P.finrank_corootSpan_le' P.flip.finrank_corootSpan_le'

Premises used: RootPairing.flip, le_antisymm, _private.0.RootPairing.finrank_corootSpan_le'
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
⊢ IsReflexive R M

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
this : IsReflexive R M
rw : Disjoint (P.rootSpan R) P.Polarization.ker
⊢ Disjoint (P.rootSpan R) (LinearMap.ker P.RootForm)

Tactic:
rw [← P.ker_polarization_eq_ker_rootForm]

Premises used: RootPairing.ker_polarization_eq_ker_rootForm
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint (P.rootSpan R) P.Polarization.ker

Tactic:
Submodule.disjoint_ker_of_finrank_le (L := P.rootSpan R) P.Polarization ?_

Premises used: Submodule.disjoint_ker_of_finrank_le, RootPairing.Polarization
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
this : IsReflexive R M
refine : finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R))
⊢ Disjoint (P.rootSpan R) P.Polarization.ker

Tactic:
refine Submodule.disjoint_ker_of_finrank_le (L := P.rootSpan R) P.Polarization ?_

Premises used: Submodule.disjoint_ker_of_finrank_le, RootPairing.Polarization
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
this : IsReflexive R M
rw : finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(P.corootSpan R)
rw₁ rw₂ : finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R))

Tactic:
rw [P.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, P.finrank_corootSpan_eq']

Premises used: RootPairing.finrank_corootSpan_eq', RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
⊢ Disjoint (P.corootSpan R) (LinearMap.ker P.CorootForm)

Tactic:
P.flip.disjoint_rootSpan_ker_rootForm

Premises used: RootPairing.flip, RootPairing.CorootForm, RootPairing.disjoint_rootSpan_ker_rootForm
-- 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 : IsDomain R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsAnisotropic
inst_8 : P.IsRootSystem
⊢ P.RootForm.Nondegenerate

Tactic:
simpa [(rootForm_symmetric P).isRefl.nondegenerate_iff_separatingLeft,
    LinearMap.separatingLeft_iff_ker_eq_bot] using P.disjoint_rootSpan_ker_rootForm

Premises used: LinearMap.IsSymm.isRefl, LinearMap.separatingLeft_iff_ker_eq_bot, RootPairing.disjoint_rootSpan_ker_rootForm, LinearMap.IsRefl.nondegenerate_iff_separatingLeft, RootPairing.rootForm_symmetric
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ IsReflexive R M

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this : IsReflexive R M
⊢ IsReflexive R N

Tactic:
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
⊢ IsCompl (P.rootSpan R) (LinearMap.ker P.RootForm)

Tactic:
(Submodule.isCompl_iff_disjoint _ _ ?_).mpr P.disjoint_rootSpan_ker_rootForm

Premises used: Iff.mpr, Submodule.isCompl_iff_disjoint, RootPairing.disjoint_rootSpan_ker_rootForm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
refine : finrank R M ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
⊢ IsCompl (P.rootSpan R) (LinearMap.ker P.RootForm)

Tactic:
refine (Submodule.isCompl_iff_disjoint _ _ ?_).mpr P.disjoint_rootSpan_ker_rootForm

Premises used: Iff.mpr, Submodule.isCompl_iff_disjoint, RootPairing.disjoint_rootSpan_ker_rootForm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
rw :
  finrank R (Dual R N) = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
rw₁ :
  finrank R (Dual R N) =
    finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
rw₂ : finrank R (Dual R N) = finrank R N
rw₃ rw₄ : finrank R N = finrank R N
⊢ finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
rw [P.toPerfPair.finrank_eq, ← P.finrank_corootSpan_eq',
      Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R), Subspace.dual_finrank_eq]

Premises used: RootPairing.finrank_corootSpan_eq', RootPairing.toLinearMap, Subspace.dual_finrank_eq, LinearEquiv.finrank_eq, LinearMap.toPerfPair, RootPairing.corootSpan, Subspace.finrank_add_finrank_dualAnnihilator_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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
⊢ finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
have aux : finrank R M =
      finrank R (P.rootSpan R) + finrank R (P.corootSpan R).dualAnnihilator := by
    rw [P.toPerfPair.finrank_eq, ← P.finrank_corootSpan_eq',
      Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R), Subspace.dual_finrank_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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
rw : finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) ≤ finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
⊢ finrank R M ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)

Tactic:
rw [aux, add_le_add_iff_left]

Premises used: add_le_add_iff_left
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))) ≤
    finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)

Tactic:
Submodule.finrank_mono P.corootSpan_dualAnnihilator_le_ker_rootForm

Premises used: Submodule.finrank_mono, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
h :
  finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) =
    finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)))
⊢ finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) ≤ finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)

Tactic:
convert! Submodule.finrank_mono P.corootSpan_dualAnnihilator_le_ker_rootForm

Premises used: Submodule.finrank_mono, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) =
    finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)))

Tactic:
(LinearEquiv.finrank_map_eq _ _).symm

Premises used: Set.Mem, LinearEquiv.finrank_map_eq, Eq.symm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) =
    finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)))

Tactic:
exact (LinearEquiv.finrank_map_eq _ _).symm

Premises used: LinearEquiv.finrank_map_eq, Eq.symm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ IsCompl (P.corootSpan R) (LinearMap.ker P.CorootForm)

Tactic:
P.flip.isCompl_rootSpan_ker_rootForm

Premises used: RootPairing.flip, RootPairing.CorootForm, RootPairing.isCompl_rootSpan_ker_rootForm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this_2 : IsReflexive R N
this : finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ LinearMap.ker P.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
(Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm

Premises used: Submodule.eq_of_le_of_finrank_eq, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, Eq.symm
-- 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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this_2 : IsReflexive R N
this : finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
refine :
  finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))) =
    finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
⊢ LinearMap.ker P.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
refine (Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm

Premises used: Submodule.eq_of_le_of_finrank_eq, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, Eq.symm