-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma _root_.LinearMap.BilinForm.lieInvariant_iff [LieAlgebra R L] [LieModule R L M] :
    Φ.lieInvariant L ↔ Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)

Proof state:
case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)
x : L
y z : M
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

Tactic:
replace h := LinearMap.congr_fun₂ (h x) y z

Result:
case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : (⁅x, Φ⁆ y) z = (0 y) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

Proof state:
case refine_1
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
⊢ ⁅x, Φ⁆ = 0

Tactic:
ext y z

Result:
case refine_1.H
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
⊢ (⁅x, Φ⁆ y) z = (0 y) z

Proof state:
case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : -(Φ y) ⁅x, z⁆ = (Φ ⁅x, y⁆) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

Tactic:
simp [← h]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : (⁅x, Φ⁆ y) z = (0 y) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

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

Result:
case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
x : L
y z : M
h : -(Φ y) ⁅x, z⁆ = (Φ ⁅x, y⁆) z
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

Proof state:
case refine_1.H
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
⊢ (⁅x, Φ⁆ y) z = (0 y) z

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

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ LinearMap.BilinForm.lieInvariant L Φ ↔ Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)

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

Result:
case refine_1
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
⊢ ⁅x, Φ⁆ = 0

case refine_2
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)
x : L
y z : M
⊢ (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆