awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
this :
  Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (b.h' i)
_i : IsAddTorsionFree L
⊢ Eq.{u_2 + 1} (α := K)
    ((((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
            Weight K (↥b.cartan) L) :
          (a : ↥b.cartan) → K)
        (b.h' i) :
      K)
    (2 : K)

Tactic:
simp [baseSupp']

Premises used: LieAlgebra.Basis.baseSupp'
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
this :
  Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (b.h' i)
_i : IsAddTorsionFree L
⊢ coroot (↑(↑((b.baseSupportEquiv : (a : ι) → ↥b.base.support) i) : ↥root) : Weight K (↥b.cartan) L) = b.h' i

Tactic:
exact (eq_coroot_of_mem_corootSpace_of_two (b.baseSupp' i).val this (by simp [baseSupp'])).symm

Premises used: LieAlgebra.Basis.baseSupp', LieAlgebra.IsKilling.eq_coroot_of_mem_corootSpace_of_two, Eq.symm, Subtype.val
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
suffices :
  Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (b.h' i)
⊢ coroot (↑(↑((b.baseSupportEquiv : (a : ι) → ↥b.base.support) i) : ↥root) : Weight K (↥b.cartan) L) = b.h' i

Tactic:
suffices b.h' i ∈ corootSpace (b.baseSupp' i) by
    have _i : IsAddTorsionFree L := .of_isTorsionFree K L
    exact (eq_coroot_of_mem_corootSpace_of_two (b.baseSupp' i).val this (by simp [baseSupp'])).symm
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
rw : Membership.mem (γ := LieSubalgebra K L) (lieSpan K L (range b.h)) (b.h i)
⊢ ⁅b.e i, b.f i⁆ ∈ b.cartan

Tactic:
rw [(b.sl2 i).lie_e_f, b.cartan_eq_lieSpan]

Premises used: LieAlgebra.Basis.sl2, LieAlgebra.Basis.cartan_eq_lieSpan, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
⊢ Membership.mem (γ := LieSubalgebra K L) (lieSpan K L (range b.h)) (b.h i)

Tactic:
subset_lieSpan <| mem_range_self i

Premises used: Set.mem_range_self, LieSubalgebra.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
⊢ Membership.mem (γ := LieSubalgebra K L) (lieSpan K L (range b.h)) (b.h i)

Tactic:
exact subset_lieSpan <| mem_range_self i

Premises used: Set.mem_range_self, LieSubalgebra.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
⊢ ⁅b.e i, b.f i⁆ ∈ b.cartan

Tactic:
have h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan := by
    rw [(b.sl2 i).lie_e_f, b.cartan_eq_lieSpan]
    exact subset_lieSpan <| mem_range_self i
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
⊢ b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem

Tactic:
simp [(b.sl2 i).lie_e_f, h']

Premises used: LieAlgebra.Basis.h', LieAlgebra.Basis.sl2, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
⊢ b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem

Tactic:
have h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩ := by simp [(b.sl2 i).lie_e_f, h']
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
rw :
  Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem)
⊢ Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (b.h' i)

Tactic:
rw [h_eq]
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
x : ↥b.cartan
z : L
hz : z ∈ b.cartan
⊢ Eq (α := L)
    ((HPow.hPow (β := ℕ)
            (HSub.hSub (α := End K L)
              ((toEnd K (↥b.cartan) L : (a : ↥b.cartan) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) z hz) :
                End K L)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := End K L)
                ((b.baseSupp i : (a : ↥b.cartan) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) z hz) : K) 1))
            1 :
          (a : L) → L)
        (b.e i) :
      L)
    (0 : L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
⊢ b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)

Tactic:
have he : b.e i ∈ rootSpace b.cartan (b.baseSupp i) :=
    (mem_genWeightSpace _ _ _).mpr fun ⟨z, hz⟩ ↦ ⟨1, by simp⟩
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
he : b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)
x : ↥b.cartan
z : L
hz : z ∈ b.cartan
⊢ Eq (α := L)
    ((HPow.hPow (β := ℕ)
            (HSub.hSub (α := End K L)
              ((toEnd K (↥b.cartan) L : (a : ↥b.cartan) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) z hz) :
                End K L)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := End K L)
                ((-(⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) z hz) : K) 1))
            1 :
          (a : L) → L)
        (b.f i) :
      L)
    (0 : L)

Tactic:
simp [← eq_neg_iff_add_eq_zero]

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
he : b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)
⊢ b.f i ∈ rootSpace b.cartan (-(⇑(b.baseSupp i) : (a : ↥b.cartan) → K))

Tactic:
have hf : b.f i ∈ rootSpace b.cartan (-b.baseSupp i) :=
    (mem_genWeightSpace _ _ _).mpr fun ⟨z, hz⟩ ↦ ⟨1, by simp [← eq_neg_iff_add_eq_zero]⟩
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
he : b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)
hf : b.f i ∈ rootSpace b.cartan (-(⇑(b.baseSupp i) : (a : ↥b.cartan) → K))
⊢ Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem)

Tactic:
(mem_corootSpace _).mpr <| Submodule.subset_span ⟨b.e i, he, b.f i, hf, rfl⟩

Premises used: Iff.mpr, LieAlgebra.Basis.e, LieAlgebra.Basis.f, And.intro, Exists.intro, Submodule.subset_span, LieAlgebra.mem_corootSpace, rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
he : b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)
hf : b.f i ∈ rootSpace b.cartan (-(⇑(b.baseSupp i) : (a : ↥b.cartan) → K))
⊢ Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem)

Tactic:
exact (mem_corootSpace _).mpr <| Submodule.subset_span ⟨b.e i, he, b.f i, hf, rfl⟩

Premises used: Iff.mpr, LieAlgebra.mem_corootSpace
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
a :
  ∀ (i j : ι),
    (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
          (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
        (RootPairing.Base.cartanMatrix b.base) i j =
      b.A i j
⊢ (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
        (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
      (RootPairing.Base.cartanMatrix b.base) =
    b.A

Tactic:
ext i j
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i j : ι
a :
  Eq (α := K)
    ((algebraMap ℤ K : (a : ℤ) → K)
        ((reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
              (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
            (RootPairing.Base.cartanMatrix b.base) i j :
          ℤ) :
      K)
    ((algebraMap ℤ K : (a : ℤ) → K) (b.A i j) : K)
⊢ (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
        (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
      (RootPairing.Base.cartanMatrix b.base) i j =
    b.A i j

Tactic:
apply FaithfulSMul.algebraMap_injective ℤ K

Premises used: Int, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i j : ι
a :
  RootPairing.pairing (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)
      (↑((Equiv.symm (Equiv.symm b.baseSupportEquiv) : (a : ι) → ↥b.base.support) i) : ↥root)
      (↑((Equiv.symm (Equiv.symm b.baseSupportEquiv) : (a : ι) → ↥b.base.support) j) : ↥root) =
    (algebraMap ℤ K : (a : ℤ) → K) (b.A i j)
⊢ Eq (α := K)
    ((algebraMap ℤ K : (a : ℤ) → K)
        ((reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
              (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
            (RootPairing.Base.cartanMatrix b.base) i j :
          ℤ) :
      K)
    ((algebraMap ℤ K : (a : ℤ) → K) (b.A i j) : K)

Tactic:
rw [reindex_apply, submatrix_apply, RootPairing.Base.algebraMap_cartanMatrixIn_apply]

Premises used: RootPairing.Base.algebraMap_cartanMatrixIn_apply, Matrix.reindex_apply, Matrix.submatrix_apply
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i j : ι
⊢ RootPairing.pairing (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)
      (↑((Equiv.symm (Equiv.symm b.baseSupportEquiv) : (a : ι) → ↥b.base.support) i) : ↥root)
      (↑((Equiv.symm (Equiv.symm b.baseSupportEquiv) : (a : ι) → ↥b.base.support) j) : ↥root) =
    (algebraMap ℤ K : (a : ℤ) → K) (b.A i j)

Tactic:
simp [← Weight.coe_coe]

Premises used: LieModule.Weight.coe_coe
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
this :
  ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
    HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.2) ⋯) : R) :
          K) =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.2) ⋯) : R) : K)
obtain :
  ∀ (r : K[X])
    (hr :
      ∀ (i : ι × ι),
        Polynomial.eval (a i.1 - a i.2) r =
          HSub.hSub (α := K) (β := K)
            ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.1) ⋯) : R) :
              K)
            ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.2) ⋯) : R) :
              K)),
    ∃ (r : K[X]),
      ∀ (i j : ι),
        Polynomial.eval (a i - a j) r =
          HSub.hSub (α := K) (β := K)
            ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) :
              K)
            ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) :
              K)
⊢ ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) : K)

Tactic:
obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this

Premises used: Iff.mpr, Polynomial.exists_eval_eq_iff
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
this :
  ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
    HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.2) ⋯) : R) :
          K) =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.2) ⋯) : R) : K)
r : K[X]
hr :
  ∀ (i : ι × ι),
    Polynomial.eval (a i.1 - a i.2) r =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.2) ⋯) : R) : K)
⊢ ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) : K)

Tactic:
⟨r, fun i j ↦ hr (i, j)⟩

Premises used: Prod.mk, Exists.intro
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
this :
  ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
    HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.2) ⋯) : R) :
          K) =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.2) ⋯) : R) : K)
r : K[X]
hr :
  ∀ (i : ι × ι),
    Polynomial.eval (a i.1 - a i.2) r =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.2) ⋯) : R) : K)
⊢ ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) : K)

Tactic:
exact ⟨r, fun i j ↦ hr (i, j)⟩
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
suffices :
  ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
    HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.2) ⋯) : R) :
          K) =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.2) ⋯) : R) : K)
⊢ ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) : K)

Tactic:
suffices ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
      algebraMap R K (f ⟨a ij.1, ha ij.1⟩) - algebraMap R K (f ⟨a ij.2, ha ij.2⟩) =
      algebraMap R K (f ⟨a kl.1, ha kl.1⟩) - algebraMap R K (f ⟨a kl.2, ha kl.2⟩) by
    obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this
    exact ⟨r, fun i j ↦ hr (i, j)⟩
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
⊢ Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯ =
    Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a k) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a l) ⋯

Tactic:
have heq : (⟨a i, ha i⟩ - ⟨a j, ha j⟩ : E) = ⟨a k, ha k⟩ - ⟨a l, ha l⟩ := Subtype.ext hij