[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ↑χ ⁅x, y⁆ = 0
[PROOFSTEP]
rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ⁅↑χ x, ↑χ y⁆ = 0
[PROOFSTEP]
rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ derivedSeries R L 1
⊢ ↑χ x = 0
[PROOFSTEP]
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ← LieSubmodule.mem_coeSubmodule,
  LieSubmodule.lieIdeal_oper_eq_linear_span] at h 
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ x = 0
[PROOFSTEP]
refine' Submodule.span_induction h _ _ _ _
[GOAL]
case refine'_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x : L), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → ↑χ x = 0
[PROOFSTEP]
rintro y ⟨⟨z, hz⟩, ⟨⟨w, hw⟩, rfl⟩⟩
[GOAL]
case refine'_1.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
z : L
hz : z ∈ ⊤
w : L
hw : w ∈ ⊤
⊢ ↑χ ⁅↑{ val := z, property := hz }, ↑{ val := w, property := hw }⁆ = 0
[PROOFSTEP]
apply lieCharacter_apply_lie
[GOAL]
case refine'_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ 0 = 0
[PROOFSTEP]
exact χ.map_zero
[GOAL]
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x y : L), ↑χ x = 0 → ↑χ y = 0 → ↑χ (x + y) = 0
[PROOFSTEP]
intro y z hy hz
[GOAL]
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
y z : L
hy : ↑χ y = 0
hz : ↑χ z = 0
⊢ ↑χ (y + z) = 0
[PROOFSTEP]
rw [LieHom.map_add, hy, hz, add_zero]
[GOAL]
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (a : R) (x : L), ↑χ x = 0 → ↑χ (a • x) = 0
[PROOFSTEP]
intro t y hy
[GOAL]
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
t : R
y : L
hy : ↑χ y = 0
⊢ ↑χ (t • y) = 0
[PROOFSTEP]
rw [LieHom.map_smul, hy, smul_zero]
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x y : L
⊢ AddHom.toFun
      { toAddHom := ψ.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := ψ.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := ψ.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self, LinearMap.toFun_eq_coe,
  LinearMap.map_zero]
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
χ : LieCharacter R L
⊢ (fun ψ =>
        {
          toLinearMap :=
            { toAddHom := ψ.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L), AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
          map_lie' :=
            (_ :
              ∀ {x y : L},
                AddHom.toFun
                    { toAddHom := ψ.toAddHom,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : L),
                              AddHom.toFun ψ.toAddHom (r • x) =
                                ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                    ⁅x, y⁆ =
                  ⁅AddHom.toFun
                      { toAddHom := ψ.toAddHom,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : L),
                                AddHom.toFun ψ.toAddHom (r • x) =
                                  ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                      x,
                    AddHom.toFun
                      { toAddHom := ψ.toAddHom,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : L),
                                AddHom.toFun ψ.toAddHom (r • x) =
                                  ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                      y⁆) })
      ((fun χ => ↑χ) χ) =
    χ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
χ : LieCharacter R L
x✝ : L
⊢ ↑((fun ψ =>
            {
              toLinearMap :=
                { toAddHom := ψ.toAddHom,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : L),
                        AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
              map_lie' :=
                (_ :
                  ∀ {x y : L},
                    AddHom.toFun
                        { toAddHom := ψ.toAddHom,
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : L),
                                  AddHom.toFun ψ.toAddHom (r • x) =
                                    ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                        ⁅x, y⁆ =
                      ⁅AddHom.toFun
                          { toAddHom := ψ.toAddHom,
                              map_smul' :=
                                (_ :
                                  ∀ (r : R) (x : L),
                                    AddHom.toFun ψ.toAddHom (r • x) =
                                      ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                          x,
                        AddHom.toFun
                          { toAddHom := ψ.toAddHom,
                              map_smul' :=
                                (_ :
                                  ∀ (r : R) (x : L),
                                    AddHom.toFun ψ.toAddHom (r • x) =
                                      ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                          y⁆) })
          ((fun χ => ↑χ) χ))
      x✝ =
    ↑χ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
⊢ (fun χ => ↑χ)
      ((fun ψ =>
          {
            toLinearMap :=
              { toAddHom := ψ.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L),
                      AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
            map_lie' :=
              (_ :
                ∀ {x y : L},
                  AddHom.toFun
                      { toAddHom := ψ.toAddHom,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : L),
                                AddHom.toFun ψ.toAddHom (r • x) =
                                  ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                      ⁅x, y⁆ =
                    ⁅AddHom.toFun
                        { toAddHom := ψ.toAddHom,
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : L),
                                  AddHom.toFun ψ.toAddHom (r • x) =
                                    ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                        x,
                      AddHom.toFun
                        { toAddHom := ψ.toAddHom,
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : L),
                                  AddHom.toFun ψ.toAddHom (r • x) =
                                    ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                        y⁆) })
        ψ) =
    ψ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x✝ : L
⊢ ↑((fun χ => ↑χ)
          ((fun ψ =>
              {
                toLinearMap :=
                  { toAddHom := ψ.toAddHom,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : L),
                          AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
                map_lie' :=
                  (_ :
                    ∀ {x y : L},
                      AddHom.toFun
                          { toAddHom := ψ.toAddHom,
                              map_smul' :=
                                (_ :
                                  ∀ (r : R) (x : L),
                                    AddHom.toFun ψ.toAddHom (r • x) =
                                      ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                          ⁅x, y⁆ =
                        ⁅AddHom.toFun
                            { toAddHom := ψ.toAddHom,
                                map_smul' :=
                                  (_ :
                                    ∀ (r : R) (x : L),
                                      AddHom.toFun ψ.toAddHom (r • x) =
                                        ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                            x,
                          AddHom.toFun
                            { toAddHom := ψ.toAddHom,
                                map_smul' :=
                                  (_ :
                                    ∀ (r : R) (x : L),
                                      AddHom.toFun ψ.toAddHom (r • x) =
                                        ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                            y⁆) })
            ψ))
      x✝ =
    ↑ψ x✝
[PROOFSTEP]
rfl
