[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ 0.carrier
_hy : y ∈ 0.carrier
⊢ ⁅x, y⁆ ∈ 0.carrier
[PROOFSTEP]
rw [(Submodule.mem_bot R).1 hx, zero_lie]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ 0.carrier
_hy : y ∈ 0.carrier
⊢ 0 ∈ 0.carrier
[PROOFSTEP]
exact Submodule.zero_mem 0
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L'' : LieSubalgebra R L
h : (fun L' => L'.carrier) L' = (fun L' => L'.carrier) L''
⊢ L' = L''
[PROOFSTEP]
rcases L' with ⟨⟨⟩⟩
[GOAL]
case mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L'' : LieSubalgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier
h :
  (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ } =
    (fun L' => L'.carrier) L''
⊢ { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ } = L''
[PROOFSTEP]
rcases L'' with ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier
h :
  (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }, lie_mem' := lie_mem'✝¹ } =
    (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ }
⊢ { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }, lie_mem' := lie_mem'✝¹ } =
    { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.mk.mk.e_toSubmodule.e_toAddSubmonoid
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier
h :
  (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }, lie_mem' := lie_mem'✝¹ } =
    (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : { x // x ∈ L' }), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ⁅x✝ + y✝, z✝⁆ = ⁅x✝, z✝⁆ + ⁅y✝, z✝⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ↑⁅x✝ + y✝, z✝⁆ = ↑(⁅x✝, z✝⁆ + ⁅y✝, z✝⁆)
[PROOFSTEP]
apply add_lie
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : { x // x ∈ L' }), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ⁅x✝, y✝ + z✝⁆ = ⁅x✝, y✝⁆ + ⁅x✝, z✝⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, y✝ + z✝⁆ = ↑(⁅x✝, y✝⁆ + ⁅x✝, z✝⁆)
[PROOFSTEP]
apply lie_add
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x : { x // x ∈ L' }), ⁅x, x⁆ = 0
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : { x // x ∈ L' }
⊢ ⁅x✝, x✝⁆ = 0
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, x✝⁆ = ↑0
[PROOFSTEP]
apply lie_self
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : { x // x ∈ L' }), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ⁅x✝, ⁅y✝, z✝⁆⁆ = ⁅⁅x✝, y✝⁆, z✝⁆ + ⁅y✝, ⁅x✝, z✝⁆⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, ⁅y✝, z✝⁆⁆ = ↑(⁅⁅x✝, y✝⁆, z✝⁆ + ⁅y✝, ⁅x✝, z✝⁆⁆)
[PROOFSTEP]
apply leibniz_lie
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : { x // x ∈ L' }), ⁅x, t • y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
{ intros
  apply SetCoe.ext
  apply lie_smul
}
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : { x // x ∈ L' }), ⁅x, t • y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : { x // x ∈ L' }
⊢ ⁅x✝, t✝ • y✝⁆ = t✝ • ⁅x✝, y✝⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, t✝ • y✝⁆ = ↑(t✝ • ⁅x✝, y✝⁆)
[PROOFSTEP]
apply lie_smul
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
p : Submodule R L
h :
  ∀ {x y : L},
    x ∈
        { toAddSubmonoid := p.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈
          { toAddSubmonoid := p.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := p.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ {
        toSubmodule :=
          { toAddSubmonoid := p.toAddSubmonoid,
            smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) },
        lie_mem' := h }.toSubmodule =
    p
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x y : L},
    x ∈
        { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : L},
                      x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                        c • x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' :=
                                    smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈
          { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L},
                        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, y⁆ ∈
          { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L},
                        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 : L},
                  x ∈
                      { toAddSubmonoid := toAddSubmonoid✝,
                              smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                    c • x ∈
                      { toAddSubmonoid := toAddSubmonoid✝,
                              smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) },
        lie_mem' := h }.toSubmodule =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'
[PROOFSTEP]
rw [SetLike.ext'_iff] at h 
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L₁' L₂' : LieSubalgebra R L
h✝ : L₁'.toSubmodule = L₂'.toSubmodule
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'
[PROOFSTEP]
rw [← coe_set_eq]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L₁' L₂' : LieSubalgebra R L
h✝ : L₁'.toSubmodule = L₂'.toSubmodule
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'
[PROOFSTEP]
exact h
[GOAL]
R : Type u
L : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRingModule L M
N : Type w₁
inst✝⁵ : AddCommGroup N
inst✝⁴ : LieRingModule L N
inst✝³ : Module R N
inst✝² : LieModule R L N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : { x // x ∈ L' }
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
simp only [coe_bracket_of_module, smul_lie, Submodule.coe_smul_of_tower]
[GOAL]
R : Type u
L : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRingModule L M
N : Type w₁
inst✝⁵ : AddCommGroup N
inst✝⁴ : LieRingModule L N
inst✝³ : Module R N
inst✝² : LieModule R L N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : { x // x ∈ L' }
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
simp only [coe_bracket_of_module, lie_smul]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : Submodule R L₂ := LinearMap.range ↑f
⊢ ∀ {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]
rintro - - ⟨x, rfl⟩ ⟨y, rfl⟩
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : Submodule R L₂ := LinearMap.range ↑f
x y : L
⊢ ⁅↑↑f x, ↑↑f y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact ⟨⁅x, y⁆, f.map_lie x y⟩
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : L →ₗ[R] { x // x ∈ LinearMap.range ↑f } := LinearMap.rangeRestrict ↑f
x y : L
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : L →ₗ[R] { x // x ∈ LinearMap.range ↑f } := LinearMap.rangeRestrict ↑f
x y : L
⊢ ↑(AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        ⁅x, y⁆) =
    ↑⁅AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          x,
        AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          y⁆
[PROOFSTEP]
exact f.map_lie x y
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ Function.Surjective ↑(rangeRestrict f)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy }
[PROOFSTEP]
erw [mem_range] at hy 
[GOAL]
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ range f
hy : ∃ y_1, ↑f y_1 = y
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy✝ }
[PROOFSTEP]
obtain ⟨x, rfl⟩ := hy
[GOAL]
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := ↑f x, property := hy }
[PROOFSTEP]
use x
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ↑(rangeRestrict f) x = { val := ↑f x, property := hy }
[PROOFSTEP]
simp only [Subtype.mk_eq_mk, rangeRestrict_apply]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective ↑f
x y : L
hxy : ↑(rangeRestrict f) x = ↑(rangeRestrict f) y
⊢ x = y
[PROOFSTEP]
simp only [Subtype.mk_eq_mk, rangeRestrict_apply] at hxy 
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective ↑f
x y : L
hxy : ↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
exact h hxy
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
rintro ⟨K, rfl⟩ _ _
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K : LieSubalgebra R L
x✝ y✝ : L
⊢ x✝ ∈ K.toSubmodule → y✝ ∈ K.toSubmodule → ⁅x✝, y✝⁆ ∈ K.toSubmodule
[PROOFSTEP]
exact K.lie_mem'
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ K, K.toSubmodule = p
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ K, K.toSubmodule = p
[PROOFSTEP]
use{ p with lie_mem' := h _ _ }
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ LieHom.range (incl K) = K
[PROOFSTEP]
rw [← coe_to_submodule_eq_iff]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ (LieHom.range (incl K)).toSubmodule = K.toSubmodule
[PROOFSTEP]
exact (K : Submodule R L).range_subtype
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hx :
  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]
erw [Submodule.mem_map] at hx 
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hx : ∃ y, y ∈ K.toSubmodule ∧ ↑↑f y = x
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]
rcases hx with ⟨x', hx', hx⟩
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.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' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [← hx]
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.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' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
⊢ ⁅↑↑f x', y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
erw [Submodule.mem_map] at hy 
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hy : ∃ y_1, y_1 ∈ K.toSubmodule ∧ ↑↑f y_1 = y
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
⊢ ⁅↑↑f x', y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rcases hy with ⟨y', hy', hy⟩
[GOAL]
case intro.intro.intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
y' : L
hy' : y' ∈ K.toSubmodule
hy : ↑↑f y' = y
⊢ ⁅↑↑f x', y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [← hy]
[GOAL]
case intro.intro.intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
y' : L
hy' : y' ∈ K.toSubmodule
hy : ↑↑f y' = y
⊢ ⁅↑↑f x', ↑↑f y'⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
erw [Submodule.mem_map]
[GOAL]
case intro.intro.intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
y' : L
hy' : y' ∈ K.toSubmodule
hy : ↑↑f y' = y
⊢ ∃ y, y ∈ K.toSubmodule ∧ ↑↑f y = ⁅↑↑f x', ↑↑f y'⁆
[PROOFSTEP]
exact ⟨⁅x', y'⁆, K.lie_mem hx' hy', f.map_lie x' y'⟩
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L := Submodule.comap (↑f) K₂.toSubmodule
x y : L
hx :
  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]
suffices ⁅f x, f y⁆ ∈ K₂ by simp [this]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L := Submodule.comap (↑f) K₂.toSubmodule
x y : L
hx :
  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
this : ⁅↑f x, ↑f y⁆ ∈ K₂
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L := Submodule.comap (↑f) K₂.toSubmodule
x y : L
hx :
  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
⊢ ⁅↑f x, ↑f y⁆ ∈ K₂
[PROOFSTEP]
exact K₂.lie_mem hx hy
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ LieHom.range f = map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x✝ : L₂
⊢ x✝ ∈ LieHom.range f ↔ x✝ ∈ map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
src✝ : Submodule R L := sInf {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}
x y : L
hx :
  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]
simp only [Submodule.mem_carrier, mem_iInter, Submodule.sInf_coe, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp,
  and_imp] at hx hy ⊢
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
src✝ : Submodule R L := sInf {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}
x y : L
hx : ∀ (a : LieSubalgebra R L), a ∈ S → x ∈ ↑a.toSubmodule
hy : ∀ (a : LieSubalgebra R L), a ∈ S → y ∈ ↑a.toSubmodule
⊢ ∀ (a : LieSubalgebra R L), a ∈ S → ⁅x, y⁆ ∈ ↑a.toSubmodule
[PROOFSTEP]
intro K hK
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
src✝ : Submodule R L := sInf {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}
x y : L
hx : ∀ (a : LieSubalgebra R L), a ∈ S → x ∈ ↑a.toSubmodule
hy : ∀ (a : LieSubalgebra R L), a ∈ S → y ∈ ↑a.toSubmodule
K : LieSubalgebra R L
hK : K ∈ S
⊢ ⁅x, y⁆ ∈ ↑K.toSubmodule
[PROOFSTEP]
exact K.lie_mem (hx K hK) (hy K hK)
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ↑(sInf S) = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
[PROOFSTEP]
rw [← coe_to_submodule, sInf_coe_to_submodule, Submodule.sInf_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x : L
⊢ x ∈ ⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p ↔
    x ∈ ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ IsGLB S (sInf S)
[PROOFSTEP]
have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' :=
  by
  intros
  exact Iff.rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
K✝ K'✝ : LieSubalgebra R L
⊢ ↑K✝ ≤ ↑K'✝ ↔ K✝ ≤ K'✝
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB S (sInf S)
[PROOFSTEP]
apply IsGLB.of_image @h
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB ((fun x => ↑x) '' S) ↑(sInf S)
[PROOFSTEP]
simp only [sInf_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB ((fun x => ↑x) '' S) (⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s)
[PROOFSTEP]
exact isGLB_biInf
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : CompleteLattice (LieSubalgebra R L) :=
  completeLatticeOfInf (LieSubalgebra R L) (_ : ∀ (S : Set (LieSubalgebra R L)), IsGLB S (sInf S))
N : LieSubalgebra R L
x✝ : L
h : x✝ ∈ ⊥
⊢ x✝ ∈ N
[PROOFSTEP]
rw [mem_bot] at h 
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : CompleteLattice (LieSubalgebra R L) :=
  completeLatticeOfInf (LieSubalgebra R L) (_ : ∀ (S : Set (LieSubalgebra R L)), IsGLB S (sInf S))
N : LieSubalgebra R L
x✝ : L
h : x✝ = 0
⊢ x✝ ∈ N
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : CompleteLattice (LieSubalgebra R L) :=
  completeLatticeOfInf (LieSubalgebra R L) (_ : ∀ (S : Set (LieSubalgebra R L)), IsGLB S (sInf S))
N : LieSubalgebra R L
x✝ : L
h : x✝ = 0
⊢ 0 ∈ N
[PROOFSTEP]
exact N.zero_mem'
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
[PROOFSTEP]
rw [← mem_coe_submodule, ← mem_coe_submodule, ← mem_coe_submodule, inf_coe_to_submodule, Submodule.mem_inf]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ K = ⊥ ↔ ∀ (x : L), x ∈ K → x = 0
[PROOFSTEP]
rw [_root_.eq_bot_iff]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ K ≤ ⊥ ↔ ∀ (x : L), x ∈ K → x = 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Subsingleton (LieSubalgebra R { x // x ∈ ⊥ })
[PROOFSTEP]
apply subsingleton_of_bot_eq_top
[GOAL]
case hα
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ ⊥ = ⊤
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case hα.h.mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
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
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : x ∈ ⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
rw [LieSubalgebra.mem_bot] at hx 
[GOAL]
case hα.h.mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra 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
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra 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, mem_bot, mem_top]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Subsingleton ↑↑⊥
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x y : { x // x ∈ K }
⊢ ↑(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
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ x ∈ ofLe h ↔ ↑x ∈ K
[PROOFSTEP]
simp only [ofLe, homOfLe_apply, LieHom.mem_range]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ (∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x) ↔ ↑x ∈ K
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ (∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x) → ↑x ∈ K
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
y : { x // x ∈ K }
⊢ ↑{ val := ↑y, property := (_ : ↑y ∈ K') } ∈ K
[PROOFSTEP]
exact y.property
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ ↑x ∈ K → ∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h✝ : K ≤ K'
x : { x // x ∈ K' }
h : ↑x ∈ K
⊢ ∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x
[PROOFSTEP]
use⟨(x : L), h⟩
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
⊢ ofLe h = comap (incl K') K
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x✝ : { x // x ∈ K' }
⊢ x✝ ∈ ofLe h ↔ x✝ ∈ comap (incl K') K
[PROOFSTEP]
rw [mem_ofLe]
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x✝ : { x // x ∈ K' }
⊢ ↑x✝ ∈ K ↔ x✝ ∈ comap (incl K') K
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
x : L
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
[PROOFSTEP]
change x ∈ (lieSpan R L s : Set L) ↔ _
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
x : L
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
[PROOFSTEP]
erw [sInf_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
x : L
⊢ x ∈ ⋂ (s_1 : LieSubalgebra R L) (_ : s_1 ∈ {N | s ⊆ ↑N}), ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
[PROOFSTEP]
exact Set.mem_iInter₂
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
⊢ s ⊆ ↑(lieSpan R L s)
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
m : L
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)
[PROOFSTEP]
erw [mem_lieSpan]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
m : L
hm : m ∈ s
⊢ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
[PROOFSTEP]
intro K hK
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ ↑K
⊢ m ∈ K
[PROOFSTEP]
exact hK hm
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
⊢ s ⊆ ↑(lieSpan R L s).toSubmodule
[PROOFSTEP]
apply subset_lieSpan
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ ↑K
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K → s ⊆ ↑K
[PROOFSTEP]
exact Set.Subset.trans subset_lieSpan
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
⊢ s ⊆ ↑K → lieSpan R L s ≤ K
[PROOFSTEP]
intro hs m hm
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : m ∈ lieSpan R L s
⊢ m ∈ K
[PROOFSTEP]
rw [mem_lieSpan] at hm 
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
⊢ m ∈ K
[PROOFSTEP]
exact hm _ hs
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s t : Set L
h : s ⊆ t
⊢ lieSpan R L s ≤ lieSpan R L t
[PROOFSTEP]
rw [lieSpan_le]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s t : Set L
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)
[PROOFSTEP]
exact Set.Subset.trans h subset_lieSpan
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p
[PROOFSTEP]
rw [p.exists_lieSubalgebra_coe_eq_iff]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → (lieSpan R L ↑p).toSubmodule = p
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
⊢ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
intro x m hm
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
rw [← h, mem_coe_submodule]
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ lieSpan R L ↑p → ⁅x, m⁆ ∈ (lieSpan R L ↑p).toSubmodule
[PROOFSTEP]
exact lie_mem _ (subset_lieSpan hm)
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (lieSpan R L ↑p).toSubmodule = p
[PROOFSTEP]
rw [← coe_to_submodule_mk p @h, coe_to_submodule, coe_to_submodule_eq_iff, lieSpan_eq]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h : Function.Injective ↑f
⊢ Function.Injective ↑↑f
[PROOFSTEP]
rwa [LieHom.coe_toLinearMap]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
⊢ L₁'.toSubmodule = L₁''.toSubmodule
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
x : L₁
⊢ x ∈ L₁'.toSubmodule ↔ x ∈ L₁''.toSubmodule
[PROOFSTEP]
change x ∈ (L₁' : Set L₁) ↔ x ∈ (L₁'' : Set L₁)
[GOAL]
case h
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
x : L₁
⊢ x ∈ ↑L₁' ↔ x ∈ ↑L₁''
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
src✝ : { x // x ∈ L₁''.toSubmodule } ≃ₗ[R] { x // x ∈ Submodule.map (↑(toLinearEquiv e)) L₁''.toSubmodule } :=
  LinearEquiv.submoduleMap (toLinearEquiv e) L₁''.toSubmodule
x y : { x // x ∈ L₁'' }
⊢ AddHom.toFun src✝.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
src✝ : { x // x ∈ L₁''.toSubmodule } ≃ₗ[R] { x // x ∈ Submodule.map (↑(toLinearEquiv e)) L₁''.toSubmodule } :=
  LinearEquiv.submoduleMap (toLinearEquiv e) L₁''.toSubmodule
x y : { x // x ∈ L₁'' }
⊢ ↑(AddHom.toFun src✝.toAddHom ⁅x, y⁆) = ↑⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
exact LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = L₂'.toSubmodule
[PROOFSTEP]
rw [← h]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = (LieSubalgebra.map e.toLieHom L₁').toSubmodule
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
src✝ : { x // x ∈ L₁'.toSubmodule } ≃ₗ[R] { x // x ∈ L₂'.toSubmodule } :=
  LinearEquiv.ofSubmodules (toLinearEquiv e) L₁'.toSubmodule L₂'.toSubmodule
    (_ : Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = L₂'.toSubmodule)
x y : { x // x ∈ L₁' }
⊢ AddHom.toFun src✝.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
src✝ : { x // x ∈ L₁'.toSubmodule } ≃ₗ[R] { x // x ∈ L₂'.toSubmodule } :=
  LinearEquiv.ofSubmodules (toLinearEquiv e) L₁'.toSubmodule L₂'.toSubmodule
    (_ : Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = L₂'.toSubmodule)
x y : { x // x ∈ L₁' }
⊢ ↑(AddHom.toFun src✝.toAddHom ⁅x, y⁆) = ↑⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
exact LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y
