awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
J : ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
| ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
rw [← I.incl_idealRange]

Premises used: LieIdeal.incl_idealRange
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
J : ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
| comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
congr
    next => skip
    rw [← I.incl_idealRange]

Premises used: LieIdeal.incl_idealRange
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
conv_rhs : ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
conv_rhs =>
    congr
    next => skip
    rw [← I.incl_idealRange]

Premises used: LieIdeal.incl_idealRange
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
rw : ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker
rw₁ : I.incl.IsIdealMorphism
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆

Tactic:
rw [comap_bracket_eq]

Premises used: LieIdeal.comap_bracket_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ I.incl.IsIdealMorphism

Tactic:
I.incl_isIdealMorphism

Premises used: LieIdeal.incl_isIdealMorphism
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ I.incl.IsIdealMorphism

Tactic:
exact I.incl_isIdealMorphism

Premises used: LieIdeal.incl_isIdealMorphism
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
rw : comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [comap_bracket_incl]

Premises used: LieIdeal.comap_bracket_incl
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ I ⊓ I₁ = I₁

Tactic:
rw [← inf_eq_right] at h₁ h₂

Premises used: inf_eq_right
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
h₃ : I ⊓ I₁ = I₁
⊢ I ⊓ I₂ = I₂

Tactic:
rw [← inf_eq_right] at h₁ h₂

Premises used: inf_eq_right
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
rw : comap I.incl ⁅I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
rw₁ rw₂ : comap I.incl ⁅I₁, I₂⁆ = comap I.incl ⁅I₁, I₂⁆
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
⊢ LinearMap.BilinForm.lieInvariant L Φ ↔
    Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
      (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ

Tactic:
⟨fun h x ↦ ?_, fun h x y z ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
refine_1 : ∀ (h : LinearMap.BilinForm.lieInvariant L Φ) (x : L), ⁅x, Φ⁆ = 0
refine_2 :
  ∀
    (h :
      Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
        (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ)
    (x : L) (y z : M),
    Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
⊢ LinearMap.BilinForm.lieInvariant L Φ ↔
    Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
      (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ

Tactic:
refine ⟨fun h x ↦ ?_, fun h x y z ↦ ?_⟩
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
refine_1 :
  ∀ (y z : M),
    Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ ⁅x, Φ⁆ = 0

Tactic:
ext y z
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
refine_1₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₂ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₃ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (0 : (a : M) → R) z
refine_1₄ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    0
refine_1₅ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R) =
    0
refine_1₆ refine_1₇ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]

Premises used: LinearMap.zero_apply, sub_self, LieHom.lie_apply, Module.Dual.lie_apply, LinearMap.sub_apply
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h :
  Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
    (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ
x : L
y z : M
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
replace h := LinearMap.congr_fun₂ (h x) y z
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
x : L
y z : M
h :
  Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
    ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
simp only [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply,
      LinearMap.zero_apply, sub_eq_zero] at h

Premises used: LinearMap.zero_apply, sub_eq_zero, LieHom.lie_apply, Module.Dual.lie_apply, LinearMap.sub_apply
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
x : L
y z : M
h :
  Eq.{u_1 + 1} (α := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
    ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
    (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
this :
  (∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)) →
    ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) ⁅x, y⁆ : R) (0 : R)
⊢ y ∈ (Φ.orthogonal (↑N : Submodule R M)).carrier → ⁅x, y⁆ ∈ (Φ.orthogonal (↑N : Submodule R M)).carrier

Tactic:
simpa only [LinearMap.BilinForm.isOrtho_def, -- and some default simp lemmas
        AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
        LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]

Premises used: LieSubmodule.mem_toSubmodule, AddSubsemigroup.mem_carrier, Submodule.mem_toAddSubmonoid, LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.isOrtho_def, AddSubmonoid.mem_toSubsemigroup
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
suffices :
  (∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)) →
    ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) ⁅x, y⁆ : R) (0 : R)
⊢ y ∈ (Φ.orthogonal (↑N : Submodule R M)).carrier → ⁅x, y⁆ ∈ (Φ.orthogonal (↑N : Submodule R M)).carrier

Tactic:
suffices (∀ n ∈ N, Φ n y = 0) → ∀ n ∈ N, Φ n ⁅x, y⁆ = 0 by
      simpa only [LinearMap.BilinForm.isOrtho_def, -- and some default simp lemmas
        AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
        LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
a : M
ha : a ∈ N
rw : Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, a⁆ : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) a : M →ₗ[R] R) : (a : M) → R) ⁅x, y⁆ : R) (0 : R)

Tactic:
rw [← neg_eq_zero, ← hΦ_inv]

Premises used: neg_eq_zero
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
a : M
ha : a ∈ N
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, a⁆ : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
H _ <| N.lie_mem ha

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
a : M
ha : a ∈ N
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, a⁆ : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
exact H _ <| N.lie_mem ha

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
⊢ (↑(orthogonal Φ hΦ_inv N) : Submodule R M) = Φ.orthogonal (↑N : Submodule R M)

Tactic:
rfl

Premises used: Submodule.orthogonalBilin, LinearMap.BilinForm.orthogonal, rfl
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
y : M
⊢ y ∈ orthogonal Φ hΦ_inv N ↔
    ∀ x ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
simp [orthogonal, LinearMap.BilinForm.isOrtho_def, LinearMap.BilinForm.mem_orthogonal_iff]

Premises used: LieAlgebra.InvariantForm.orthogonal, LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.isOrtho_def
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
rw : I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)

Tactic:
rw [disjoint_iff, ← hI.lt_iff, lt_iff_le_and_ne]

Premises used: IsAtom.lt_iff, lt_iff_le_and_ne, disjoint_iff
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
this : ¬I ≤ orthogonal Φ hΦ_inv I
⊢ I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
suffices : ¬I ≤ orthogonal Φ hΦ_inv I
⊢ I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I

Tactic:
suffices ¬I ≤ orthogonal Φ hΦ_inv I by simpa
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
apply : I = ⊥
⊢ False

Tactic:
apply hI.1

Premises used: And.left
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
rw : {x : L | ∃ (x_1 : ↥I) (n : ↥I), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑⊥ : Set L)
⊢ I = ⊥

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]

Premises used: lie_eq_self_of_isAtom_of_nonabelian, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
simp : ⁅(↑x : L), (↑y : L)⁆ = 0
⊢ ⁅(↑x : L), (↑y : L)⁆ ∈ (↑⊥ : Set L)

Tactic:
simp only [LieSubmodule.bot_coe, Set.mem_singleton_iff]

Premises used: LieSubmodule.bot_coe, Set.mem_singleton_iff
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
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)
⊢ ⁅(↑x : L), (↑y : L)⁆ = 0

Tactic:
apply hΦ_nondeg.1

Premises used: And.left
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
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)
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : L) → L →ₗ[R] R) ⁅(↑x : L), (↑y : L)⁆ : L →ₗ[R] R) : (a : L) → R) z : R) (0 : R)

Tactic:
rw [hΦ_inv, neg_eq_zero]

Premises used: neg_eq_zero
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
⊢ ⁅(↑x : L), z⁆ ∈ I

Tactic:
have hyz : ⁅(x : L), z⁆ ∈ I := lie_mem_left _ _ _ _ _ x.2
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
hyz : ⁅(↑x : L), z⁆ ∈ I
⊢ 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:
contra hyz y y.2

Premises used: LinearMap.IsOrtho, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Lie.InvariantForm
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
hyz : ⁅(↑x : L), z⁆ ∈ I
⊢ 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:
exact contra hyz y y.2

Premises used: Subtype.val, Subtype.property
-- 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 : Disjoint I (orthogonal Φ hΦ_inv I)
⊢ IsCompl (↑I : Submodule K L) (↑(orthogonal Φ hΦ_inv I) : Submodule K L)

Tactic:
rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl,
      ← orthogonal_toSubmodule _ hΦ_inv, LieSubmodule.disjoint_toSubmodule]

Premises used: LieSubmodule.disjoint_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint, LieAlgebra.InvariantForm.orthogonal_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
⊢ Disjoint I (orthogonal Φ hΦ_inv I)

Tactic:
orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI

Premises used: LieAlgebra.InvariantForm.orthogonal_disjoint
-- 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
⊢ Disjoint I (orthogonal Φ hΦ_inv I)

Tactic:
exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI

Premises used: LieAlgebra.InvariantForm.orthogonal_disjoint
-- 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 (↑I : Submodule K L) (↑(orthogonal Φ hΦ_inv I) : Submodule K L)
⊢ IsCompl I (orthogonal Φ hΦ_inv I)

Tactic:
rw [← LieSubmodule.isCompl_toSubmodule]

Premises used: LieSubmodule.isCompl_toSubmodule