awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x :
      S)
have 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))
Tactic: rw [posRootForm_posForm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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
    (∑ 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))
have this : P.IsAnisotropic
Tactic: have := P.isAnisotropic_of_isValuedIn S
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
have 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)
Tactic: obtain ⟨i, hi⟩ := P.exists_coroot_ne S hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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
⊢ 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))
have 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)
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (RootPositiveForm.posForm (P.posRootForm S))
have left : LinearMap.SeparatingLeft (M₁ := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
  (RootPositiveForm.posForm (P.posRootForm S))
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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))
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (RootPositiveForm.posForm (P.posRootForm S))
have right : LinearMap.SeparatingRight (M₁ := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
  (RootPositiveForm.posForm (P.posRootForm S))
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)))
⊢ (∀ (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
have 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)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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_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
have 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)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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_4} R ↥(P.corootSpan R)
have 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))
Tactic: rw [← P.finrank_range_polarization_eq_finrank_span_coroot R, range_polarizationIn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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))
⊢ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) = finrank.{u_2, u_4} R ↥(P.corootSpan R)
have 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))
Tactic: rw [← P.finrank_range_polarization_eq_finrank_span_coroot R, range_polarizationIn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
have rw : finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R)) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)
Tactic: rw [← finrank_rootSpan_map_polarization_eq_finrank_corootSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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.rootSpan R) (LinearMap.ker P.RootForm)
have this : IsReflexive R M
Tactic: have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) (LinearMap.ker P.RootForm)
have rw : Disjoint (P.rootSpan R) P.Polarization.ker
Tactic: rw [← P.ker_polarization_eq_ker_rootForm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
have refine : finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R))
Tactic: refine Submodule.disjoint_ker_of_finrank_le (L := P.rootSpan R) P.Polarization ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R))
have rw : finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(P.corootSpan R)
Tactic: rw [P.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, P.finrank_corootSpan_eq']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_4} R ↥(Submodule.map P.Polarization (P.rootSpan R))
have rw₁ : finrank.{u_2, u_3} R ↥(P.rootSpan R) ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R)
Tactic: rw [P.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, P.finrank_corootSpan_eq']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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.rootSpan R) (LinearMap.ker P.RootForm)
have this : IsReflexive R M
Tactic: have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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
⊢ IsCompl (P.rootSpan R) (LinearMap.ker P.RootForm)
have this₁ : IsReflexive R N
Tactic: have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
have refine : finrank R M ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
Tactic: refine (Submodule.isCompl_iff_disjoint _ _ ?_).mpr P.disjoint_rootSpan_ker_rootForm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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))
have rw : finrank R (Dual R N) = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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))
⊢ finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
have rw₁ : finrank R (Dual R N) = finrank.{u_2, u_4} R ↥(P.corootSpan 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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))
⊢ finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
have rw₂ : finrank R (Dual R N) = finrank R N
Tactic: rw [P.toPerfPair.finrank_eq, ← P.finrank_corootSpan_eq',
      Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R), Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank R M = finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
have rw₃ : finrank R N = finrank R N
Tactic: rw [P.toPerfPair.finrank_eq, ← P.finrank_corootSpan_eq',
      Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R), Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
have aux : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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 M ≤ finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
have rw : finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) ≤ finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
Tactic: rw [aux, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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 ↥(LinearMap.ker P.RootForm)
have 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)))
Tactic: convert! Submodule.finrank_mono P.corootSpan_dualAnnihilator_le_ker_rootForm