[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ adE R A (i, i) = 0
[PROOFSTEP]
have h' : (-2 : ℤ).toNat = 0 := by rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ Int.toNat (-2) = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : Int.toNat (-2) = 0
⊢ adE R A (i, i) = 0
[PROOFSTEP]
simp [adE, h, h']
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ adF R A (i, i) = 0
[PROOFSTEP]
have h' : (-2 : ℤ).toNat = 0 := by rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ Int.toNat (-2) = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : Int.toNat (-2) = 0
⊢ adF R A (i, i) = 0
[PROOFSTEP]
simp [adF, h, h']


[GOAL]
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ (fun f => (β_ M N).hom ≫ TensorProduct.lift f)
      ((fun f => LinearMap.compr₂ (TensorProduct.mk R ↑N ↑M) ((β_ N M).hom ≫ f)) f) =
    f
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ ∀ (x : ↑M) (y : ↑N),
    ↑((fun f => (β_ M N).hom ≫ TensorProduct.lift f)
            ((fun f => LinearMap.compr₂ (TensorProduct.mk R ↑N ↑M) ((β_ N M).hom ≫ f)) f))
        (x ⊗ₜ[R] y) =
      ↑f (x ⊗ₜ[R] y)
[PROOFSTEP]
intro m n
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
m : ↑M
n : ↑N
⊢ ↑((fun f => (β_ M N).hom ≫ TensorProduct.lift f)
          ((fun f => LinearMap.compr₂ (TensorProduct.mk R ↑N ↑M) ((β_ N M).hom ≫ f)) f))
      (m ⊗ₜ[R] n) =
    ↑f (m ⊗ₜ[R] n)
[PROOFSTEP]
rw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply, TensorProduct.lift.tmul, LinearMap.compr₂_apply,
  TensorProduct.mk_apply, coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ ∀ {X' X Y : ModuleCat R} (f : X' ⟶ X) (g : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y),
    ↑((fun N P => monoidalClosedHomEquiv M N P) X' Y).symm (f ≫ g) =
      (MonoidalCategory.tensorLeft M).map f ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ ↑((fun N P => monoidalClosedHomEquiv M N P) X'✝ Y✝).symm (f✝ ≫ g✝) =
    (MonoidalCategory.tensorLeft M).map f✝ ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X✝ Y✝).symm g✝
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ ∀ (x : ↑M) (y : ↑X'✝),
    ↑(↑((fun N P => monoidalClosedHomEquiv M N P) X'✝ Y✝).symm (f✝ ≫ g✝)) (x ⊗ₜ[R] y) =
      ↑((MonoidalCategory.tensorLeft M).map f✝ ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X✝ Y✝).symm g✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
intro m n
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
m : ↑M
n : ↑X'✝
⊢ ↑(↑((fun N P => monoidalClosedHomEquiv M N P) X'✝ Y✝).symm (f✝ ≫ g✝)) (m ⊗ₜ[R] n) =
    ↑((MonoidalCategory.tensorLeft M).map f✝ ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X✝ Y✝).symm g✝) (m ⊗ₜ[R] n)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ NatTrans.app (ihom.ev M) N = ↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    ↑(NatTrans.app (ihom.ev M) N) (x ⊗ₜ[R] y) =
      ↑(↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)) (x ⊗ₜ[R] y)
[PROOFSTEP]
apply ModuleCat.monoidalClosed_uncurry


[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
j : J
⊢ Monoid ((F ⋙ forget MonCat).obj j)
[PROOFSTEP]
change Monoid (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
j : J
⊢ Monoid ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
a b : (j : J) → ↑(F.obj j)
ah : a ∈ Functor.sections (F ⋙ forget MonCat)
bh : b ∈ Functor.sections (F ⋙ forget MonCat)
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget MonCat).map f ((a * b) j) = (a * b) j'
[PROOFSTEP]
simp only [Functor.comp_map, MonoidHom.map_mul, Pi.mul_apply]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
a b : (j : J) → ↑(F.obj j)
ah : a ∈ Functor.sections (F ⋙ forget MonCat)
bh : b ∈ Functor.sections (F ⋙ forget MonCat)
j j' : J
f : j ⟶ j'
⊢ (forget MonCat).map (F.map f) (a j * b j) = a j' * b j'
[PROOFSTEP]
dsimp [Functor.sections] at ah bh
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
a b : (j : J) → ↑(F.obj j)
ah : a ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
bh : b ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
j j' : J
f : j ⟶ j'
⊢ (forget MonCat).map (F.map f) (a j * b j) = a j' * b j'
[PROOFSTEP]
rw [← ah f, ← bh f, forget_map, map_mul]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget MonCat).map f (OfNat.ofNat 1 j) = OfNat.ofNat 1 j'
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
⊢ IsLimit (limitCone F)
[PROOFSTEP]
refine IsLimit.ofFaithful (forget MonCatMax) (Types.limitConeIsLimit.{v, u} _) (fun s => ⟨⟨_, ?_⟩, ?_⟩) (fun s => rfl)
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
s : Cone F
⊢ { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
      property :=
        (_ :
          ∀ {j j' : J} (f : j ⟶ j'),
            (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
              NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
    1
[PROOFSTEP]
aesop_cat
[GOAL]
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    OneHom.toFun
        {
          toFun := fun v =>
            { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j v,
              property :=
                (_ :
                  ∀ {j j' : J} (f : j ⟶ j'),
                    (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) v =
                      NatTrans.app ((forget MonCatMax).mapCone s).π j' v) },
          map_one' :=
            (_ :
              { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
                  property :=
                    (_ :
                      ∀ {j j' : J} (f : j ⟶ j'),
                        (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
                          NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
                1) }
        (x * y) =
      OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j v,
                property :=
                  (_ :
                    ∀ {j j' : J} (f : j ⟶ j'),
                      (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) v =
                        NatTrans.app ((forget MonCatMax).mapCone s).π j' v) },
            map_one' :=
              (_ :
                { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
                    property :=
                      (_ :
                        ∀ {j j' : J} (f : j ⟶ j'),
                          (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
                            NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j v,
                property :=
                  (_ :
                    ∀ {j j' : J} (f : j ⟶ j'),
                      (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) v =
                        NatTrans.app ((forget MonCatMax).mapCone s).π j' v) },
            map_one' :=
              (_ :
                { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
                    property :=
                      (_ :
                        ∀ {j j' : J} (f : j ⟶ j'),
                          (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
                            NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
                  1) }
          y
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommMonCatMax
j : J
⊢ CommMonoid ((F ⋙ forget CommMonCatMax).obj j)
[PROOFSTEP]
change CommMonoid (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommMonCatMax
j : J
⊢ CommMonoid ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommMonCatMax
c' : Cone (F ⋙ forget₂ CommMonCat MonCatMax)
t : IsLimit c'
⊢ (forget₂ CommMonCat MonCatMax).mapCone
      { pt := of (Types.limitCone (F ⋙ forget CommMonCat)).pt,
        π := NatTrans.mk (limitπMonoidHom (F ⋙ forget₂ CommMonCatMax MonCatMax)) } ≅
    c'
[PROOFSTEP]
apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit _) t
[GOAL]
J✝ : Type v
inst✝ : SmallCategory J✝
J : Type v
𝒥 : Category.{v, v} J
F : J ⥤ CommMonCatMax
⊢ PreservesLimit F (forget₂ CommMonCatMax MonCatMax)
[PROOFSTEP]
infer_instance


[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ AddCommGroup ((F ⋙ forget (ModuleCat R)).obj j)
[PROOFSTEP]
change AddCommGroup (F.obj j)
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ AddCommGroup ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ Module R ((F ⋙ forget (ModuleCat R)).obj j)
[PROOFSTEP]
change Module R (F.obj j)
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ Module R ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
src✝ : AddSubgroup
  ((j : J) → ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat).obj j)) :=
  AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat)
r : R
s : (j : J) → ↑(F.obj j)
sh :
  s ∈
    {
          toAddSubsemigroup :=
            { carrier := Functor.sections (F ⋙ forget (ModuleCat R)),
              add_mem' :=
                (_ : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
          zero_mem' :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                ((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                        forget AddGroupCat).map
                    f (OfNat.ofNat 0 j) =
                  OfNat.ofNat 0 j') }.toAddSubsemigroup.carrier
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget (ModuleCat R)).map f ((r • s) j) = (r • s) j'
[PROOFSTEP]
simp only [forget_map, Functor.comp_map, Pi.smul_apply, map_smul]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
src✝ : AddSubgroup
  ((j : J) → ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat).obj j)) :=
  AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat)
r : R
s : (j : J) → ↑(F.obj j)
sh :
  s ∈
    {
          toAddSubsemigroup :=
            { carrier := Functor.sections (F ⋙ forget (ModuleCat R)),
              add_mem' :=
                (_ : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
          zero_mem' :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                ((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                        forget AddGroupCat).map
                    f (OfNat.ofNat 0 j) =
                  OfNat.ofNat 0 j') }.toAddSubsemigroup.carrier
j j' : J
f : j ⟶ j'
⊢ r • ↑(F.map f) (s j) = r • s j'
[PROOFSTEP]
dsimp [Functor.sections] at sh
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
src✝ : AddSubgroup
  ((j : J) → ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat).obj j)) :=
  AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat)
r : R
s : (j : J) → ↑(F.obj j)
sh : s ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
j j' : J
f : j ⟶ j'
⊢ r • ↑(F.map f) (s j) = r • s j'
[PROOFSTEP]
rw [sh f]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ AddCommMonoid { x // x ∈ sectionsSubmodule F }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ AddCommGroup { x // x ∈ sectionsSubmodule F }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ Module R { x // x ∈ sectionsSubmodule F }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ IsLimit (limitCone F)
[PROOFSTEP]
refine'
  IsLimit.ofFaithful (forget (ModuleCat R)) (Types.limitConeIsLimit.{v, w} _)
    (fun s => ⟨⟨(Types.limitConeIsLimit.{v, w} _).lift ((forget (ModuleCat R)).mapCone s), _⟩, _⟩) (fun s => rfl)
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) (x + y) =
      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x +
        IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) y
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (r : R) (x : ↑s.pt),
    AddHom.toFun
        { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
          map_add' := ?refine'_1 }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          {
            toFun :=
              IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
            map_add' := ?refine'_1 }
          x
[PROOFSTEP]
all_goals
  intros
  dsimp [Types.limitConeIsLimit]
  simp
  rfl
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) (x + y) =
      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x +
        IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
x✝ y✝ : ↑s.pt
⊢ IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) (x✝ + y✝) =
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x✝ +
      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) y✝
[PROOFSTEP]
dsimp [Types.limitConeIsLimit]
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
x✝ y✝ : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) (x✝ + y✝),
      property :=
        (_ :
          ∀ {j j' : J} (f : j ⟶ j'),
            (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) (x✝ + y✝) =
              NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' (x✝ + y✝)) } =
    { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) } +
      { val := fun j => ↑(NatTrans.app s.π j) y✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) y✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' y✝) }
[PROOFSTEP]
simp
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
x✝ y✝ : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) x✝ + ↑(NatTrans.app s.π j) y✝,
      property :=
        (_ :
          (fun x => x ∈ Functor.sections (F ⋙ forget (ModuleCat R))) fun j =>
            ↑(NatTrans.app s.π j) x✝ + ↑(NatTrans.app s.π j) y✝) } =
    { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) } +
      { val := fun j => ↑(NatTrans.app s.π j) y✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) y✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' y✝) }
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (r : R) (x : ↑s.pt),
    AddHom.toFun
        { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
          map_add' :=
            (_ :
              ∀ (x y : ↑s.pt),
                IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                    (x + y) =
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      x +
                    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      y) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          {
            toFun :=
              IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
            map_add' :=
              (_ :
                ∀ (x y : ↑s.pt),
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      (x + y) =
                    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                        x +
                      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R)))
                        ((forget (ModuleCat R)).mapCone s) y) }
          x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
r✝ : R
x✝ : ↑s.pt
⊢ AddHom.toFun
      { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
        map_add' :=
          (_ :
            ∀ (x y : ↑s.pt),
              IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                  (x + y) =
                IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x +
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                    y) }
      (r✝ • x✝) =
    ↑(RingHom.id R) r✝ •
      AddHom.toFun
        { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
          map_add' :=
            (_ :
              ∀ (x y : ↑s.pt),
                IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                    (x + y) =
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      x +
                    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      y) }
        x✝
[PROOFSTEP]
dsimp [Types.limitConeIsLimit]
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
r✝ : R
x✝ : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) (r✝ • x✝),
      property :=
        (_ :
          ∀ {j j' : J} (f : j ⟶ j'),
            (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) (r✝ • x✝) =
              NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' (r✝ • x✝)) } =
    r✝ •
      { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) }
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
r✝ : R
x✝ : ↑s.pt
⊢ { val := fun j => r✝ • ↑(NatTrans.app s.π j) x✝,
      property :=
        (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (ModuleCat R))) fun j => r✝ • ↑(NatTrans.app s.π j) x✝) } =
    r✝ •
      { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
i : ι
⊢ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (𝟙 i) =
    𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
i : ι
⊢ ∀ (x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)),
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (𝟙 i)) x =
      ↑(𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
i : ι
x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)
⊢ ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (𝟙 i)) x =
    ↑(𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)) x
[PROOFSTEP]
apply Module.DirectedSystem.map_self
[GOAL]
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk) =
    { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
      { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ ∀ (x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj X✝)),
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk)) x =
      ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
            { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk)
        x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj X✝)
⊢ ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk)) x =
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
          { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk)
      x
[PROOFSTEP]
symm
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj X✝)
⊢ ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
          { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk)
      x =
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk)) x
[PROOFSTEP]
apply Module.DirectedSystem.map_map
[GOAL]
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
⊢ (directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝ =
    DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
⊢ ∀ (x : ↑((directLimitDiagram G f).obj x✝¹)),
    ↑((directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝) x =
      ↑(DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
x : ↑((directLimitDiagram G f).obj x✝¹)
⊢ ↑((directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝) x =
    ↑(DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij) x
[PROOFSTEP]
exact DirectLimit.of_f
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
rw [← s.w (homOfLE h)]
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑((directLimitDiagram G f).map (homOfLE h) ≫ NatTrans.app s.ι j) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
⊢ NatTrans.app (directLimitCocone G f).ι i ≫
      (fun s =>
          DirectLimit.lift R ι G f s.ι.app
            (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
        s =
    NatTrans.app s.ι i
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
⊢ ∀ (x : ↑((directLimitDiagram G f).obj i)),
    ↑(NatTrans.app (directLimitCocone G f).ι i ≫
            (fun s =>
                DirectLimit.lift R ι G f s.ι.app
                  (_ :
                    ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
              s)
        x =
      ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
x : ↑((directLimitDiagram G f).obj i)
⊢ ↑(NatTrans.app (directLimitCocone G f).ι i ≫
          (fun s =>
              DirectLimit.lift R ι G f s.ι.app
                (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
            s)
      x =
    ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
dsimp only [directLimitCocone, CategoryStruct.comp]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
x : ↑((directLimitDiagram G f).obj i)
⊢ ↑(LinearMap.comp
          (DirectLimit.lift R ι G f s.ι.app
            (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
          (DirectLimit.of R ι G f i))
      x =
    ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
rw [LinearMap.comp_apply]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
x : ↑((directLimitDiagram G f).obj i)
⊢ ↑(DirectLimit.lift R ι G f s.ι.app
          (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
      (↑(DirectLimit.of R ι G f i) x) =
    ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
apply DirectLimit.lift_of
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        DirectLimit.lift R ι G f s.ι.app
          (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
      s
[PROOFSTEP]
have : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i) :=
  by
  funext i
  rw [← h]
  rfl
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
⊢ s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
[PROOFSTEP]
funext i
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
i : ι
⊢ NatTrans.app s.ι i = LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
[PROOFSTEP]
rw [← h]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
i : ι
⊢ NatTrans.app (directLimitCocone G f).ι i ≫ m =
    LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
⊢ m =
    (fun s =>
        DirectLimit.lift R ι G f s.ι.app
          (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
      s
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
⊢ ∀ (x : ↑(directLimitCocone G f).pt),
    ↑m x =
      ↑((fun s =>
              DirectLimit.lift R ι G f s.ι.app
                (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
            s)
        x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
x : ↑(directLimitCocone G f).pt
⊢ ↑m x =
    ↑((fun s =>
            DirectLimit.lift R ι G f s.ι.app
              (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
          s)
      x
[PROOFSTEP]
simp only [this]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
x : ↑(directLimitCocone G f).pt
⊢ ↑m x =
    ↑(DirectLimit.lift R ι G f (fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i))
          (_ :
            ∀ (i j : ι) (hij : i ≤ j) (x : G i),
              ↑((fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) j)
                  (↑(f i j hij) x) =
                ↑((fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) i) x))
      x
[PROOFSTEP]
apply Module.DirectLimit.lift_unique


[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing L
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieAlgebra R L
[PROOFSTEP]
infer_instance


[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ g) ≫ (braiding Y₁ Y₂).hom = (braiding X₁ X₂).hom ≫ (g ⊗ f)
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂), ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
[PROOFSTEP]
intro x y
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    ((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    ↑((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro x y z
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ ↑((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)
[PROOFSTEP]
apply (cancel_epi (α_ X Y Z).hom).1
[GOAL]
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    ↑((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑((α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro x y z
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ ↑((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑((α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : ModuleCat R
⊢ (β_ x✝¹ x✝).hom ≫ (β_ x✝ x✝¹).hom = 𝟙 (x✝¹ ⊗ x✝)
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : ModuleCat R
⊢ ∀ (x : ↑x✝¹) (y : ↑x✝), ↑((β_ x✝¹ x✝).hom ≫ (β_ x✝ x✝¹).hom) (x ⊗ₜ[R] y) = ↑(𝟙 (x✝¹ ⊗ x✝)) (x ⊗ₜ[R] y)
[PROOFSTEP]
aesop_cat


[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a✝ b✝ : M
hm₁ : a✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
hm₂ : b✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ ⁅x, a✝ + b✝⁆ ∈ N
[PROOFSTEP]
rw [lie_add]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a✝ b✝ : M
hm₁ : a✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
hm₂ : b✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ ⁅x, a✝⁆ + ⁅x, b✝⁆ ∈ N
[PROOFSTEP]
exact N.add_mem' (hm₁ x) (hm₂ x)
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
⊢ ⁅x, 0⁆ ∈ N
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
m : M
hm :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := {m | ∀ (x : L), ⁅x, m⁆ ∈ N},
              add_mem' :=
                (_ :
                  ∀ {a b : M},
                    a ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → b ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → ∀ (x : L), ⁅x, a + b⁆ ∈ N) },
          zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ ∈ N) }.toAddSubsemigroup.carrier
x : L
⊢ ⁅x, t • m⁆ ∈ N
[PROOFSTEP]
rw [lie_smul]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
m : M
hm :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := {m | ∀ (x : L), ⁅x, m⁆ ∈ N},
              add_mem' :=
                (_ :
                  ∀ {a b : M},
                    a ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → b ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → ∀ (x : L), ⁅x, a + b⁆ ∈ N) },
          zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ ∈ N) }.toAddSubsemigroup.carrier
x : L
⊢ t • ⁅x, m⁆ ∈ N
[PROOFSTEP]
exact N.smul_mem' t (hm x)
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
m : M
hm :
  m ∈
    {
            toAddSubmonoid :=
              {
                toAddSubsemigroup :=
                  { carrier := {m | ∀ (x : L), ⁅x, m⁆ ∈ N},
                    add_mem' :=
                      (_ :
                        ∀ {a b : M},
                          a ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} →
                            b ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → ∀ (x : L), ⁅x, a + b⁆ ∈ N) },
                zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ ∈ N) },
            smul_mem' :=
              (_ :
                ∀ (t : R) (m : M),
                  m ∈
                      {
                            toAddSubsemigroup :=
                              { carrier := {m | ∀ (x : L), ⁅x, m⁆ ∈ N},
                                add_mem' :=
                                  (_ :
                                    ∀ {a b : M},
                                      a ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} →
                                        b ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → ∀ (x : L), ⁅x, a + b⁆ ∈ N) },
                            zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ ∈ N) }.toAddSubsemigroup.carrier →
                    ∀ (x : L), ⁅x, t • m⁆ ∈ N) }.toAddSubmonoid.toAddSubsemigroup.carrier
y : L
⊢ ⁅y, ⁅x, m⁆⁆ ∈ N
[PROOFSTEP]
rw [leibniz_lie]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
m : M
hm :
  m ∈
    {
            toAddSubmonoid :=
              {
                toAddSubsemigroup :=
                  { carrier := {m | ∀ (x : L), ⁅x, m⁆ ∈ N},
                    add_mem' :=
                      (_ :
                        ∀ {a b : M},
                          a ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} →
                            b ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → ∀ (x : L), ⁅x, a + b⁆ ∈ N) },
                zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ ∈ N) },
            smul_mem' :=
              (_ :
                ∀ (t : R) (m : M),
                  m ∈
                      {
                            toAddSubsemigroup :=
                              { carrier := {m | ∀ (x : L), ⁅x, m⁆ ∈ N},
                                add_mem' :=
                                  (_ :
                                    ∀ {a b : M},
                                      a ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} →
                                        b ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N} → ∀ (x : L), ⁅x, a + b⁆ ∈ N) },
                            zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ ∈ N) }.toAddSubsemigroup.carrier →
                    ∀ (x : L), ⁅x, t • m⁆ ∈ N) }.toAddSubmonoid.toAddSubsemigroup.carrier
y : L
⊢ ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆ ∈ N
[PROOFSTEP]
exact N.add_mem' (hm ⁅y, x⁆) (N.lie_mem (hm y))
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
⊢ N ≤ normalizer N
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ m ∈ normalizer N
[PROOFSTEP]
rw [mem_normalizer]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N
[PROOFSTEP]
exact fun x => N.lie_mem hm
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
⊢ normalizer (N₁ ⊓ N₂) = normalizer N₁ ⊓ normalizer N₂
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ normalizer (N₁ ⊓ N₂) ↔ m✝ ∈ normalizer N₁ ⊓ normalizer N₂
[PROOFSTEP]
simp [← forall_and]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
⊢ Monotone normalizer
[PROOFSTEP]
intro N₁ N₂ h m hm
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁✝ N₂✝ N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : m ∈ normalizer N₁
⊢ m ∈ normalizer N₂
[PROOFSTEP]
rw [mem_normalizer] at hm ⊢
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁✝ N₂✝ N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₂
[PROOFSTEP]
exact fun x => h (hm x)
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
⊢ comap f (normalizer N) = normalizer (comap f N)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
m✝ : M'
⊢ m✝ ∈ comap f (normalizer N) ↔ m✝ ∈ normalizer (comap f N)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ N' : LieSubmodule R L M
⊢ ⁅⊤, N⁆ ≤ N' ↔ N ≤ normalizer N'
[PROOFSTEP]
rw [lie_le_iff]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ N' : LieSubmodule R L M
⊢ (∀ (x : L), x ∈ ⊤ → ∀ (m : M), m ∈ N → ⁅x, m⁆ ∈ N') ↔ N ≤ normalizer N'
[PROOFSTEP]
tauto
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
src✝ : LieSubmodule R { x // x ∈ H } L := LieSubmodule.normalizer (toLieSubmodule H)
y z : L
hy : y ∈ src✝.carrier
hz : z ∈ src✝.carrier
x : { x // x ∈ H }
⊢ ⁅x, ⁅y, z⁆⁆ ∈ toLieSubmodule H
[PROOFSTEP]
rw [coe_bracket_of_module, mem_toLieSubmodule, leibniz_lie, ← lie_skew y, ← sub_eq_add_neg]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
src✝ : LieSubmodule R { x // x ∈ H } L := LieSubmodule.normalizer (toLieSubmodule H)
y z : L
hy : y ∈ src✝.carrier
hz : z ∈ src✝.carrier
x : { x // x ∈ H }
⊢ ⁅⁅↑x, y⁆, z⁆ - ⁅⁅↑x, z⁆, y⁆ ∈ H
[PROOFSTEP]
exact H.sub_mem (hz ⟨_, hy x⟩) (hy ⟨_, hz x⟩)
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
⊢ x ∈ normalizer H ↔ ∀ (y : L), y ∈ H → ⁅y, x⁆ ∈ H
[PROOFSTEP]
rw [Subtype.forall']
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
⊢ x ∈ normalizer H ↔ ∀ (x_1 : { a // a ∈ H }), ⁅↑x_1, x⁆ ∈ H
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
⊢ x ∈ normalizer H ↔ ∀ (y : L), y ∈ H → ⁅x, y⁆ ∈ H
[PROOFSTEP]
rw [mem_normalizer_iff']
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
⊢ (∀ (y : L), y ∈ H → ⁅y, x⁆ ∈ H) ↔ ∀ (y : L), y ∈ H → ⁅x, y⁆ ∈ H
[PROOFSTEP]
refine' forall₂_congr fun y hy => _
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
[PROOFSTEP]
rw [← lie_skew, neg_mem_iff (G := L)]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y z : L
hx : x ∈ normalizer H
hy : y ∈ Submodule.span R {x} ⊔ H.toSubmodule
hz : z ∈ Submodule.span R {x} ⊔ H.toSubmodule
⊢ ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
[PROOFSTEP]
rw [Submodule.mem_sup] at hy hz
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y z : L
hx : x ∈ normalizer H
hy : ∃ y_1, y_1 ∈ Submodule.span R {x} ∧ ∃ z, z ∈ H.toSubmodule ∧ y_1 + z = y
hz : ∃ y, y ∈ Submodule.span R {x} ∧ ∃ z_1, z_1 ∈ H.toSubmodule ∧ y + z_1 = z
⊢ ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
[PROOFSTEP]
obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy
[GOAL]
case intro.intro.intro.intro
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x z : L
hx : x ∈ normalizer H
hz : ∃ y, y ∈ Submodule.span R {x} ∧ ∃ z_1, z_1 ∈ H.toSubmodule ∧ y + z_1 = z
u₁ : L
hu₁ : u₁ ∈ Submodule.span R {x}
v : L
hv : v ∈ H
⊢ ⁅u₁ + v, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
[PROOFSTEP]
obtain ⟨u₂, hu₂, w, hw : w ∈ H, rfl⟩ := hz
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
u₁ : L
hu₁ : u₁ ∈ Submodule.span R {x}
v : L
hv : v ∈ H
u₂ : L
hu₂ : u₂ ∈ Submodule.span R {x}
w : L
hw : w ∈ H
⊢ ⁅u₁ + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
[PROOFSTEP]
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hu₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
v : L
hv : v ∈ H
u₂ : L
hu₂ : u₂ ∈ Submodule.span R {x}
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Submodule.mem_span_singleton.mp hu₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, s • x + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
[PROOFSTEP]
apply Submodule.mem_sup_right
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule
[PROOFSTEP]
simp only [LieSubalgebra.mem_coe_submodule, smul_lie, add_lie, zero_add, lie_add, smul_zero, lie_smul, lie_self]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H
[PROOFSTEP]
refine' H.add_mem (H.smul_mem s _) (H.add_mem (H.smul_mem t _) (H.lie_mem hv hw))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.refine'_1
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅v, x⁆ ∈ H
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.refine'_2
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x : L
hx : x ∈ normalizer H
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅x, w⁆ ∈ H
[PROOFSTEP]
exacts [(H.mem_normalizer_iff' x).mp hx v hv, (H.mem_normalizer_iff x).mp hx w hw]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y : L
hx : x ∈ normalizer H
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H
[PROOFSTEP]
rw [← lie_skew, neg_mem_iff (G := L)]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y : L
hx : x ∈ normalizer H
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
[PROOFSTEP]
exact hx ⟨y, hy⟩
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ normalizer H
⊢ ∃ I, ↑R { x // x ∈ K } I = ofLe h₁
[PROOFSTEP]
rw [exists_nested_lieIdeal_coe_eq_iff]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ normalizer H
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
[PROOFSTEP]
exact fun x y hx hy => ideal_in_normalizer (h₂ hx) hy
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
⊢ normalizer H = H ↔ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) = ⊥
[PROOFSTEP]
rw [LieSubmodule.eq_bot_iff]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
⊢ normalizer H = H ↔
    ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => le_antisymm _ H.le_normalizer⟩
[GOAL]
case refine'_1
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
⊢ ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
[PROOFSTEP]
rintro ⟨x⟩ hx
[GOAL]
case refine'_1.mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ Quot.mk Setoid.r x = 0
[PROOFSTEP]
suffices x ∈ H by
  rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero, coe_toLieSubmodule, mem_coe_submodule]
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
this : x ∈ H
⊢ Quot.mk Setoid.r x = 0
[PROOFSTEP]
rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero, coe_toLieSubmodule, mem_coe_submodule]
[GOAL]
case refine'_1.mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ x ∈ H
[PROOFSTEP]
rw [← h, H.mem_normalizer_iff']
[GOAL]
case refine'_1.mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ ∀ (y : L), y ∈ H → ⁅y, x⁆ ∈ H
[PROOFSTEP]
intro y hy
[GOAL]
case refine'_1.mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
[PROOFSTEP]
replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
[GOAL]
case refine'_1.mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x y : L
hy : y ∈ H
hx : ⁅{ val := y, property := hy }, ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H
[PROOFSTEP]
rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx
[GOAL]
case refine'_2
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
⊢ normalizer H ≤ H
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
⊢ x ∈ H
[PROOFSTEP]
let y := LieSubmodule.Quotient.mk' H.toLieSubmodule x
[GOAL]
case refine'_2
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
⊢ x ∈ H
[PROOFSTEP]
have hy : y ∈ LieModule.maxTrivSubmodule R H (L ⧸ H.toLieSubmodule) :=
  by
  rintro ⟨z, hz⟩
  rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module, Submodule.coe_mk,
    mem_toLieSubmodule]
  exact (H.mem_normalizer_iff' x).mp hx z hz
[GOAL]
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
⊢ y ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
z : L
hz : z ∈ H
⊢ ⁅{ val := z, property := hz }, y⁆ = 0
[PROOFSTEP]
rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module, Submodule.coe_mk,
  mem_toLieSubmodule]
[GOAL]
case mk
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H
[PROOFSTEP]
exact (H.mem_normalizer_iff' x).mp hx z hz
[GOAL]
case refine'_2
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
hy : y ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ x ∈ H
[PROOFSTEP]
simpa using h y hy