awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    D
⊢ Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))

Tactic:
simp [← (ad_isIdealMorphism R L).eq]

Premises used: LieHom.IsIdealMorphism.eq, LieDerivation.ad_isIdealMorphism
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    D
⊢ Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))

Tactic:
have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by simp [← (ad_isIdealMorphism R L).eq]
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    D
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D

Tactic:
change D ∈ 𝕀ᗮ at hD
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
rw :
  ∀
    (hD :
      Membership.mem (γ := Submodule R (LieDerivation R L L))
        (LieSubalgebra.toSubmodule
          (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
            (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
        D),
    Membership.mem (γ := Submodule R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule
        (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
          (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
      ⁅x, D⁆
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ⁅x, D⁆

Tactic:
rw [this] at hD ⊢
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    D
rw :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    (Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D)
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    ⁅x, D⁆

Tactic:
rw [← lie_ad]

Premises used: LieDerivation.lie_ad
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    D
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    (Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D)

Tactic:
lie_mem_right _ _ (ad R L).idealRange.killingCompl _ _ hD

Premises used: Set.Mem, setOf, LieIdeal.killingCompl, LieDerivation.ad, LieHom.idealRange, lie_mem_right
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    D
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    (Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D)

Tactic:
exact lie_mem_right _ _ (ad R L).idealRange.killingCompl _ _ hD

Premises used: LieIdeal.killingCompl, LieDerivation.ad, LieHom.idealRange, lie_mem_right
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
simp :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LinearMap.range (↑(ad R L) : L →ₗ[R] LieDerivation R L L)))
    ⁅x, D⁆
⊢ Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)

Tactic:
simp only [ad_apply_lieDerivation, LieHom.range_toSubmodule, neg_mem_iff]

Premises used: LieDerivation.ad_apply_lieDerivation, neg_mem_iff, LieHom.range_toSubmodule
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LinearMap.range (↑(ad R L) : L →ₗ[R] LieDerivation R L L)))
    ⁅x, D⁆

Tactic:
(rangeAdOrthogonal R L).lie_mem hD

Premises used: LieDerivation.IsKilling.rangeAdOrthogonal, Set.Mem, setOf, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LinearMap.range (↑(ad R L) : L →ₗ[R] LieDerivation R L L)))
    ⁅x, D⁆

Tactic:
exact (rangeAdOrthogonal R L).lie_mem hD

Premises used: LieDerivation.IsKilling.rangeAdOrthogonal, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
rw :
  Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
    (Submodule.map (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (Submodule.subtype (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (LinearMap.ker
        (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
          (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
⊢ Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
    (Submodule.map (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (Submodule.subtype (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (LinearMap.ker (killingForm R ↥(LieHom.range (ad R L)))))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)

Tactic:
rw [← killingForm_restrict_range_ad]

Premises used: LieDerivation.IsKilling.killingForm_restrict_range_ad
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Membership.mem (α := LieDerivation R L L)
    (↑(LieSubalgebra.toSubmodule (LieHom.range (ad R L))) : Set (LieDerivation R L L))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
    (Submodule.map (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (Submodule.subtype (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (LinearMap.ker
        (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
          (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)

Tactic:
exact LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl ⟨by simp, ad_mem_orthogonal_of_mem_orthogonal hD x⟩
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
h : x = 0
⊢ Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
refine :
  ∀
    (h :
      Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
        (0 : LieDerivation R L L)),
    x = 0
⊢ Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
      (0 : LieDerivation R L L) ↔
    x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
h :
  Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L)
rwa : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieHom.ker (ad R L)) x), x = 0
rwa₁ : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x), x = 0
rwa₂ : ∀ (h : Membership.mem (γ := LieIdeal R L) ⊥ x), x = 0
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : x = 0), x = 0
⊢ x = 0

Tactic:
rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h

Premises used: LieSubmodule.mem_bot, LieAlgebra.center_eq_bot, LieHom.mem_ker, LieDerivation.ad_ker_eq_center
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ LinearMap.BilinForm.Nondegenerate.{u_1, u_2} (M := ↥(LieHom.range (ad R L))) (killingForm R ↥(LieHom.range (ad R L)))

Tactic:
LieAlgebra.IsKilling.killingForm_nondegenerate R 𝕀

Premises used: Membership.mem, LieHom.range, LieAlgebra.IsKilling.killingForm_nondegenerate, Subtype, LieDerivation.ad
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
h :
  ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))) = ↥(LieHom.range (ad R L)) →
    HEq (α := AddCommMonoid ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
        (Submodule.addCommMonoid (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
        AddCommMonoid ↥(LieHom.range (ad R L))) AddCommGroup.toAddCommMonoid →
      HEq (α := Module.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
          (Submodule.module (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
          Module.{u_1, u_2} R ↥(LieHom.range (ad R L))) LieAlgebra.toModule →
        Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
          (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
          (killingForm R ↥(LieHom.range (ad R L)))
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))

Tactic:
convert! LieAlgebra.IsKilling.killingForm_nondegenerate R 𝕀
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
e_2 : ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))) = ↥(LieHom.range (ad R L))
e_4 :
  HEq (α := AddCommMonoid ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (Submodule.addCommMonoid (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
    AddCommMonoid ↥(LieHom.range (ad R L))) AddCommGroup.toAddCommMonoid
e_5 :
  HEq (α := Module.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (Submodule.module (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
    Module.{u_1, u_2} R ↥(LieHom.range (ad R L))) LieAlgebra.toModule
⊢ Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (killingForm R ↥(LieHom.range (ad R L)))

Tactic:
killingForm_restrict_range_ad R L

Premises used: LieDerivation.IsKilling.killingForm_restrict_range_ad
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
e_2 : ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))) = ↥(LieHom.range (ad R L))
e_4 :
  HEq (α := AddCommMonoid ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (Submodule.addCommMonoid (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
    AddCommMonoid ↥(LieHom.range (ad R L))) AddCommGroup.toAddCommMonoid
e_5 :
  HEq (α := Module.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (Submodule.module (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
    Module.{u_1, u_2} R ↥(LieHom.range (ad R L))) LieAlgebra.toModule
⊢ Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (killingForm R ↥(LieHom.range (ad R L)))

Tactic:
exact killingForm_restrict_range_ad R L

Premises used: LieDerivation.IsKilling.killingForm_restrict_range_ad
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
rw :
  Eq (α := Submodule R (LieDerivation R L L)) (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))
    (LieSubalgebra.toSubmodule ⊤)
⊢ Eq (α := LieSubalgebra R (LieDerivation R L L)) (LieHom.range (ad R L)) ⊤

Tactic:
rw [← LieSubalgebra.toSubmodule_inj]

Premises used: LieSubalgebra.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
apply :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ⊥
⊢ Eq (α := Submodule R (LieDerivation R L L)) (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))
    (LieSubalgebra.toSubmodule ⊤)

Tactic:
apply LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl (killingForm_restrict_range_ad_nondegenerate R L)
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ⊥

Tactic:
(Submodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_

Premises used: Iff.mpr, LieDerivation.ext, Submodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
refine :
  ∀ (D : LieDerivation R L L)
    (hD :
      Membership.mem (γ := Submodule R (LieDerivation R L L))
        (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
          (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
        D)
    (x : L), Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)
⊢ Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ⊥

Tactic:
refine (Submodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_

Premises used: Iff.mpr, LieDerivation.ext, Submodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)

Tactic:
simpa using ad_mem_ker_killingForm_ad_range_of_mem_orthogonal hD x

Premises used: LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
D : LieDerivation R L L
rw : Membership.mem (γ := LieSubalgebra R (LieDerivation R L L)) ⊤ D
⊢ Membership.mem (γ := LieSubalgebra R (LieDerivation R L L)) (LieHom.range (ad R L)) D

Tactic:
rw [range_ad_eq_top R L]

Premises used: LieDerivation.IsKilling.range_ad_eq_top