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 N
this_2 : IsTorsionFree S N
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  Eq.{u_5 + 1} (α := S)
    ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) :
      S)
    (0 : S)
this :
  Eq.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑(P.rootSpanMem S i) : M) : M →ₗ[R] R) : (a : M) → R)
        (↑(P.rootSpanMem S i) : M) :
      R)
    (0 : R)
⊢ False

Tactic:
apply IsAnisotropic.rootForm_root_ne_zero i this

Premises used: RootPairing.IsAnisotropic.rootForm_root_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 : 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 N
this : IsTorsionFree S N
⊢ Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0

Tactic:
have h_ne : ∏ i, (P.RootFormIn S (P.rootSpanMem S i) (P.rootSpanMem S i)) ≠ 0 := by
    refine Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_
    have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h
    rw [algebraMap_rootFormIn] at this
    apply IsAnisotropic.rootForm_root_ne_zero i this
-- 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
⊢ finrank.{u_5, u_4} S ↥(P.corootSpan S) ≤
    finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))

Tactic:
LinearMap.finrank_le_of_isSMulRegular (P.corootSpan S)
    (LinearMap.range (M₂ := N) (P.PolarizationIn S))
    (smul_right_injective N h_ne) ?_

Premises used: LinearMap.range, RootPairing.PolarizationIn, smul_right_injective, RootPairing.corootSpan, LinearMap.finrank_le_of_isSMulRegular
-- 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
refine :
  ∀ (x : N),
    Membership.mem (γ := Submodule S N) (P.corootSpan S) x →
      Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
        (HSMul.hSMul.{u_5, u_4, u_4} (α := S)
          (∏ i : ι,
            (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                  LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
                (a : ↥(P.rootSpan S)) → S)
              (P.rootSpanMem S i))
          x)
⊢ finrank.{u_5, u_4} S ↥(P.corootSpan S) ≤
    finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))

Tactic:
refine LinearMap.finrank_le_of_isSMulRegular (P.corootSpan S)
    (LinearMap.range (M₂ := N) (P.PolarizationIn S))
    (smul_right_injective N h_ne) ?_

Premises used: LinearMap.range, RootPairing.PolarizationIn, smul_right_injective, RootPairing.corootSpan, LinearMap.finrank_le_of_isSMulRegular
-- 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
x : N
hx : Membership.mem (γ := Submodule S N) (P.corootSpan S) x
obtain :
  ∀ (c : ι → S) (hc : ∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N) = x),
    Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
      (HSMul.hSMul.{u_5, u_4, u_4} (α := S)
        (∏ i : ι,
          (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            (P.rootSpanMem S i))
        x)
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (HSMul.hSMul.{u_5, u_4, u_4} (α := S)
      (∏ i : ι,
        (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i))
      x)

Tactic:
obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun S).mp hx

Premises used: Submodule.mem_span_range_iff_exists_fun, Iff.mp
-- 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
x : N
hx : Membership.mem (γ := Submodule S N) (P.corootSpan S) x
c : ι → S
hc : ∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N) = x
rw :
  Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (∑ x : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S)
        (∏ i : ι,
          (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            (P.rootSpanMem S i))
        (HSMul.hSMul (β := N) (c x) ((P.coroot : (a : ι) → N) x : N)))
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (HSMul.hSMul.{u_5, u_4, u_4} (α := S)
      (∏ i : ι,
        (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i))
      x)

Tactic:
rw [← hc, Finset.smul_sum]

Premises used: Finset.smul_sum
-- 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
x : N
hx : Membership.mem (γ := Submodule S N) (P.corootSpan S) x
c : ι → S
hc : ∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N) = x
simp_rw :
  Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (∑ x : ι,
      c x •
        HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
          (∏ i : ι,
            (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                  LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
                (a : ↥(P.rootSpan S)) → S)
              (P.rootSpanMem S i))
          ((P.coroot : (a : ι) → N) x : N))
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (∑ x : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S)
        (∏ i : ι,
          (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            (P.rootSpanMem S i))
        (HSMul.hSMul (β := N) (c x) ((P.coroot : (a : ι) → N) x : N)))

Tactic:
simp_rw [smul_smul, mul_comm, ← smul_smul]

Premises used: smul_smul, mul_comm
-- 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
x : N
hx : Membership.mem (γ := Submodule S N) (P.corootSpan S) x
c : ι → S
hc : ∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N) = x
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (∑ x : ι,
      c x •
        HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
          (∏ i : ι,
            (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                  LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
                (a : ↥(P.rootSpan S)) → S)
              (P.rootSpanMem S i))
          ((P.coroot : (a : ι) → N) x : N))

Tactic:
Submodule.sum_smul_mem (LinearMap.range (P.PolarizationIn S)) c
    fun j _ ↦ prod_rootFormIn_smul_coroot_mem_range_PolarizationIn P S j

Premises used: Submodule.sum_smul_mem, Set.Mem, LinearMap.range, RootPairing.PolarizationIn, RootPairing.prod_rootFormIn_smul_coroot_mem_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 : 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 N
this : IsTorsionFree S N
h_ne :
  Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0
x : N
hx : Membership.mem (γ := Submodule S N) (P.corootSpan S) x
c : ι → S
hc : ∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N) = x
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (∑ x : ι,
      c x •
        HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
          (∏ i : ι,
            (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                  LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
                (a : ↥(P.rootSpan S)) → S)
              (P.rootSpanMem S i))
          ((P.coroot : (a : ι) → N) x : N))

Tactic:
exact Submodule.sum_smul_mem (LinearMap.range (P.PolarizationIn S)) c
    fun j _ ↦ prod_rootFormIn_smul_coroot_mem_range_PolarizationIn P S j

Premises used: Submodule.sum_smul_mem, LinearMap.range, RootPairing.PolarizationIn, RootPairing.prod_rootFormIn_smul_coroot_mem_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 : 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
rw :
  finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) ≤
    finrank.{u_5, u_3} S ↥(P.rootSpan S)
⊢ finrank.{u_5, u_4} S ↥(P.corootSpan S) ≤ finrank.{u_5, u_3} S ↥(P.rootSpan S)

Tactic:
rw [← finrank_range_polarization_eq_finrank_span_coroot]

Premises used: RootPairing.finrank_range_polarization_eq_finrank_span_coroot
-- 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
⊢ finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) ≤
    finrank.{u_5, u_3} S ↥(P.rootSpan S)

Tactic:
LinearMap.finrank_range_le (P.PolarizationIn S)

Premises used: RootPairing.PolarizationIn, LinearMap.finrank_range_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 : 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
⊢ finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) ≤
    finrank.{u_5, u_3} S ↥(P.rootSpan S)

Tactic:
exact LinearMap.finrank_range_le (P.PolarizationIn S)

Premises used: RootPairing.PolarizationIn, LinearMap.finrank_range_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 : 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
⊢ finrank.{u_5, u_4} S ↥(P.corootSpan S) = finrank.{u_5, u_3} S ↥(P.rootSpan S)

Tactic:
le_antisymm (P.finrank_corootSpan_le S) (P.flip.finrank_corootSpan_le S)

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 : 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
⊢ 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 : 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 : IsReflexive R M
⊢ IsTorsionFree S M

Tactic:
have : Module.IsTorsionFree S M := .trans_faithfulSMul S R M
-- 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
rw : Disjoint (α := Submodule S ↥(P.rootSpan S)) ⊤ (LinearMap.ker (P.PolarizationIn S))
⊢ Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)

Tactic:
rw [← LinearMap.ker_eq_bot, ← top_disjoint]

Premises used: LinearMap.ker_eq_bot, top_disjoint
-- 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
⊢ Disjoint (α := Submodule S ↥(P.rootSpan S)) ⊤ (LinearMap.ker (P.PolarizationIn S))

Tactic:
Submodule.disjoint_ker_of_finrank_le (L := ⊤) (P.PolarizationIn S) ?_

Premises used: RootPairing.PolarizationIn, Submodule.disjoint_ker_of_finrank_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 : 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
refine : finrank.{u_5, u_3} S ↥⊤ ≤ finrank.{u_5, u_4} S ↥(Submodule.map (M := ↥(P.rootSpan S)) (P.PolarizationIn S) ⊤)
⊢ Disjoint (α := Submodule S ↥(P.rootSpan S)) ⊤ (LinearMap.ker (P.PolarizationIn S))

Tactic:
refine Submodule.disjoint_ker_of_finrank_le (L := ⊤) (P.PolarizationIn S) ?_

Premises used: RootPairing.PolarizationIn, Submodule.disjoint_ker_of_finrank_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 : 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
rw :
  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) ⊤)
⊢ finrank.{u_5, u_3} S ↥⊤ ≤ finrank.{u_5, u_4} S ↥(Submodule.map (M := ↥(P.rootSpan S)) (P.PolarizationIn S) ⊤)

Tactic:
rw [finrank_top, ← finrank_corootSpan_eq, ← finrank_range_polarization_eq_finrank_span_coroot]

Premises used: RootPairing.finrank_range_polarization_eq_finrank_span_coroot, finrank_top, RootPairing.finrank_corootSpan_eq