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 : 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
have refine : ∀ (i : ι),
  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)),
      False
Tactic: refine Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_
-- 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 : 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
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)
⊢ False
have this₁ : Eq.{u_2 + 1} (α := R)
  ((algebraMap S R : (a : S) → R)
      ((((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) :
    R)
  (0 : R)
Tactic: have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h
-- 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 : 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)
    ((algebraMap S R : (a : S) → R)
        ((((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) :
      R)
    (0 : R)
⊢ False
have 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)
Tactic: rw [algebraMap_rootFormIn] at this
Cleared hypotheses: this
-- 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 : 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
⊢ finrank.{u_5, u_4} S ↥(P.corootSpan S) ≤
    finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
have 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
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
-- 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 : 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))
have 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)
Tactic: refine LinearMap.finrank_le_of_isSMulRegular (P.corootSpan S)
    (LinearMap.range (M₂ := N) (P.PolarizationIn S))
    (smul_right_injective N h_ne) ?_
-- 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 : 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
⊢ 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)
have 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)
Tactic: obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun S).mp 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 : 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))
    (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)
have 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)))
Tactic: rw [← hc, Finset.smul_sum]
-- 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 : 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 : ι,
      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)))
have 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))
Tactic: simp_rw [smul_smul, mul_comm, ← smul_smul]
-- 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 : 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)
have 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)
Tactic: rw [← finrank_range_polarization_eq_finrank_span_coroot]
-- 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 : 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
⊢ Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
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 : 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
⊢ Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
have this₁ : IsTorsionFree S M
Tactic: have : Module.IsTorsionFree S M := .trans_faithfulSMul S R M
-- 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 : 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
⊢ Injective.{u_3 + 1, u_4 + 1} (α := ↥(P.rootSpan S)) (β := N) (⇑(P.PolarizationIn S) : (a : ↥(P.rootSpan S)) → N)
have rw : Disjoint (α := Submodule S ↥(P.rootSpan S)) ⊤ (LinearMap.ker (P.PolarizationIn S))
Tactic: rw [← LinearMap.ker_eq_bot, ← top_disjoint]
-- 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 : 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))
have refine : finrank.{u_5, u_3} S ↥⊤ ≤ finrank.{u_5, u_4} S ↥(Submodule.map (M := ↥(P.rootSpan S)) (P.PolarizationIn S) ⊤)
Tactic: refine Submodule.disjoint_ker_of_finrank_le (L := ⊤) (P.PolarizationIn 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 : 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_3} S ↥⊤ ≤ finrank.{u_5, u_4} S ↥(Submodule.map (M := ↥(P.rootSpan S)) (P.PolarizationIn S) ⊤)
have 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) ⊤)
Tactic: rw [finrank_top, ← finrank_corootSpan_eq, ← finrank_range_polarization_eq_finrank_span_coroot]
-- 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 : 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
⊢ ∃ (i : ι), Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
have hI : 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
-- 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 : 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)
⊢ ∃ (i : ι), Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
have h : 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
-- 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 : 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)
⊢ ∃ (i : ι), Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
have 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
Tactic: rw [PolarizationIn_apply] at h
Cleared hypotheses: h
-- 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 : 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
⊢ ∃ (i : ι), Ne.{u_5 + 1} (α := S) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) (0 : S)
have 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
Tactic: contrapose! h
Cleared hypotheses: h