awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (↑I : Submodule K L) (↑(orthogonal Φ hΦ_inv I) : Submodule K L)

Tactic:
orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Premises used: LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (↑I : Submodule K L) (↑(orthogonal Φ hΦ_inv I) : Submodule K L)

Tactic:
exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Premises used: LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
rw : IsCompl (LieIdeal.toLieSubalgebra K L I).toSubmodule (Φ.orthogonal (LieIdeal.toLieSubalgebra K L I).toSubmodule)
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(LieIdeal.toLieSubalgebra K L I).toSubmodule)
    (Φ.restrict (LieIdeal.toLieSubalgebra K L I).toSubmodule)

Tactic:
rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]

Premises used: LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L I).toSubmodule (Φ.orthogonal (LieIdeal.toLieSubalgebra K L I).toSubmodule)

Tactic:
orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Premises used: Set.Mem, setOf, Submodule.orthogonalBilin, LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, LinearMap.BilinForm.orthogonal
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L I).toSubmodule (Φ.orthogonal (LieIdeal.toLieSubalgebra K L I).toSubmodule)

Tactic:
exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Premises used: LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
rw :
  IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
    (Φ.restrict (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)

Tactic:
rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]

Premises used: LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
simp : IsCompl (Φ.orthogonal (↑I : Submodule K L)) (↑I : Submodule K L)
⊢ IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)

Tactic:
simp only [LieIdeal.toLieSubalgebra_toSubmodule, orthogonal_toSubmodule,
    LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl]

Premises used: LieIdeal.toLieSubalgebra_toSubmodule, LieAlgebra.InvariantForm.orthogonal_toSubmodule, LinearMap.BilinForm.orthogonal_orthogonal
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (Φ.orthogonal (↑I : Submodule K L)) (↑I : Submodule K L)

Tactic:
(orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI).symm

Premises used: Submodule.orthogonalBilin, LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, LinearMap.BilinForm.orthogonal, IsCompl.symm
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (Φ.orthogonal (↑I : Submodule K L)) (↑I : Submodule K L)

Tactic:
exact (orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI).symm

Premises used: LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, IsCompl.symm
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
a : sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} ≤ I
a₁ : I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
⊢ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
a : ∀ (b : LieIdeal K L), Membership.mem (γ := Set (LieIdeal K L)) {J : LieIdeal K L | IsAtom J ∧ J ≤ I} b → b ≤ I
⊢ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} ≤ I

Tactic:
apply sSup_le

Premises used: sSup_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I J : LieIdeal K L
hJ' : J ≤ I
⊢ J ≤ I

Tactic:
hJ'
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I J : LieIdeal K L
hJ' : J ≤ I
⊢ J ≤ I

Tactic:
exact hJ'
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
pos : ∀ (hI : I = ⊥), I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
neg : ∀ (hI : ¬I = ⊥), I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : I = ⊥
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
hI.le.trans bot_le

Premises used: Eq.le, LE.le.trans, bot_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : I = ⊥
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
exact hI.le.trans bot_le

Premises used: Eq.le, LE.le.trans, bot_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
neg : ∀ (J : LieIdeal K L) (hJ : IsAtom J) (hJI : J ≤ I), I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
obtain ⟨J, hJ, hJI⟩ := (eq_bot_or_exists_atom_le I).resolve_left hI

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Or.resolve_left
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
this.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
refine : J ⊔ J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
refine this.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
a : J ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
a₁ : J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
⊢ J ⊔ J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
apply sup_le

Premises used: sup_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ J ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
le_sSup ⟨hJ, hJI⟩

Premises used: Set.Mem, And.intro, le_sSup
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ J ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
exact le_sSup ⟨hJ, hJI⟩
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
a :
  LE.le.{u_2} (α := LieIdeal K L) (sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ J' ⊓ I})
    (sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I})
⊢ J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
rw [← atomistic (J' ⊓ I)]

Premises used: Min.min
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
a :
  Subset.{u_2} (α := Set (LieIdeal K L)) {J : LieIdeal K L | IsAtom J ∧ J ≤ J' ⊓ I}
    {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
⊢ LE.le.{u_2} (α := LieIdeal K L) (sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ J' ⊓ I})
    (sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I})

Tactic:
apply sSup_le_sSup

Premises used: sSup_le_sSup
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
a : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I
⊢ Subset.{u_2} (α := Set (LieIdeal K L)) {J : LieIdeal K L | IsAtom J ∧ J ≤ J' ⊓ I}
    {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
simp only [le_inf_iff, Set.setOf_subset_setOf, and_imp]

Premises used: and_imp, le_inf_iff, Set.setOf_subset_setOf
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
a a₁ a₂ a₃ a₄ : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I
a₅ : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a
a₆ : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → a ≤ I
⊢ ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I

Tactic:
tauto
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
neg : I ≤ J ⊔ J' ⊓ I
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}

Tactic:
suffices I ≤ J ⊔ (J' ⊓ I) by
    refine this.trans ?_
    apply sup_le
    · exact le_sSup ⟨hJ, hJI⟩
    rw [← atomistic (J' ⊓ I)]
    apply sSup_le_sSup
    simp only [le_inf_iff, Set.setOf_subset_setOf, and_imp]
    tauto
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : J ⊔ J' = ⊤
rw : I ≤ (J ⊔ J') ⊓ I
rw₁ : I ≤ ⊤ ⊓ I
rw₂ rw₃ : I ≤ I
⊢ I ≤ J ⊔ J' ⊓ I

Tactic:
rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]

Premises used: top_inf_eq, sup_inf_assoc_of_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
neg : J ⊔ J' = ⊤
⊢ I ≤ J ⊔ J' ⊓ I

Tactic:
suffices J ⊔ J' = ⊤ by rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
⊢ J ⊔ J' = ⊤

Tactic:
(orthogonal_isCompl Φ hΦ_nondeg hΦ_inv hΦ_refl hL J hJ).codisjoint.eq_top

Premises used: Set.Mem, setOf, LieAlgebra.InvariantForm.orthogonal_isCompl, IsCompl.codisjoint, Codisjoint.eq_top
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
⊢ J ⊔ J' = ⊤

Tactic:
exact (orthogonal_isCompl Φ hΦ_nondeg hΦ_inv hΦ_refl hL J hJ).codisjoint.eq_top

Premises used: LieAlgebra.InvariantForm.orthogonal_isCompl, IsCompl.codisjoint, Codisjoint.eq_top
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hst : (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I

Tactic:
apply finrank_lt_finrank_of_lt

Premises used: Submodule.finrank_lt_finrank_of_lt
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this_1 : I ≤ J ⊔ J' ⊓ I
this : ¬I ≤ J'
⊢ (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hst : ¬I ≤ J'
⊢ (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)

Tactic:
suffices ¬I ≤ J' by simpa
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
hst : J = ⊥
⊢ False

Tactic:
apply hJ.1

Premises used: And.left
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
hst : J ≤ ⊥
⊢ J = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff