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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
i : ι
h₀ :
  Ne.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)
rw :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
⊢ (P.coroot : (a : ι) → N) i =
    HSMul.hSMul (β := N)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)

Tactic:
rw [polarizationEquiv_apply, ← (smul_right_injective N h₀).eq_iff, P.rootForm_self_smul_coroot i,
    smul_smul, mul_div_cancel₀ _ h₀]

Premises used: RootPairing.rootForm_self_smul_coroot, Function.Injective.eq_iff, smul_smul, smul_right_injective, RootPairing.polarizationEquiv_apply, mul_div_cancel₀
-- 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
inst_7 : P.IsRootSystem
i : ι
h₀ :
  Ne.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)

Tactic:
norm_cast
-- 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
inst_7 : P.IsRootSystem
i : ι
⊢ (P.PolarizationEquiv.symm : (a : N) → M) ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.root : (a : ι) → M) i : M)

Tactic:
simp [coroot_eq_polarizationEquiv_apply_root]

Premises used: RootPairing.coroot_eq_polarizationEquiv_apply_root
-- 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
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
i : (↑s : Type u_1)
⊢ HDiv.hDiv (α := R) (β := R) (2 : R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑i : ι)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (↑i : ι) : M) :
        R) ≠
    0

Tactic:
simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]

Premises used: RootPairing.IsAnisotropic.rootForm_root_ne_zero, two_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 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
i : (↑s : Type u_1)
⊢ (P.coroot : (a : ι) → N) (↑i : ι) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := Rˣ) (β := N)
      ((fun (i : (↑s : Type u_1)) ↦
          (Units.mk0
              (HDiv.hDiv (α := R) (β := R) (2 : R)
                ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑i : ι)) : M →ₗ[R] R) : (a : M) → R)
                    ((P.root : (a : ι) → M) (↑i : ι) : M) :
                  R))
              ⋯ :
            Rˣ))
        i)
      ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)

Tactic:
simp [coroot_eq_polarizationEquiv_apply_root]

Premises used: RootPairing.coroot_eq_polarizationEquiv_apply_root
-- 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
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
obtain :
  ∀ (f : (↑s : Type u_1) → Rˣ)
    (hf :
      ∀ (i : (↑s : Type u_1)),
        (P.coroot : (a : ι) → N) (↑i : ι) =
          HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)),
    LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s

Tactic:
obtain ⟨f, hf⟩ : ∃ f : s → Rˣ, ∀ i : s, P.coroot i = f i • P.PolarizationEquiv (P.root i) :=
    ⟨fun i ↦ Units.mk0 (2 / P.RootForm (P.root i) (P.root i))
      (by simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]),
     fun i ↦ by simp [coroot_eq_polarizationEquiv_apply_root]⟩
-- 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
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
h₁ :
  ∀ (x : (↑s : Type u_1)),
    Eq.{u_4 + 1} (α := N) (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) x : N)
      (((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
            HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
              (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M))
          x :
        N)
⊢ Eq (α := (a : (↑s : Type u_1)) → N)
    (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
    ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
        HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
          (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
      (↑s : Type u_1) → N)

Tactic:
ext
-- 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
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
x : (↑s : Type u_1)
⊢ Eq.{u_4 + 1} (α := N) (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) x : N)
    (((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
          HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
            (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M))
        x :
      N)

Tactic:
simp [hf, polarizationEquiv_apply]

Premises used: RootPairing.polarizationEquiv_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
⊢ Eq (α := (a : (↑s : Type u_1)) → N)
    (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
    ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
        HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
          (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
      (↑s : Type u_1) → N)

Tactic:
have : (s.restrict P.coroot) = P.PolarizationEquiv.toLinearMap ∘ (f • (s.restrict P.root)) := by
    ext; simp [hf, polarizationEquiv_apply]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
this :
  Eq (α := (a : (↑s : Type u_1)) → N)
    (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
    ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
        HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
          (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
      (↑s : Type u_1) → N)
rw :
  LinearIndependent R
    (HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
      (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M))
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s

Tactic:
rw [← linearIndependent_restrict_iff, this,
    LinearMap.linearIndependent_iff_of_injOn _ P.PolarizationEquiv.injective.injOn]

Premises used: Function.Injective.injOn, linearIndependent_restrict_iff, RootPairing.PolarizationEquiv, LinearMap.linearIndependent_iff_of_injOn, LinearEquiv.injective
-- 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
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
this :
  Eq (α := (a : (↑s : Type u_1)) → N)
    (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
    ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
        HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
          (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
      (↑s : Type u_1) → N)
⊢ LinearIndependent R
    (HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
      (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M))

Tactic:
simpa
-- 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
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s ↔
    LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s

Tactic:
⟨P.flip.linearIndepOn_coroot_iff_aux, P.linearIndepOn_coroot_iff_aux⟩

Premises used: _private.0.RootPairing.linearIndepOn_coroot_iff_aux, RootPairing.flip, Iff.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 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
⊢ P.IsAnisotropic

Tactic:
P.isAnisotropic_of_isValuedIn R

Premises used: RootPairing.isAnisotropic_of_isValuedIn
-- 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 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
⊢ LE.le.{u_2} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
(P.rootForm_self_sum_of_squares x).nonneg

Premises used: RootPairing.rootForm_self_sum_of_squares, IsSumSq.nonneg
-- 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 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
⊢ LinearMap.Nondegenerate (M₁ := ↥(P.rootSpan R)) (P.RootForm.restrict (P.rootSpan R))

Tactic:
(P.RootForm.nondegenerate_restrict_iff_disjoint_ker P.zero_le_rootForm
    P.rootForm_symmetric).mpr P.disjoint_rootSpan_ker_rootForm

Premises used: Iff.mpr, RootPairing.RootForm, RootPairing.zero_le_rootForm, LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker, LinearMap.BilinForm.restrict, RootPairing.disjoint_rootSpan_ker_rootForm, 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 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
⊢ Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ↔
    x ∈ LinearMap.ker P.RootForm

Tactic:
P.RootForm.apply_apply_same_eq_zero_iff P.zero_le_rootForm P.rootForm_symmetric

Premises used: RootPairing.RootForm, RootPairing.zero_le_rootForm, LinearMap.BilinForm.apply_apply_same_eq_zero_iff, 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 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
hx' : Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm

Tactic:
have : x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm := ⟨hx, P.rootForm_self_eq_zero_iff.mp hx'⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
hx' : Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
this : x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm
⊢ x = 0

Tactic:
simpa [P.disjoint_rootSpan_ker_rootForm.eq_bot] using this

Premises used: RootPairing.disjoint_rootSpan_ker_rootForm, Disjoint.eq_bot
-- 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 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
h : x ≠ 0
apply : Ne.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ LT.lt.{u_2} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
apply (P.zero_le_rootForm x).lt_of_ne

Premises used: RootPairing.zero_le_rootForm, LE.le.lt_of_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 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
h : x ≠ 0
contrapose :
  ∀ (h : Eq.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)),
    x = 0
⊢ Ne.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
contrapose h
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
h : Eq.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ x = 0

Tactic:
P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero hx h.symm

Premises used: RootPairing.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero, 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 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
h : Eq.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ x = 0

Tactic:
exact P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero hx h.symm

Premises used: RootPairing.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero, 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 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
x : M
⊢ Membership.mem (γ := Submodule R M) (P.rootSpan R) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : DecidableEq ι
i : ↥b.support
a :
  ∀ (j k : ↥b.support),
    h i (Sum.inl j) (Sum.inl k) =
      Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j)
        (Sum.inl k)
a₁ :
  ∀ (j : ↥b.support) (k : ι),
    h i (Sum.inl j) (Sum.inr k) =
      Matrix.fromBlocks (l := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
        (Sum.inl j) (Sum.inr k)
a₂ :
  ∀ (j : ι) (k : ↥b.support),
    h i (Sum.inr j) (Sum.inl k) =
      Matrix.fromBlocks (n := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
        (Sum.inr j) (Sum.inl k)
a₃ :
  ∀ (j k : ι),
    h i (Sum.inr j) (Sum.inr k) =
      Matrix.fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0
        (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j) (Sum.inr k)
⊢ h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))

Tactic:
ext (j | j) (k | k)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : DecidableEq ι
i j k : ↥b.support
⊢ h i (Sum.inl j) (Sum.inl k) =
    Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j)
      (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : DecidableEq ι
i j : ↥b.support
k : ι
⊢ h i (Sum.inl j) (Sum.inr k) =
    Matrix.fromBlocks (l := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
      (Sum.inl j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : DecidableEq ι
i : ↥b.support
j : ι
k : ↥b.support
⊢ h i (Sum.inr j) (Sum.inl k) =
    Matrix.fromBlocks (n := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
      (Sum.inr j) (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : DecidableEq ι
i : ↥b.support
j k : ι
⊢ h i (Sum.inr j) (Sum.inr k) =
    Matrix.fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0
      (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply