-- Mathlib/Algebra/Lie/Abelian.lean
theorem isTrivial_iff_max_triv_eq_top : IsTrivial L M ↔ maxTrivSubmodule R L M = ⊤

Proof state:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
m : M
⊢ m ∈ ⊤

Tactic:
exact LieSubmodule.mem_top m

Result:
no goals

Proof state:
case mp.mk
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
⊢ maxTrivSubmodule R L M = ⊤

Tactic:
ext

Result:
case mp.mk.h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
m✝ : M
⊢ m✝ ∈ maxTrivSubmodule R L M ↔ m✝ ∈ ⊤

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ IsTrivial L M → maxTrivSubmodule R L M = ⊤

Tactic:
rintro ⟨h⟩

Result:
case mp.mk
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
⊢ maxTrivSubmodule R L M = ⊤

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ maxTrivSubmodule R L M = ⊤ → IsTrivial L M

Tactic:
intro h

Result:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
⊢ IsTrivial L M

Proof state:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0

Tactic:
intro x m

Result:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
x : L
m : M
⊢ ⁅x, m⁆ = 0

Proof state:
case mp.mk.h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
m✝ : M
⊢ m✝ ∈ maxTrivSubmodule R L M ↔ m✝ ∈ ⊤

Tactic:
simp only [mem_maxTrivSubmodule, h, forall_const, LieSubmodule.mem_top]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ IsTrivial L M ↔ maxTrivSubmodule R L M = ⊤

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ IsTrivial L M → maxTrivSubmodule R L M = ⊤

case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ maxTrivSubmodule R L M = ⊤ → IsTrivial L M

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
⊢ IsTrivial L M

Tactic:
constructor

Result:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0

Proof state:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
m : M
⊢ ∀ (x : L), ⁅x, m⁆ = 0

Tactic:
rw [← mem_maxTrivSubmodule R L M, h]

Result:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
m : M
⊢ m ∈ ⊤

Proof state:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
x : L
m : M
⊢ ⁅x, m⁆ = 0

Tactic:
revert x

Result:
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
m : M
⊢ ∀ (x : L), ⁅x, m⁆ = 0