-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma map_posFittingComp_eq (e : M ≃ₗ⁅R,L⁆ M₂) :
    (posFittingComp R L M).map e = posFittingComp R L M₂

Proof state:
case h.e'_2.h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
m✝ : M₂
⊢ m✝ ∈ posFittingComp R L M₂ ↔
    m✝ ∈ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
rw [this]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
    LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))

Tactic:
rw [← LieSubmodule.map_comp]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
    LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
exact LieSubmodule.map_mono (map_posFittingComp_le _)

Result:
no goals

Proof state:
case h.e'_2
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Tactic:
ext

Result:
case h.e'_2.h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
m✝ : M₂
⊢ m✝ ∈ posFittingComp R L M₂ ↔
    m✝ ∈ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M) = posFittingComp R L M₂

Tactic:
refine le_antisymm (map_posFittingComp_le _) ?_

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)

Tactic:
convert LieSubmodule.map_id

Result:
case h.e'_2
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
suffices posFittingComp R L M₂ = ((posFittingComp R L M₂).map (e.symm : M₂ →ₗ⁅R,L⁆ M)).map e by
  rw [this]
  exact LieSubmodule.map_mono (map_posFittingComp_le _)

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))