awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h :
  Membership.mem (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    x
hαx : x ∈ (↑(Weight.ker (M := L) (χ := α)) : Set ↥H)
hx : x ∈ (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) : Set ↥H)
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)

Tactic:
simpa using hαx
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h :
  Membership.mem (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    x
hαx : x ∈ (↑(Weight.ker (M := L) (χ := α)) : Set ↥H)
hx : x ∈ (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) : Set ↥H)
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)

Tactic:
replace hαx : α x = 0 := by simpa using hαx
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h :
  Membership.mem (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    x
hx : x ∈ (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) : Set ↥H)
hαx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
⊢ x = 0

Tactic:
eq_zero_of_apply_eq_zero_of_mem_corootSpace x α hαx hx

Premises used: LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h :
  Membership.mem (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    x
hx : x ∈ (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) : Set ↥H)
hαx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
⊢ x = 0

Tactic:
exact eq_zero_of_apply_eq_zero_of_mem_corootSpace x α hαx hx

Premises used: LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contrapose :
  ∀
    (hα :
      Eq.{u_2 + 1} (α := K)
        ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
        (0 : K)),
    α.IsZero
⊢ Ne.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)

Tactic:
contrapose hα
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα :
  Eq.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)
this :
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H) ⊥
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this

Premises used: LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, Disjoint.eq_bot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα :
  Eq.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)
this :
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H) ⊥
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ α.IsZero

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα :
  Eq.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)
suffices :
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ α.IsZero

Tactic:
suffices (cartanEquivDual H).symm α ∈ α.ker ⊓ corootSpace α by
    rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
    simpa using this
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα :
  Eq.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
Submodule.mem_inf.mp ⟨hα, cartanEquivDual_symm_apply_mem_corootSpace α⟩

Premises used: Set.Mem, setOf, Set.inter, Submodule.mem_inf, And.intro, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα :
  Eq.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
exact Submodule.mem_inf.mp ⟨hα, cartanEquivDual_symm_apply_mem_corootSpace α⟩

Premises used: Submodule.mem_inf, And.intro, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
rw : Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K) (2 : K)
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) (2 : K)

Tactic:
rw [← Weight.coe_coe]

Premises used: LieModule.Weight.coe_coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K) (2 : K)

Tactic:
simpa [coroot] using inv_mul_cancel₀ (root_apply_cartanEquivDual_symm_ne_zero hα)

Premises used: LieAlgebra.IsKilling.coroot, LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
⊢ coroot α = 0 ↔ α.IsZero

Tactic:
⟨fun hα ↦ ?_, fun hα ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
refine_1 : ∀ (hα : coroot α = 0), α.IsZero
refine_2 : ∀ (hα : α.IsZero), coroot α = 0
⊢ coroot α = 0 ↔ α.IsZero

Tactic:
refine ⟨fun hα ↦ ?_, fun hα ↦ ?_⟩
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : coroot α = 0
refine_1 : ∀ (contra : ¬α.IsZero), False
⊢ α.IsZero

Tactic:
by_contra contra
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : coroot α = 0
contra : ¬α.IsZero
⊢ False

Tactic:
simpa [hα, ← α.coe_coe, map_zero] using root_apply_coroot contra

Premises used: LieModule.Weight.coe_coe, map_zero, LieAlgebra.IsKilling.root_apply_coroot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
⊢ coroot α = 0

Tactic:
simp [coroot, Weight.coe_toLinear_eq_zero_iff.mpr hα]

Premises used: Iff.mpr, LieAlgebra.IsKilling.coroot, LieModule.Weight.coe_toLinear_eq_zero_iff
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
inst_8 : Nontrivial L
⊢ Eq.{u_3 + 1} (α := ↥H) (coroot 0) 0

Tactic:
simp [Weight.isZero_zero]

Premises used: LieModule.Weight.isZero_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)

Tactic:
simp [hα.eq, coroot_eq_zero_iff.mpr hα]

Premises used: Iff.mpr, LieModule.Weight.IsZero.eq, LieAlgebra.IsKilling.coroot_eq_zero_iff
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
this : Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
rw :
  Eq (α := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (K ∙ coroot α)
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)

Tactic:
rw [coe_corootSpace_eq_span_singleton']

Premises used: LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
this : Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
⊢ Eq (α := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (K ∙ coroot α)

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
this : Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
⊢ Eq (α := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (K ∙ coroot α)

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
suffices : Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)

Tactic:
suffices (K ∙ coroot α) = K ∙ α' by rw [coe_corootSpace_eq_span_singleton']; exact this.symm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ IsUnit (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) α')⁻¹ : K))

Tactic:
simpa using root_apply_cartanEquivDual_symm_ne_zero hα

Premises used: LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ IsUnit (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) α')⁻¹ : K))

Tactic:
have : IsUnit (2 * (α α')⁻¹) := by simpa using root_apply_cartanEquivDual_symm_ne_zero hα
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
this : IsUnit (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) α')⁻¹ : K))
change :
  Eq (α := Submodule K ↥H)
    (K ∙ HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (((α : (a : ↥H) → K) α')⁻¹ : K) α')) (K ∙ α')
⊢ Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')

Tactic:
change (K ∙ (2 • (α α')⁻¹ • α')) = _

Premises used: Inv.inv, Submodule.span, HSMul.hSMul, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
this : IsUnit (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) α')⁻¹ : K))
⊢ Eq (α := Submodule K ↥H)
    (K ∙ HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (((α : (a : ↥H) → K) α')⁻¹ : K) α')) (K ∙ α')

Tactic:
simpa [← Nat.cast_smul_eq_nsmul K, smul_smul] using Submodule.span_singleton_smul_eq this _

Premises used: smul_smul, Submodule.span_singleton_smul_eq, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
if : ∀ (hα : α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
if₁ : ∀ (hα : ¬α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
if₂ : ∀ (hα : α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
if₃ if₄ :
  ∀ (hα : ¬α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)

Tactic:
if hα : α.IsZero then
    simp [hα.eq, coroot_eq_zero_iff.mpr hα]
  else
    set α' := (cartanEquivDual H).symm α
    suffices (K ∙ coroot α) = K ∙ α' by rw [coe_corootSpace_eq_span_singleton']; exact this.symm
    have : IsUnit (2 * (α α')⁻¹) := by simpa using root_apply_cartanEquivDual_symm_ne_zero hα
    change (K ∙ (2 • (α α')⁻¹ • α')) = _
    simpa [← Nat.cast_smul_eq_nsmul K, smul_smul] using Submodule.span_singleton_smul_eq this _

Premises used: LinearEquiv.symm, Membership.mem, smul_smul, LieModule.Weight.IsZero, Subtype, Nat.cast_smul_eq_nsmul, LieModule.Weight.toLinear, LieAlgebra.IsKilling.cartanEquivDual, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
pos : ∀ (h₀ : α.IsZero), x = coroot α
neg : ∀ (h₀ : ¬α.IsZero), x = coroot α
⊢ x = coroot α

Tactic:
by_cases h₀ : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : α.IsZero
⊢ x = coroot α

Tactic:
simp [h₀.eq] at h_two

Premises used: LieModule.Weight.IsZero.eq
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : ¬α.IsZero
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) x
⊢ Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) x

Tactic:
rwa [← coe_corootSpace_eq_span_singleton]

Premises used: LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : ¬α.IsZero
⊢ Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) x

Tactic:
replace h_mem : x ∈ K ∙ coroot α := by rwa [← coe_corootSpace_eq_span_singleton]
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x : ↥H
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : ¬α.IsZero
h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) x
neg :
  ∀ (t : K) (h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (t • coroot α) : K) (2 : K))
    (h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) (t • coroot α)), t • coroot α = coroot α
⊢ x = coroot α

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp h_mem

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl