[GOAL]
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
N✝ N' N O : LieSubmodule R L M
h : (fun s => s.carrier) N = (fun s => s.carrier) O
⊢ N = O
[PROOFSTEP]
cases N
[GOAL]
case 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
N N' O : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : (fun s => s.carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = (fun s => s.carrier) O
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = O
[PROOFSTEP]
cases O
[GOAL]
case mk.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
N N' : LieSubmodule R L M
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s => s.carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s => s.carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSubmodule
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
N N' : LieSubmodule R L M
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s => s.carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s => s.carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ toSubmodule✝¹ = toSubmodule✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
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
N N' : LieSubmodule R L M
src✝ : Submodule R M := 0
x : L
m : M
h :
  m ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, m⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [(Submodule.mem_bot R).1 h]
[GOAL]
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
N N' : LieSubmodule R L M
src✝ : Submodule R M := 0
x : L
m : M
h :
  m ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, 0⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
apply lie_zero
[GOAL]
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
N N' : LieSubmodule R L M
p : Submodule R M
h :
  ∀ {x : L} {m : M},
    m ∈
        { toAddSubmonoid := p.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      ⁅x, m⁆ ∈
        { toAddSubmonoid := p.toAddSubmonoid,
                smul_mem' :=
                  (_ : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ↑{
        toSubmodule :=
          { toAddSubmonoid := p.toAddSubmonoid,
            smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier) },
        lie_mem := h } =
    p
[PROOFSTEP]
cases p
[GOAL]
case 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
N N' : LieSubmodule R L M
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x : L} {m : M},
    m ∈
        { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : M},
                      x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                        c • x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' :=
                                    smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      ⁅x, m⁆ ∈
        { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : M},
                      x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                        c • x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' :=
                                    smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ↑{
        toSubmodule :=
          { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M},
                  x ∈
                      { toAddSubmonoid := toAddSubmonoid✝,
                              smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                    c • x ∈
                      { toAddSubmonoid := toAddSubmonoid✝,
                              smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) },
        lie_mem := h } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
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
N N' x y : LieSubmodule R L M
h : ↑x = ↑y
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case 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
N N' y : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = ↑y
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk.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
N N' : LieSubmodule R L M
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
[PROOFSTEP]
congr
[GOAL]
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
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
a✝ b✝ : M
x : a✝ ∈ s
y : b✝ ∈ s
⊢ a✝ + b✝ ∈ s
[PROOFSTEP]
rw [hs] at x y ⊢
[GOAL]
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
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
a✝ b✝ : M
x : a✝ ∈ ↑N
y : b✝ ∈ ↑N
⊢ a✝ + b✝ ∈ ↑N
[PROOFSTEP]
exact N.add_mem' x y
[GOAL]
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
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
⊢ 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier
[PROOFSTEP]
exact hs.symm ▸ N.zero_mem'
[GOAL]
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
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
⊢ ∀ (c : R) {x : M},
    x ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' :=
                          (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
exact hs.symm ▸ N.smul_mem'
[GOAL]
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
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
⊢ ∀ {x : L} {m : M},
    m ∈
        {
                toAddSubmonoid :=
                  { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
                    zero_mem' :=
                      (_ : 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) },
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : M},
                      x ∈
                          {
                                toAddSubsemigroup :=
                                  { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
                                zero_mem' :=
                                  (_ :
                                    0 ∈
                                      { carrier := s,
                                          add_mem' :=
                                            (_ :
                                              ∀ {a b : M},
                                                a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
                        c • x ∈
                          {
                                toAddSubsemigroup :=
                                  { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
                                zero_mem' :=
                                  (_ :
                                    0 ∈
                                      { carrier := s,
                                          add_mem' :=
                                            (_ :
                                              ∀ {a b : M},
                                                a ∈ s →
                                                  b ∈ s →
                                                    a + b ∈
                                                      s) }.carrier) }.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      ⁅x, m⁆ ∈
        {
                toAddSubmonoid :=
                  { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
                    zero_mem' :=
                      (_ : 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) },
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : M},
                      x ∈
                          {
                                toAddSubsemigroup :=
                                  { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
                                zero_mem' :=
                                  (_ :
                                    0 ∈
                                      { carrier := s,
                                          add_mem' :=
                                            (_ :
                                              ∀ {a b : M},
                                                a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
                        c • x ∈
                          {
                                toAddSubsemigroup :=
                                  { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
                                zero_mem' :=
                                  (_ :
                                    0 ∈
                                      { carrier := s,
                                          add_mem' :=
                                            (_ :
                                              ∀ {a b : M},
                                                a ∈ s →
                                                  b ∈ s →
                                                    a + b ∈
                                                      s) }.carrier) }.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact hs.symm ▸ N.lie_mem
[GOAL]
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
N N' : LieSubmodule R L M
⊢ ∀ (x y : L) (m : { x // x ∈ ↑N }), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
[PROOFSTEP]
intro x y m
[GOAL]
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
N N' : LieSubmodule R L M
x y : L
m : { x // x ∈ ↑N }
⊢ ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
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
N N' : LieSubmodule R L M
x y : L
m : { x // x ∈ ↑N }
⊢ ↑⁅x + y, m⁆ = ↑(⁅x, m⁆ + ⁅y, m⁆)
[PROOFSTEP]
apply add_lie
[GOAL]
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
N N' : LieSubmodule R L M
⊢ ∀ (x : L) (m n : { x // x ∈ ↑N }), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
[PROOFSTEP]
intro x m n
[GOAL]
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
N N' : LieSubmodule R L M
x : L
m n : { x // x ∈ ↑N }
⊢ ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
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
N N' : LieSubmodule R L M
x : L
m n : { x // x ∈ ↑N }
⊢ ↑⁅x, m + n⁆ = ↑(⁅x, m⁆ + ⁅x, n⁆)
[PROOFSTEP]
apply lie_add
[GOAL]
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
N N' : LieSubmodule R L M
⊢ ∀ (x y : L) (m : { x // x ∈ ↑N }), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
[PROOFSTEP]
intro x y m
[GOAL]
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
N N' : LieSubmodule R L M
x y : L
m : { x // x ∈ ↑N }
⊢ ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
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
N N' : LieSubmodule R L M
x y : L
m : { x // x ∈ ↑N }
⊢ ↑⁅x, ⁅y, m⁆⁆ = ↑(⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆)
[PROOFSTEP]
apply leibniz_lie
[GOAL]
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
N N' : LieSubmodule R L M
⊢ ∀ (t : R) (x : L) (m : { x // x ∈ ↑N }), ⁅t • x, m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
intro t x y
[GOAL]
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
N N' : LieSubmodule R L M
t : R
x : L
y : { x // x ∈ ↑N }
⊢ ⁅t • x, y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
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
N N' : LieSubmodule R L M
t : R
x : L
y : { x // x ∈ ↑N }
⊢ ↑⁅t • x, y⁆ = ↑(t • ⁅x, y⁆)
[PROOFSTEP]
apply smul_lie
[GOAL]
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
N N' : LieSubmodule R L M
⊢ ∀ (t : R) (x : L) (m : { x // x ∈ ↑N }), ⁅x, t • m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
intro t x y
[GOAL]
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
N N' : LieSubmodule R L M
t : R
x : L
y : { x // x ∈ ↑N }
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
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
N N' : LieSubmodule R L M
t : R
x : L
y : { x // x ∈ ↑N }
⊢ ↑⁅x, t • y⁆ = ↑(t • ⁅x, y⁆)
[PROOFSTEP]
apply lie_smul
[GOAL]
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
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅x, y⁆ ∈ I
[PROOFSTEP]
rw [← lie_skew, ← neg_lie]
[GOAL]
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
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅-y, x⁆ ∈ I
[PROOFSTEP]
apply lie_mem_right
[GOAL]
case 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
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ x ∈ I
[PROOFSTEP]
assumption
[GOAL]
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
I : LieIdeal R L
src✝ : Submodule R L := ↑I
⊢ ∀ {x y : L},
    x ∈
        { toAddSubmonoid := src✝.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : L},
                      x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈
          { toAddSubmonoid := src✝.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L},
                        x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := src✝.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L},
                        x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
intro x y _ hy
[GOAL]
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
I : LieIdeal R L
src✝ : Submodule R L := ↑I
x y : L
a✝ :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
apply lie_mem_right
[GOAL]
case 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
I : LieIdeal R L
src✝ : Submodule R L := ↑I
x y : L
a✝ :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ y ∈ I
[PROOFSTEP]
exact hy
[GOAL]
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
p : Submodule R M
⊢ (∃ N, ↑N = p) ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
constructor
[GOAL]
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
p : Submodule R M
⊢ (∃ N, ↑N = p) → ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
rintro ⟨N, rfl⟩ _ _
[GOAL]
case mp.intro
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
N : LieSubmodule R L M
x✝ : L
m✝ : M
⊢ m✝ ∈ ↑N → ⁅x✝, m✝⁆ ∈ ↑N
[PROOFSTEP]
exact N.lie_mem
[GOAL]
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
p : Submodule R M
⊢ (∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p
[PROOFSTEP]
intro h
[GOAL]
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
p : Submodule R M
h : ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
⊢ ∃ N, ↑N = p
[PROOFSTEP]
use{ p with lie_mem := @h }
[GOAL]
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
K : LieSubalgebra R L
⊢ (∃ I, ↑R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
[PROOFSTEP]
simp only [← coe_to_submodule_eq_iff, LieIdeal.coe_to_lieSubalgebra_to_submodule,
  Submodule.exists_lieSubmodule_coe_eq_iff L]
  -- Porting note: was `exact Iff.rfl`
[GOAL]
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
K : LieSubalgebra R L
⊢ (∀ (x m : L), m ∈ K.toSubmodule → ⁅x, m⁆ ∈ K.toSubmodule) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
[PROOFSTEP]
simp only [mem_coe_submodule]
[GOAL]
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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∃ I, ↑R { x // x ∈ K' } I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
[PROOFSTEP]
simp only [exists_lieIdeal_coe_eq_iff, coe_bracket, mem_ofLe]
[GOAL]
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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : { x // x ∈ K' }), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
[PROOFSTEP]
constructor
[GOAL]
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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : { x // x ∈ K' }), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
[PROOFSTEP]
intro h' x y hx hy
[GOAL]
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
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : { x // x ∈ K' }), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K
[PROOFSTEP]
exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy
[GOAL]
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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : { x // x ∈ K' }), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
[PROOFSTEP]
rintro h' ⟨x, hx⟩ ⟨y, hy⟩ hy'
[GOAL]
case mpr.mk.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
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : ↑{ val := y, property := hy } ∈ K
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := y, property := hy }⁆ ∈ K
[PROOFSTEP]
exact h' x y hx hy'
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
src✝ : Submodule R M := sInf {x | ∃ s, s ∈ S ∧ ↑s = x}
x : L
m : M
h :
  m ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, m⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp only [Submodule.mem_carrier, mem_iInter, Submodule.sInf_coe, mem_setOf_eq, forall_apply_eq_imp_iff₂,
  forall_exists_index, and_imp] at h ⊢
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
src✝ : Submodule R M := sInf {x | ∃ s, s ∈ S ∧ ↑s = x}
x : L
m : M
h : ∀ (a : LieSubmodule R L M), a ∈ S → m ∈ ↑↑a
⊢ ∀ (a : LieSubmodule R L M), a ∈ S → ⁅x, m⁆ ∈ ↑↑a
[PROOFSTEP]
intro N hN
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
src✝ : Submodule R M := sInf {x | ∃ s, s ∈ S ∧ ↑s = x}
x : L
m : M
h : ∀ (a : LieSubmodule R L M), a ∈ S → m ∈ ↑↑a
N : LieSubmodule R L M
hN : N ∈ S
⊢ ⁅x, m⁆ ∈ ↑↑N
[PROOFSTEP]
apply N.lie_mem (h N hN)
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
⊢ ↑(sInf S) = ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule, sInf_coe_toSubmodule, Submodule.sInf_coe]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
⊢ ⋂ (p : Submodule R M) (_ : p ∈ {x | ∃ s, s ∈ S ∧ ↑s = x}), ↑p = ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
[PROOFSTEP]
ext m
[GOAL]
case 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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
m : M
⊢ m ∈ ⋂ (p : Submodule R M) (_ : p ∈ {x | ∃ s, s ∈ S ∧ ↑s = x}), ↑p ↔ m ∈ ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp only [mem_iInter, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp, and_imp, SetLike.mem_coe, mem_coeSubmodule]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
⊢ IsGLB S (sInf S)
[PROOFSTEP]
have h : ∀ {N N' : LieSubmodule R L M}, (N : Set M) ≤ N' ↔ N ≤ N' := fun {_ _} ↦ Iff.rfl
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB S (sInf S)
[PROOFSTEP]
apply IsGLB.of_image h
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB ((fun {x} => ↑x) '' S) ↑(sInf S)
[PROOFSTEP]
simp only [sInf_coe]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB ((fun {x} => ↑x) '' S) (⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s)
[PROOFSTEP]
exact isGLB_biInf
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
src✝¹ : PartialOrder (LieSubmodule R L M) := SetLike.instPartialOrder
src✝ : CompleteLattice (LieSubmodule R L M) :=
  completeLatticeOfInf (LieSubmodule R L M) (_ : ∀ (S : Set (LieSubmodule R L M)), IsGLB S (sInf S))
N : LieSubmodule R L M
x✝ : M
h : x✝ ∈ ⊥
⊢ x✝ ∈ N
[PROOFSTEP]
rw [mem_bot] at h 
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
src✝¹ : PartialOrder (LieSubmodule R L M) := SetLike.instPartialOrder
src✝ : CompleteLattice (LieSubmodule R L M) :=
  completeLatticeOfInf (LieSubmodule R L M) (_ : ∀ (S : Set (LieSubmodule R L M)), IsGLB S (sInf S))
N : LieSubmodule R L M
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ N
[PROOFSTEP]
rw [h]
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
src✝¹ : PartialOrder (LieSubmodule R L M) := SetLike.instPartialOrder
src✝ : CompleteLattice (LieSubmodule R L M) :=
  completeLatticeOfInf (LieSubmodule R L M) (_ : ∀ (S : Set (LieSubmodule R L M)), IsGLB S (sInf S))
N : LieSubmodule R L M
x✝ : M
h : x✝ = 0
⊢ 0 ∈ N
[PROOFSTEP]
exact N.zero_mem'
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ↑(N ⊔ N') = ↑N ⊔ ↑N'
[PROOFSTEP]
have aux : ∀ {x : L} {m}, m ∈ (N ⊔ N' : Submodule R M) → ⁅x, m⁆ ∈ (N ⊔ N' : Submodule R M) :=
  by
  simp only [Submodule.mem_sup]
  rintro x m ⟨y, hy, z, hz, rfl⟩
  refine' ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
[PROOFSTEP]
simp only [Submodule.mem_sup]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ∀ {x : L} {m : M}, (∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = m) → ∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = ⁅x, m⁆
[PROOFSTEP]
rintro x m ⟨y, hy, z, hz, rfl⟩
[GOAL]
case intro.intro.intro.intro
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : L
y : M
hy : y ∈ ↑N
z : M
hz : z ∈ ↑N'
⊢ ∃ y_1, y_1 ∈ ↑N ∧ ∃ z_1, z_1 ∈ ↑N' ∧ y_1 + z_1 = ⁅x, y + z⁆
[PROOFSTEP]
refine' ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑(N ⊔ N') = ↑N ⊔ ↑N'
[PROOFSTEP]
refine'
  le_antisymm (sInf_le ⟨{ (N ⊔ N' : Submodule R M) with lie_mem := aux }, _⟩)
    _
      -- Porting note: rewrote proof
[GOAL]
case refine'_1
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ (let src := ↑N ⊔ ↑N';
      {
        toSubmodule :=
          { toAddSubmonoid := src.toAddSubmonoid,
            smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ src.carrier → c • x ∈ src.carrier) },
        lie_mem := (_ : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N') }) ∈
      {x | N ≤ x ∧ N' ≤ x} ∧
    ↑(let src := ↑N ⊔ ↑N';
        {
          toSubmodule :=
            { toAddSubmonoid := src.toAddSubmonoid,
              smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ src.carrier → c • x ∈ src.carrier) },
          lie_mem := (_ : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N') }) =
      ↑N ⊔ ↑N'
[PROOFSTEP]
simp only [← coeSubmodule_le_coeSubmodule, mem_setOf_eq, and_true_iff]
[GOAL]
case refine'_1
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ≤
      { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) } ∧
    ↑N' ≤
      { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.left
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ≤
    { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
      smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_1.right
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N' ≤
    { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
      smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_1.left
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
x : M
hx : x ∈ ↑N
⊢ x ∈
    { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
      smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
[PROOFSTEP]
simp [Submodule.mem_sup_left hx, hx, Submodule.mem_sup_right hx]
[GOAL]
case refine'_1.right
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
x : M
hx : x ∈ ↑N'
⊢ x ∈
    { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
      smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
[PROOFSTEP]
simp [Submodule.mem_sup_left hx, hx, Submodule.mem_sup_right hx]
[GOAL]
case refine'_2
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ⊔ ↑N' ≤ ↑(N ⊔ N')
[PROOFSTEP]
simp
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : M
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
[PROOFSTEP]
rw [← mem_coeSubmodule, ← mem_coeSubmodule, ← mem_coeSubmodule, inf_coe_toSubmodule, Submodule.mem_inf]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : M
⊢ x ∈ N ⊔ N' ↔ ∃ y, y ∈ N ∧ ∃ z, z ∈ N' ∧ y + z = x
[PROOFSTEP]
rw [← mem_coeSubmodule, sup_coe_toSubmodule, Submodule.mem_sup]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : M
⊢ (∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = x) ↔ ∃ y, y ∈ N ∧ ∃ z, z ∈ N' ∧ y + z = x
[PROOFSTEP]
exact Iff.rfl
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ N = ⊥ ↔ ∀ (m : M), m ∈ N → m = 0
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ N ≤ ⊥ ↔ ∀ (m : M), m ∈ N → m = 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ Subsingleton (LieSubmodule R L { x // x ∈ ↑⊥ })
[PROOFSTEP]
apply subsingleton_of_bot_eq_top
[GOAL]
case 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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ⊥ = ⊤
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case hα.h.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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : M
hx : x ∈ ↑⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
change x ∈ ⊥ at hx 
[GOAL]
case hα.h.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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : M
hx : x ∈ ⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
rw [Submodule.mem_bot] at hx 
[GOAL]
case hα.h.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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : M
hx✝ : x ∈ ⊥
hx : x = 0
⊢ { val := x, property := hx✝ } ∈ ⊥ ↔ { val := x, property := hx✝ } ∈ ⊤
[PROOFSTEP]
subst hx
[GOAL]
case hα.h.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
N N' : LieSubmodule R L M
I J : LieIdeal R L
hx : 0 ∈ ⊥
⊢ { val := 0, property := hx } ∈ ⊥ ↔ { val := 0, property := hx } ∈ ⊤
[PROOFSTEP]
simp only [true_iff_iff, eq_self_iff_true, Submodule.mk_eq_zero, LieSubmodule.mem_bot, mem_top]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x✝² x✝¹ x✝ : LieSubmodule R L M
⊢ x✝² ≤ x✝ → (x✝² ⊔ x✝¹) ⊓ x✝ ≤ x✝² ⊔ x✝¹ ⊓ x✝
[PROOFSTEP]
simp only [← coeSubmodule_le_coeSubmodule, sup_coe_toSubmodule, inf_coe_toSubmodule]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
x✝² x✝¹ x✝ : LieSubmodule R L M
⊢ ↑x✝² ≤ ↑x✝ → (↑x✝² ⊔ ↑x✝¹) ⊓ ↑x✝ ≤ ↑x✝² ⊔ ↑x✝¹ ⊓ ↑x✝
[PROOFSTEP]
exact IsModularLattice.sup_inf_le_assoc_of_le _
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ Subsingleton (LieSubmodule R L M) ↔ Subsingleton (Submodule R M)
[PROOFSTEP]
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← coe_toSubmodule_eq_iff, top_coeSubmodule,
  bot_coeSubmodule]
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
⊢ Nontrivial { x // x ∈ ↑N } ↔ N ≠ ⊥
[PROOFSTEP]
constructor
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
⊢ Nontrivial { x // x ∈ ↑N } → N ≠ ⊥
[PROOFSTEP]
contrapose!
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
⊢ N ≠ ⊥ → Nontrivial { x // x ∈ ↑N }
[PROOFSTEP]
contrapose!
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
⊢ N = ⊥ → ¬Nontrivial { x // x ∈ ↑N }
[PROOFSTEP]
rintro rfl ⟨⟨m₁, h₁ : m₁ ∈ (⊥ : LieSubmodule R L M)⟩, ⟨m₂, h₂ : m₂ ∈ (⊥ : LieSubmodule R L M)⟩, h₁₂⟩
[GOAL]
case mp.mk.intro.mk.intro.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
N N' : LieSubmodule R L M
I J : LieIdeal R L
m₁ : M
h₁ : m₁ ∈ ⊥
m₂ : M
h₂ : m₂ ∈ ⊥
h₁₂ : { val := m₁, property := h₁ } ≠ { val := m₂, property := h₂ }
⊢ False
[PROOFSTEP]
simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂ 
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
⊢ ¬Nontrivial { x // x ∈ ↑N } → N = ⊥
[PROOFSTEP]
rw [not_nontrivial_iff_subsingleton, LieSubmodule.eq_bot_iff]
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
⊢ Subsingleton { x // x ∈ ↑N } → ∀ (m : M), m ∈ N → m = 0
[PROOFSTEP]
rintro ⟨h⟩ m hm
[GOAL]
case mpr.intro
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
N : LieSubmodule R L M
h : ∀ (a b : { x // x ∈ ↑N }), a = b
m : M
hm : m ∈ N
⊢ m = 0
[PROOFSTEP]
simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
h : N ≤ N'
x y : { x // x ∈ ↑N }
⊢ ↑(homOfLe h) x = ↑(homOfLe h) y → x = y
[PROOFSTEP]
simp only [homOfLe_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
x : M
⊢ x ∈ lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
[PROOFSTEP]
change x ∈ (lieSpan R L s : Set M) ↔ _
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
x : M
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
[PROOFSTEP]
erw [sInf_coe]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
x : M
⊢ x ∈ ⋂ (s_1 : LieSubmodule R L M) (_ : s_1 ∈ {N | s ⊆ ↑N}), ↑s_1 ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
[PROOFSTEP]
exact mem_iInter₂
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
⊢ s ⊆ ↑(lieSpan R L s)
[PROOFSTEP]
intro m hm
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
m : M
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)
[PROOFSTEP]
erw [mem_lieSpan]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
m : M
hm : m ∈ s
⊢ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
[PROOFSTEP]
intro N hN
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
m : M
hm : m ∈ s
N : LieSubmodule R L M
hN : s ⊆ ↑N
⊢ m ∈ N
[PROOFSTEP]
exact hN hm
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
⊢ Submodule.span R s ≤ ↑(lieSpan R L s)
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
⊢ s ⊆ ↑↑(lieSpan R L s)
[PROOFSTEP]
apply subset_lieSpan
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N ↔ s ⊆ ↑N
[PROOFSTEP]
constructor
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ ↑N
[PROOFSTEP]
exact Subset.trans subset_lieSpan
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N
[PROOFSTEP]
intro hs m hm
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : m ∈ lieSpan R L s
⊢ m ∈ N
[PROOFSTEP]
rw [mem_lieSpan] at hm 
[GOAL]
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
⊢ m ∈ N
[PROOFSTEP]
exact hm _ hs
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s t : Set M
h : s ⊆ t
⊢ lieSpan R L s ≤ lieSpan R L t
[PROOFSTEP]
rw [lieSpan_le]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s t : Set M
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)
[PROOFSTEP]
exact Subset.trans h subset_lieSpan
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∃ N, ↑N = p
[PROOFSTEP]
rw [p.exists_lieSubmodule_coe_eq_iff L]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
constructor
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p → ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
intro h
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
⊢ (∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p) → ↑(lieSpan R L ↑p) = p
[PROOFSTEP]
intro h
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
⊢ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
intro x m hm
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ p
[PROOFSTEP]
rw [← h, mem_coeSubmodule]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ lieSpan R L ↑p
[PROOFSTEP]
exact lie_mem _ (subset_lieSpan hm)
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
p : Submodule R M
h : ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
⊢ ↑(lieSpan R L ↑p) = p
[PROOFSTEP]
rw [← coe_toSubmodule_mk p @h, coe_toSubmodule, coe_toSubmodule_eq_iff, lieSpan_eq]
[GOAL]
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
⊢ lieSpan R L s = ⊥ ↔ ∀ (m : M), m ∈ s → m = 0
[PROOFSTEP]
rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M' := Submodule.map ↑f ↑N
x : L
m' : M'
h :
  m' ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, m'⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rcases h with ⟨m, hm, hfm⟩
[GOAL]
case intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M' := Submodule.map ↑f ↑N
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : ↑↑f m = m'
⊢ ⁅x, m'⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
use⁅x, m⁆
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M' := Submodule.map ↑f ↑N
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : ↑↑f m = m'
⊢ ⁅x, m⁆ ∈ ↑↑N ∧ ↑↑f ⁅x, m⁆ = ⁅x, m'⁆
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M' := Submodule.map ↑f ↑N
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : ↑↑f m = m'
⊢ ⁅x, m⁆ ∈ ↑↑N
[PROOFSTEP]
apply N.lie_mem hm
[GOAL]
case h.right
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M' := Submodule.map ↑f ↑N
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : ↑↑f m = m'
⊢ ↑↑f ⁅x, m⁆ = ⁅x, m'⁆
[PROOFSTEP]
norm_cast at hfm 
[GOAL]
case h.right
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M' := Submodule.map ↑f ↑N
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : ↑f m = m'
⊢ ↑↑f ⁅x, m⁆ = ⁅x, m'⁆
[PROOFSTEP]
simp [hfm]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M := Submodule.comap ↑f ↑N'
x : L
m : M
h :
  m ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, m⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
suffices ⁅x, f m⁆ ∈ N' by simp [this]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M := Submodule.comap ↑f ↑N'
x : L
m : M
h :
  m ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
this : ⁅x, ↑f m⁆ ∈ N'
⊢ ⁅x, m⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
src✝ : Submodule R M := Submodule.comap ↑f ↑N'
x : L
m : M
h :
  m ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : M}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, ↑f m⁆ ∈ N'
[PROOFSTEP]
apply N'.lie_mem h
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
⊢ comap (incl N) N₂ = ⊤ ↔ N ≤ N₂
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.coeSubmodule_comap, LieSubmodule.incl_coe,
  LieSubmodule.top_coeSubmodule, Submodule.comap_subtype_eq_top, coeSubmodule_le_coeSubmodule]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
⊢ comap (incl N) N₂ = ⊥ ↔ N ⊓ N₂ = ⊥
[PROOFSTEP]
simp only [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.coeSubmodule_comap, LieSubmodule.incl_coe,
  LieSubmodule.bot_coeSubmodule, ← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff, inf_coe_toSubmodule]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
src✝ : Submodule R L := Submodule.comap (↑f) (↑R L' J).toSubmodule
x y : L
h :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
suffices ⁅f x, f y⁆ ∈ J
  by
  simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
    Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie, LieSubalgebra.mem_coe_submodule]
  exact this
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
src✝ : Submodule R L := Submodule.comap (↑f) (↑R L' J).toSubmodule
x y : L
h :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
this : ⁅↑f x, ↑f y⁆ ∈ J
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
  Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie, LieSubalgebra.mem_coe_submodule]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
src✝ : Submodule R L := Submodule.comap (↑f) (↑R L' J).toSubmodule
x y : L
h :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
this : ⁅↑f x, ↑f y⁆ ∈ J
⊢ ⁅↑f x, ↑f y⁆ ∈ ↑R L' J
[PROOFSTEP]
exact this
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
src✝ : Submodule R L := Submodule.comap (↑f) (↑R L' J).toSubmodule
x y : L
h :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅↑f x, ↑f y⁆ ∈ J
[PROOFSTEP]
apply J.lie_mem h
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
h : ↑(map f I) = ↑f '' ↑I
⊢ ↑(map f I) = Submodule.map ↑f ↑I
[PROOFSTEP]
rw [SetLike.ext'_iff, LieSubmodule.coe_toSubmodule, h, Submodule.map_coe]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
h : ↑(map f I) = ↑f '' ↑I
⊢ ↑f '' ↑I = ↑↑f '' ↑↑I
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ I
⊢ ↑f x ∈ map f I
[PROOFSTEP]
apply LieSubmodule.subset_lieSpan
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ I
⊢ ↑f x ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
use x
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ I
⊢ x ∈ ↑(↑R L I).toSubmodule ∧ ↑↑f x = ↑f x
[PROOFSTEP]
exact ⟨hx, rfl⟩
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ map f I ≤ J ↔ I ≤ comap f J
[PROOFSTEP]
rw [map_le]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ ↑f '' ↑I ⊆ ↑J ↔ I ≤ comap f J
[PROOFSTEP]
exact Set.image_subset_iff
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ map f (comap f J) ≤ J
[PROOFSTEP]
rw [map_le_iff_le_comap]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ I ≤ comap f (map f I)
[PROOFSTEP]
rw [← map_le_iff_le_comap]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂✝ : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ map f I₁ ≤ map f I₂
[PROOFSTEP]
rw [SetLike.le_def] at h 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂✝ : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
h : ∀ ⦃x : L⦄, x ∈ I₁ → x ∈ I₂
⊢ map f I₁ ≤ map f I₂
[PROOFSTEP]
apply LieSubmodule.lieSpan_mono (Set.image_subset (⇑f) h)
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : J₁ ≤ J₂
⊢ comap f J₁ ≤ comap f J₂
[PROOFSTEP]
rw [← SetLike.coe_subset_coe] at h ⊢
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ ↑(comap f J₁) ⊆ ↑(comap f J₂)
[PROOFSTEP]
dsimp only [SetLike.coe]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ (↑(comap f J₁)).toAddSubmonoid.toAddSubsemigroup.carrier ⊆ (↑(comap f J₂)).toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact Set.preimage_mono h
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
h : ↑f '' ↑I = ↑J
⊢ map f I = J
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
h : ↑f '' ↑I = ↑J
⊢ map f I ≤ J
[PROOFSTEP]
erw [LieSubmodule.lieSpan_le, Submodule.map_coe, h]
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
h : ↑f '' ↑I = ↑J
⊢ J ≤ map f I
[PROOFSTEP]
rw [← SetLike.coe_subset_coe, ← h]
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
h : ↑f '' ↑I = ↑J
⊢ ↑f '' ↑I ⊆ ↑(map f I)
[PROOFSTEP]
exact LieSubmodule.subset_lieSpan
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ Subsingleton (LieIdeal R { x // x ∈ ↑⊥ })
[PROOFSTEP]
apply subsingleton_of_bot_eq_top
[GOAL]
case hα
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ ⊥ = ⊤
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case hα.h.mk
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ ↑⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
change x ∈ (⊥ : LieIdeal _ _) at hx 
[GOAL]
case hα.h.mk
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ ⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
rw [LieSubmodule.mem_bot] at hx 
[GOAL]
case hα.h.mk
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x : L
hx✝ : x ∈ ⊥
hx : x = 0
⊢ { val := x, property := hx✝ } ∈ ⊥ ↔ { val := x, property := hx✝ } ∈ ⊤
[PROOFSTEP]
subst hx
[GOAL]
case hα.h.mk
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
hx : 0 ∈ ⊥
⊢ { val := 0, property := hx } ∈ ⊥ ↔ { val := 0, property := hx } ∈ ⊤
[PROOFSTEP]
simp only [Submodule.mk_eq_zero, LieSubmodule.mem_bot, LieSubmodule.mem_top]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ idealRange f = LieIdeal.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
m✝ : L'
⊢ m✝ ∈ idealRange f ↔ m✝ ∈ LieIdeal.map f ⊤
[PROOFSTEP]
simp only [idealRange, range_eq_map]
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
m✝ : L'
⊢ m✝ ∈ LieSubmodule.lieSpan R L' ↑(LieSubalgebra.map f ⊤) ↔ m✝ ∈ LieIdeal.map f ⊤
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ IsIdealMorphism f ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
[PROOFSTEP]
simp only [isIdealMorphism_def, idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_to_submodule_eq_iff, ←
  f.range.coe_to_submodule, LieIdeal.coe_to_lieSubalgebra_to_submodule, LieSubmodule.coe_lieSpan_submodule_eq_iff,
  LieSubalgebra.mem_coe_submodule, mem_range, exists_imp, Submodule.exists_lieSubmodule_coe_eq_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆) ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆) → ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
[PROOFSTEP]
intro h x y
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y : L
⊢ ∃ z, ⁅x, ↑f y⁆ = ↑f z
[PROOFSTEP]
obtain ⟨z, hz⟩ := h x (f y) y rfl
[GOAL]
case mp.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y z : L
hz : ↑f z = ⁅x, ↑f y⁆
⊢ ∃ z, ⁅x, ↑f y⁆ = ↑f z
[PROOFSTEP]
use z
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y z : L
hz : ↑f z = ⁅x, ↑f y⁆
⊢ ⁅x, ↑f y⁆ = ↑f z
[PROOFSTEP]
exact hz.symm
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z) → ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
[PROOFSTEP]
intro h x y z hz
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
⊢ ∃ y_1, ↑f y_1 = ⁅x, y⁆
[PROOFSTEP]
obtain ⟨w, hw⟩ := h x z
[GOAL]
case mpr.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
w : L
hw : ⁅x, ↑f z⁆ = ↑f w
⊢ ∃ y_1, ↑f y_1 = ⁅x, y⁆
[PROOFSTEP]
use w
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
w : L
hw : ⁅x, ↑f z⁆ = ↑f w
⊢ ↑f w = ⁅x, y⁆
[PROOFSTEP]
rw [← hw, hz]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ LieIdeal.map f I ≤ idealRange f
[PROOFSTEP]
rw [f.idealRange_eq_map]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤
[PROOFSTEP]
exact LieIdeal.map_mono le_top
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L
⊢ x ∈ ↑(ker f) ↔ ↑f x = 0
[PROOFSTEP]
simp only [ker_coeSubmodule, LinearMap.mem_ker, coe_toLinearMap]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L
⊢ ↑f x ∈ idealRange f
[PROOFSTEP]
rw [idealRange_eq_map]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L
⊢ ↑f x ∈ LieIdeal.map f ⊤
[PROOFSTEP]
exact LieIdeal.mem_map (LieSubmodule.mem_top x)
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : IsIdealMorphism f
y : L'
⊢ y ∈ idealRange f ↔ ∃ x, ↑f x = y
[PROOFSTEP]
rw [f.isIdealMorphism_def] at h 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ↑R L' (idealRange f) = range f
y : L'
⊢ y ∈ idealRange f ↔ ∃ x, ↑f x = y
[PROOFSTEP]
rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toSubalgebra, h, f.range_coe, Set.mem_range]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ I ≤ ker f ↔ ∀ (x : L), x ∈ I → ↑f x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ I ≤ ker f → ∀ (x : L), x ∈ I → ↑f x = 0
[PROOFSTEP]
intro h x hx
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x : L), x ∈ I → ↑f x = 0) → I ≤ ker f
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : I ≤ ker f
x : L
hx : x ∈ I
⊢ ↑f x = 0
[PROOFSTEP]
specialize h hx
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ I
h : x ∈ ker f
⊢ ↑f x = 0
[PROOFSTEP]
rw [mem_ker] at h 
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L
hx : x ∈ I
h : ↑f x = 0
⊢ ↑f x = 0
[PROOFSTEP]
exact h
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L), x ∈ I → ↑f x = 0
x : L
hx : x ∈ I
⊢ x ∈ ker f
[PROOFSTEP]
rw [mem_ker]
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L), x ∈ I → ↑f x = 0
x : L
hx : x ∈ I
⊢ ↑f x = 0
[PROOFSTEP]
apply h x hx
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ker f = ⊥ ↔ Function.Injective ↑f
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, ker_coeSubmodule, LieSubmodule.bot_coeSubmodule, LinearMap.ker_eq_bot,
  coe_toLinearMap]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ range f = ⊤ ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [← LieSubalgebra.coe_to_submodule_eq_iff, range_coeSubmodule, LieSubalgebra.top_coe_submodule]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ LinearMap.range ↑f = ⊤ ↔ Function.Surjective ↑f
[PROOFSTEP]
exact LinearMap.range_eq_top
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
⊢ idealRange f = ⊤
[PROOFSTEP]
rw [← f.range_eq_top] at h 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : range f = ⊤
⊢ idealRange f = ⊤
[PROOFSTEP]
rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_to_submodule, ← LieSubmodule.coe_toSubmodule_eq_iff,
  LieSubmodule.top_coeSubmodule, LieSubalgebra.top_coe_submodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : range f = ⊤
⊢ ∃ N, ↑N = ⊤
[PROOFSTEP]
use⊤
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : range f = ⊤
⊢ ↑⊤ = ⊤
[PROOFSTEP]
exact LieSubmodule.top_coeSubmodule
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
⊢ IsIdealMorphism f
[PROOFSTEP]
rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h, LieIdeal.top_coe_lieSubalgebra]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f I = ⊥ ↔ I ≤ LieHom.ker f
[PROOFSTEP]
rw [← le_bot_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f I ≤ ⊥ ↔ I ≤ LieHom.ker f
[PROOFSTEP]
exact LieIdeal.map_le_iff_le_comap
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
⊢ ↑(map f I) = Submodule.map ↑f ↑I
[PROOFSTEP]
let J : LieIdeal R L' :=
  { (I : Submodule R L).map (f : L →ₗ[R] L') with
    lie_mem := fun {x y} hy ↦ by
      have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
      obtain ⟨z₂, hz₂, rfl⟩ := hy'
      obtain ⟨z₁, rfl⟩ := h x
      simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image, LieSubmodule.mem_coeSubmodule,
        Submodule.mem_carrier, Submodule.map_coe]
      use⁅z₁, z₂⁆
      exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩ }
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
x y : L'
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
x y : L'
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ∃ x, x ∈ I ∧ ↑f x = y
[PROOFSTEP]
simpa [hy]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
x y : L'
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy' : ∃ x, x ∈ I ∧ ↑f x = y
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
obtain ⟨z₂, hz₂, rfl⟩ := hy'
[GOAL]
case intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
x : L'
z₂ : L
hz₂ : z₂ ∈ I
hy :
  ↑f z₂ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, ↑f z₂⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
obtain ⟨z₁, rfl⟩ := h x
[GOAL]
case intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
z₂ : L
hz₂ : z₂ ∈ I
hy :
  ↑f z₂ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
z₁ : L
⊢ ⁅↑f z₁, ↑f z₂⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image, LieSubmodule.mem_coeSubmodule, Submodule.mem_carrier,
  Submodule.map_coe]
[GOAL]
case intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
z₂ : L
hz₂ : z₂ ∈ I
hy :
  ↑f z₂ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
z₁ : L
⊢ ∃ x, x ∈ (↑R L I).toSubmodule ∧ ↑f x = ⁅↑f z₁, ↑f z₂⁆
[PROOFSTEP]
use⁅z₁, z₂⁆
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : Function.Surjective ↑f
src✝ : Submodule R L' := Submodule.map (↑f) (↑R L I).toSubmodule
z₂ : L
hz₂ : z₂ ∈ I
hy :
  ↑f z₂ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L'}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
z₁ : L
⊢ ⁅z₁, z₂⁆ ∈ (↑R L I).toSubmodule ∧ ↑f ⁅z₁, z₂⁆ = ⁅↑f z₁, ↑f z₂⁆
[PROOFSTEP]
exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J✝ : LieIdeal R L'
h : Function.Surjective ↑f
J : LieIdeal R L' :=
  let src := Submodule.map (↑f) (↑R L I).toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L'}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem :=
      (_ :
        ∀ {x y : L'},
          y ∈
              { toAddSubmonoid := src.toAddSubmonoid,
                      smul_mem' :=
                        (_ :
                          ∀ (c : R) {x : L'},
                            x ∈ src.carrier → c • x ∈ src.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
            ⁅x, y⁆ ∈
              { toAddSubmonoid := src.toAddSubmonoid,
                      smul_mem' :=
                        (_ :
                          ∀ (c : R) {x : L'},
                            x ∈ src.carrier → c • x ∈ src.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier) }
⊢ ↑(map f I) = Submodule.map ↑f ↑I
[PROOFSTEP]
erw [LieSubmodule.coe_lieSpan_submodule_eq_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J✝ : LieIdeal R L'
h : Function.Surjective ↑f
J : LieIdeal R L' :=
  let src := Submodule.map (↑f) (↑R L I).toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L'}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem :=
      (_ :
        ∀ {x y : L'},
          y ∈
              { toAddSubmonoid := src.toAddSubmonoid,
                      smul_mem' :=
                        (_ :
                          ∀ (c : R) {x : L'},
                            x ∈ src.carrier → c • x ∈ src.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
            ⁅x, y⁆ ∈
              { toAddSubmonoid := src.toAddSubmonoid,
                      smul_mem' :=
                        (_ :
                          ∀ (c : R) {x : L'},
                            x ∈ src.carrier → c • x ∈ src.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier) }
⊢ ∃ N, ↑N = Submodule.map (↑f) (↑R L I).toSubmodule
[PROOFSTEP]
use J
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
y : L'
h₁ : Function.Surjective ↑f
h₂ : y ∈ map f I
⊢ ∃ x, ↑f ↑x = y
[PROOFSTEP]
rw [← LieSubmodule.mem_coeSubmodule, coe_map_of_surjective h₁, Submodule.mem_map] at h₂ 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
y : L'
h₁ : Function.Surjective ↑f
h₂ : ∃ y_1, y_1 ∈ ↑I ∧ ↑↑f y_1 = y
⊢ ∃ x, ↑f ↑x = y
[PROOFSTEP]
obtain ⟨x, hx, rfl⟩ := h₂
[GOAL]
case intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h₁ : Function.Surjective ↑f
x : L
hx : x ∈ ↑I
⊢ ∃ x_1, ↑f ↑x_1 = ↑↑f x
[PROOFSTEP]
use⟨x, hx⟩
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h₁ : Function.Surjective ↑f
x : L
hx : x ∈ ↑I
⊢ ↑f ↑{ val := x, property := hx } = ↑↑f x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I✝ : LieIdeal R L
J : LieIdeal R L'
I : LieIdeal R L
h₁ : Function.Injective ↑f
h₂ : map f I = ⊥
⊢ I = ⊥
[PROOFSTEP]
rw [← f.ker_eq_bot] at h₁ 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I✝ : LieIdeal R L
J : LieIdeal R L'
I : LieIdeal R L
h₁ : LieHom.ker f = ⊥
h₂ : map f I = ⊥
⊢ I = ⊥
[PROOFSTEP]
change comap f ⊥ = ⊥ at h₁ 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I✝ : LieIdeal R L
J : LieIdeal R L'
I : LieIdeal R L
h₂ : map f I = ⊥
h₁ : comap f ⊥ = ⊥
⊢ I = ⊥
[PROOFSTEP]
rw [eq_bot_iff, map_le_iff_le_comap, h₁] at h₂ 
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I✝ : LieIdeal R L
J : LieIdeal R L'
I : LieIdeal R L
h₂ : I ≤ ⊥
h₁ : comap f ⊥ = ⊥
⊢ I = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I✝ : LieIdeal R L
J : LieIdeal R L'
I : LieIdeal R L
h₂ : I ≤ ⊥
h₁ : comap f ⊥ = ⊥
⊢ I ≤ ⊥
[PROOFSTEP]
exact h₂
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
x y : { x // x ∈ ↑I₁ }
⊢ ↑(homOfLe h) x = ↑(homOfLe h) y → x = y
[PROOFSTEP]
simp only [homOfLe_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f (I ⊔ LieHom.ker f) = map f I
[PROOFSTEP]
suffices LieIdeal.map f (I ⊔ f.ker) ≤ LieIdeal.map f I by exact le_antisymm this (LieIdeal.map_mono le_sup_left)
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
this : map f (I ⊔ LieHom.ker f) ≤ map f I
⊢ map f (I ⊔ LieHom.ker f) = map f I
[PROOFSTEP]
exact le_antisymm this (LieIdeal.map_mono le_sup_left)
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f (I ⊔ LieHom.ker f) ≤ map f I
[PROOFSTEP]
apply LieSubmodule.lieSpan_mono
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ↑(Submodule.map (↑f) (↑R L (I ⊔ LieHom.ker f)).toSubmodule) ⊆ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
rintro x ⟨y, hy₁, hy₂⟩
[GOAL]
case h.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L'
y : L
hy₁ : y ∈ ↑(↑R L (I ⊔ LieHom.ker f)).toSubmodule
hy₂ : ↑↑f y = x
⊢ x ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
rw [← hy₂]
[GOAL]
case h.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L'
y : L
hy₁ : y ∈ ↑(↑R L (I ⊔ LieHom.ker f)).toSubmodule
hy₂ : ↑↑f y = x
⊢ ↑↑f y ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
erw [LieSubmodule.mem_sup] at hy₁ 
[GOAL]
case h.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L'
y : L
hy₁ : ∃ y_1, y_1 ∈ I ∧ ∃ z, z ∈ LieHom.ker f ∧ y_1 + z = y
hy₂ : ↑↑f y = x
⊢ ↑↑f y ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁
[GOAL]
case h.intro.intro.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L'
y : L
hy₂ : ↑↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ LieHom.ker f
hy : z₁ + z₂ = y
⊢ ↑↑f y ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
rw [← hy]
[GOAL]
case h.intro.intro.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L'
y : L
hy₂ : ↑↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ LieHom.ker f
hy : z₁ + z₂ = y
⊢ ↑↑f (z₁ + z₂) ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
rw [f.coe_toLinearMap, f.map_add, f.mem_ker.mp hz₂, add_zero]
[GOAL]
case h.intro.intro.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
x : L'
y : L
hy₂ : ↑↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ LieHom.ker f
hy : z₁ + z₂ = y
⊢ ↑f z₁ ∈ ↑(Submodule.map (↑f) (↑R L I).toSubmodule)
[PROOFSTEP]
exact ⟨z₁, hz₁, rfl⟩
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f I ⊔ map f (LieHom.ker f) = map f I
[PROOFSTEP]
simpa using map_sup_ker_eq_map (f := f)
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ map f (comap f J) = LieHom.idealRange f ⊓ J
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ map f (comap f J) ≤ LieHom.idealRange f ⊓ J
[PROOFSTEP]
rw [le_inf_iff]
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ map f (comap f J) ≤ LieHom.idealRange f ∧ map f (comap f J) ≤ J
[PROOFSTEP]
exact ⟨f.map_le_idealRange _, map_comap_le⟩
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ LieHom.idealRange f ⊓ J ≤ map f (comap f J)
[PROOFSTEP]
rw [f.isIdealMorphism_def] at h 
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ↑R L' (LieHom.idealRange f) = LieHom.range f
⊢ LieHom.idealRange f ⊓ J ≤ map f (comap f J)
[PROOFSTEP]
rw [← SetLike.coe_subset_coe, LieSubmodule.inf_coe, ← coe_toSubalgebra, h]
[GOAL]
case a
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ↑R L' (LieHom.idealRange f) = LieHom.range f
⊢ ↑(LieHom.range f) ∩ ↑J ⊆ ↑(map f (comap f J))
[PROOFSTEP]
rintro y ⟨⟨x, h₁⟩, h₂⟩
[GOAL]
case a.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ↑R L' (LieHom.idealRange f) = LieHom.range f
y : L'
h₂ : y ∈ ↑J
x : L
h₁ : ↑↑f x = y
⊢ y ∈ ↑(map f (comap f J))
[PROOFSTEP]
rw [← h₁] at h₂ ⊢
[GOAL]
case a.intro.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ↑R L' (LieHom.idealRange f) = LieHom.range f
y : L'
x : L
h₂ : ↑↑f x ∈ ↑J
h₁ : ↑↑f x = y
⊢ ↑↑f x ∈ ↑(map f (comap f J))
[PROOFSTEP]
exact mem_map h₂
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ↑(map f I) = ↑f '' ↑I
⊢ comap f (map f I) = I ⊔ LieHom.ker f
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, comap_coeSubmodule, I.map_coeSubmodule f h, LieSubmodule.sup_coe_toSubmodule,
  f.ker_coeSubmodule, Submodule.comap_map_eq]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ comap (incl I) I = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
m✝ : { x // x ∈ ↑I }
⊢ m✝ ∈ comap (incl I) I ↔ m✝ ∈ ⊤
[PROOFSTEP]
simp
  --  porting note: `ext; simp` works also in mathlib3, though the proof used to be
    --  rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.top_coeSubmodule,
    --    LieIdeal.comap_coeSubmodule, LieIdeal.incl_coe, Submodule.comap_subtype_self]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ LieHom.ker (incl I) = ⊥
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
m✝ : { x // x ∈ ↑I }
⊢ m✝ ∈ LieHom.ker (incl I) ↔ m✝ ∈ ⊥
[PROOFSTEP]
simp
  --  porting note: `ext; simp` works also in mathlib3, though the proof used to be
    --  rw [← LieSubmodule.coe_toSubmodule_eq_iff, I.incl.ker_coeSubmodule,
    --    LieSubmodule.bot_coeSubmodule, incl_coe, Submodule.ker_subtype]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ LieHom.idealRange (incl I) = I
[PROOFSTEP]
rw [LieHom.idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_to_submodule, ← LieSubmodule.coe_toSubmodule_eq_iff,
  incl_range, coe_to_lieSubalgebra_to_submodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ∃ N, ↑N = ↑I
[PROOFSTEP]
use I
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ LieHom.IsIdealMorphism (incl I)
[PROOFSTEP]
rw [I.incl.isIdealMorphism_def, incl_idealRange]
[GOAL]
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ↑R L I = LieHom.range (incl I)
[PROOFSTEP]
exact (I : LieSubalgebra R L).incl_range.symm
[GOAL]
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
⊢ ker f = ⊥ ↔ Function.Injective ↑f
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, ker_coeSubmodule, LieSubmodule.bot_coeSubmodule, LinearMap.ker_eq_bot,
  coe_toLinearMap]
[GOAL]
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
⊢ comp f (LieSubmodule.incl (ker f)) = 0
[PROOFSTEP]
ext ⟨m, hm⟩
[GOAL]
case h.mk
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ ↑(ker f)
⊢ ↑(comp f (LieSubmodule.incl (ker f))) { val := m, property := hm } = ↑0 { val := m, property := hm }
[PROOFSTEP]
exact (mem_ker m).mp hm
[GOAL]
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
M' : LieSubmodule R L M
⊢ M' ≤ ker f ↔ LieSubmodule.map f M' = ⊥
[PROOFSTEP]
rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]
[GOAL]
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
⊢ LieSubmodule.map f ⊤ = range f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m✝ : N
⊢ m✝ ∈ LieSubmodule.map f ⊤ ↔ m✝ ∈ range f
[PROOFSTEP]
simp [LieSubmodule.mem_map]
[GOAL]
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
N : LieSubmodule R L M
⊢ LieModuleHom.ker (incl N) = ⊥
[PROOFSTEP]
simp [← LieSubmodule.coe_toSubmodule_eq_iff]
[GOAL]
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
N : LieSubmodule R L M
⊢ LieModuleHom.range (incl N) = N
[PROOFSTEP]
simp [← LieSubmodule.coe_toSubmodule_eq_iff]
[GOAL]
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
N : LieSubmodule R L M
⊢ comap (incl N) N = ⊤
[PROOFSTEP]
simp [← LieSubmodule.coe_toSubmodule_eq_iff]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : { x // x ∈ ⊤ } →ₗ⁅R⁆ L := incl ⊤
x : { x // x ∈ ⊤ }
⊢ (fun x => { val := x, property := (_ : x ∈ Set.univ) })
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝,
              map_lie' :=
                (_ :
                  ∀ {x y : { x // x ∈ ⊤ }},
                    AddHom.toFun src✝.toAddHom ⁅x, y⁆ =
                      ⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆) }).toAddHom
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : { x // x ∈ ⊤ } →ₗ⁅R⁆ L := incl ⊤
x : { x // x ∈ ⊤ }
⊢ ↑((fun x => { val := x, property := (_ : x ∈ Set.univ) })
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝,
                map_lie' :=
                  (_ :
                    ∀ {x y : { x // x ∈ ⊤ }},
                      AddHom.toFun src✝.toAddHom ⁅x, y⁆ =
                        ⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆) }).toAddHom
          x)) =
    ↑x
[PROOFSTEP]
rfl
