awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
⊢ False
have apply : I = ⊥
Tactic: apply hI.1
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
⊢ I = ⊥
have rw : {x : L | ∃ (x_1 : ↥I) (n : ↥I), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑⊥ : Set L)
Tactic: rw [eq_bot_iff, ← lie_eq_self_of_isAtom_of_nonabelian I hI (hL I hI),
      LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
⊢ ⁅(↑x : L), (↑y : L)⁆ ∈ (↑⊥ : Set L)
have simp : ⁅(↑x : L), (↑y : L)⁆ = 0
Tactic: simp only [LieSubmodule.bot_coe, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
⊢ ⁅(↑x : L), (↑y : L)⁆ = 0
have a : ∀ (y_1 : L),
  Eq.{u_1 + 1} (α := R) ((((Φ : (a : L) → L →ₗ[R] R) ⁅(↑x : L), (↑y : L)⁆ : L →ₗ[R] R) : (a : L) → R) y_1 : R) (0 : R)
Tactic: apply hΦ_nondeg.1
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : L) → L →ₗ[R] R) ⁅(↑x : L), (↑y : L)⁆ : L →ₗ[R] R) : (a : L) → R) z : R) (0 : R)
have a : Eq.{u_1 + 1} (α := R) ((((Φ : (a : L) → L →ₗ[R] R) (↑y : L) : L →ₗ[R] R) : (a : L) → R) ⁅(↑x : L), z⁆ : R) (0 : R)
Tactic: rw [hΦ_inv, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : L) → L →ₗ[R] R) (↑y : L) : L →ₗ[R] R) : (a : L) → R) ⁅(↑x : L), z⁆ : R) (0 : R)
have hyz : ⁅(↑x : L), z⁆ ∈ I
Tactic: have hyz : ⁅(x : L), z⁆ ∈ I := lie_mem_left _ _ _ _ _ x.2
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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)
have rw : Disjoint I (orthogonal Φ hΦ_inv I)
Tactic: rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl,
      ← orthogonal_toSubmodule _ hΦ_inv, LieSubmodule.disjoint_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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 (orthogonal Φ hΦ_inv I)
have rw : IsCompl (↑I : Submodule K L) (↑(orthogonal Φ hΦ_inv I) : Submodule K L)
Tactic: rw [← LieSubmodule.isCompl_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(LieIdeal.toLieSubalgebra K L I).toSubmodule)
    (Φ.restrict (LieIdeal.toLieSubalgebra K L I).toSubmodule)
have rw : IsCompl (LieIdeal.toLieSubalgebra K L I).toSubmodule (Φ.orthogonal (LieIdeal.toLieSubalgebra K L I).toSubmodule)
Tactic: rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
    (Φ.restrict (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
have rw : IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
  (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
Tactic: rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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 (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
have simp : IsCompl (Φ.orthogonal (↑I : Submodule K L)) (↑I : Submodule K L)
Tactic: simp only [LieIdeal.toLieSubalgebra_toSubmodule, orthogonal_toSubmodule,
    LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I
have a : sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} ≤ I
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I
have a₁ : I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} ≤ I
have a : ∀ (b : LieIdeal K L), Membership.mem (γ := Set (LieIdeal K L)) {J : LieIdeal K L | IsAtom J ∧ J ≤ I} b → b ≤ I
Tactic: apply sSup_le
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have pos : ∀ (hI : I = ⊥), I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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}
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have neg : ∀ (hI : ¬I = ⊥), I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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}
have neg : ∀ (J : LieIdeal K L) (hJ : IsAtom J) (hJI : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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}
have refine : J ⊔ J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
Tactic: refine this.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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 ⊔ J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have a : J ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
Tactic: apply sup_le
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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}
⊢ J ⊔ J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have a₁ : J' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
Tactic: apply sup_le
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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' ⊓ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have 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})
Tactic: rw [← atomistic (J' ⊓ I)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ 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})
have 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}
Tactic: apply sSup_le_sSup
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ Subset.{u_2} (α := Set (LieIdeal K L)) {J : LieIdeal K L | IsAtom J ∧ J ≤ J' ⊓ I}
    {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have a : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I
Tactic: simp only [le_inf_iff, Set.setOf_subset_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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 : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I
have a₅ : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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 : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → IsAtom a ∧ a ≤ I
have a₆ : ∀ (a : LieIdeal K L), IsAtom a → a ≤ J' → a ≤ I → a ≤ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ I ≤ sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I}
have neg : I ≤ 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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' = ⊤
⊢ I ≤ J ⊔ J' ⊓ I
have rw : I ≤ (J ⊔ J') ⊓ I
Tactic: rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ I ≤ J ⊔ J' ⊓ I
have rw₁ : I ≤ ⊤ ⊓ I
Tactic: rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ I ≤ J ⊔ J' ⊓ I
have rw₂ : I ≤ I
Tactic: rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ I ≤ J ⊔ J' ⊓ I
have neg : J ⊔ J' = ⊤
Tactic: suffices J ⊔ J' = ⊤ by rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I
have hst : (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)
Tactic: apply finrank_lt_finrank_of_lt
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)
have hst : ¬I ≤ J'
Tactic: suffices ¬I ≤ J' by simpa
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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'
⊢ False
have hst : J = ⊥
Tactic: apply hJ.1
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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'
⊢ J = ⊥
have hst : J ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I
have hst : (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)
Tactic: decreasing_by
  apply finrank_lt_finrank_of_lt
  suffices ¬I ≤ J' by simpa
  intro hIJ'
  apply hJ.1
  rw [eq_bot_iff]
  exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL J hJ le_rfl (hJI.trans hIJ')