mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝¹ x✝ : L
⊢ {
      toFun := fun y ↦
        {
          toFun := fun z ↦
            ⁅x✝¹ + x✝, (a y) z⁆ - ⁅y, (a (x✝¹ + x✝)) z⁆ + ⁅z, (a (x✝¹ + x✝)) y⁆ - (a ⁅x✝¹ + x✝, y⁆) z +
                (a ⁅x✝¹ + x✝, z⁆) y -
              (a ⁅y, z⁆) (x✝¹ + x✝),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝¹, (a y) z⁆ - ⁅y, (a x✝¹) z⁆ + ⁅z, (a x✝¹) y⁆ - (a ⁅x✝¹, y⁆) z + (a ⁅x✝¹, z⁆) y - (a ⁅y, z⁆) x✝¹,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ } +
      {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝, (a y) z⁆ - ⁅y, (a x✝) z⁆ + ⁅z, (a x✝) y⁆ - (a ⁅x✝, y⁆) z + (a ⁅x✝, z⁆) y - (a ⁅y, z⁆) x✝,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ x✝² x✝¹ x✝ : L
⊢ ({
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x✝³ + x✝², (a y) z⁆ - ⁅y, (a (x✝³ + x✝²)) z⁆ + ⁅z, (a (x✝³ + x✝²)) y⁆ - (a ⁅x✝³ + x✝², y⁆) z +
                    (a ⁅x✝³ + x✝², z⁆) y -
                  (a ⁅y, z⁆) (x✝³ + x✝²),
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ }
        x✝¹)
      x✝ =
    (({
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝³, (a y) z⁆ - ⁅y, (a x✝³) z⁆ + ⁅z, (a x✝³) y⁆ - (a ⁅x✝³, y⁆) z + (a ⁅x✝³, z⁆) y - (a ⁅y, z⁆) x✝³,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } +
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝², (a y) z⁆ - ⁅y, (a x✝²) z⁆ + ⁅z, (a x✝²) y⁆ - (a ⁅x✝², y⁆) z + (a ⁅x✝², z⁆) y - (a ⁅y, z⁆) x✝²,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun y ↦
        {
          toFun := fun z ↦
            ⁅x✝¹ • x✝, (a y) z⁆ - ⁅y, (a (x✝¹ • x✝)) z⁆ + ⁅z, (a (x✝¹ • x✝)) y⁆ - (a ⁅x✝¹ • x✝, y⁆) z +
                (a ⁅x✝¹ • x✝, z⁆) y -
              (a ⁅y, z⁆) (x✝¹ • x✝),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝, (a y) z⁆ - ⁅y, (a x✝) z⁆ + ⁅z, (a x✝) y⁆ - (a ⁅x✝, y⁆) z + (a ⁅x✝, z⁆) y - (a ⁅y, z⁆) x✝,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ ({
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x✝³ • x✝², (a y) z⁆ - ⁅y, (a (x✝³ • x✝²)) z⁆ + ⁅z, (a (x✝³ • x✝²)) y⁆ - (a ⁅x✝³ • x✝², y⁆) z +
                    (a ⁅x✝³ • x✝², z⁆) y -
                  (a ⁅y, z⁆) (x✝³ • x✝²),
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ }
        x✝¹)
      x✝ =
    (((RingHom.id R) x✝³ •
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝², (a y) z⁆ - ⁅y, (a x✝²) z⁆ + ⁅z, (a x✝²) y⁆ - (a ⁅x✝², y⁆) z + (a ⁅x✝², z⁆) y - (a ⁅y, z⁆) x✝²,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝¹ : R
x✝ : ↥(twoCochain R L M)
⊢ {
      toFun := fun x ↦
        {
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x, ((x✝¹ • x✝) y) z⁆ - ⁅y, ((x✝¹ • x✝) x) z⁆ + ⁅z, ((x✝¹ • x✝) x) y⁆ - ((x✝¹ • x✝) ⁅x, y⁆) z +
                    ((x✝¹ • x✝) ⁅x, z⁆) y -
                  ((x✝¹ • x✝) ⁅y, z⁆) x,
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun x ↦
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x, (x✝ y) z⁆ - ⁅y, (x✝ x) z⁆ + ⁅z, (x✝ x) y⁆ - (x✝ ⁅x, y⁆) z + (x✝ ⁅x, z⁆) y - (x✝ ⁅y, z⁆) x,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝⁴ : R
x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ (({
            toFun := fun x ↦
              {
                toFun := fun y ↦
                  {
                    toFun := fun z ↦
                      ⁅x, ((x✝⁴ • x✝³) y) z⁆ - ⁅y, ((x✝⁴ • x✝³) x) z⁆ + ⁅z, ((x✝⁴ • x✝³) x) y⁆ -
                            ((x✝⁴ • x✝³) ⁅x, y⁆) z +
                          ((x✝⁴ • x✝³) ⁅x, z⁆) y -
                        ((x✝⁴ • x✝³) ⁅y, z⁆) x,
                    map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          x✝²)
        x✝¹)
      x✝ =
    ((((RingHom.id R) x✝⁴ •
            {
              toFun := fun x ↦
                {
                  toFun := fun y ↦
                    {
                      toFun := fun z ↦
                        ⁅x, (x✝³ y) z⁆ - ⁅y, (x✝³ x) z⁆ + ⁅z, (x✝³ x) y⁆ - (x✝³ ⁅x, y⁆) z + (x✝³ ⁅x, z⁆) y -
                          (x✝³ ⁅y, z⁆) x,
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ })
          x✝²)
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ a ∈ twoCocycle R L M ↔ ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ a ∈ twoCocycle R L M → ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ (∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆) → a ∈ twoCocycle R L M
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ x ∈ couple R A A' ↔ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ x ∈ couple R A A' → ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2

case mpr
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2 → x ∈ couple R A A'
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : Derivation R A A
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    { toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
      { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : Derivation R A A
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ({ toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
        { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ })
      a✝
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ : R
x✝ : Derivation R A A
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    (RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ : R
x✝ : Derivation R A A
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ((RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }) a✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ mapRange (fun x_1 m' ↦ ⁅x + y, m'⁆) ⋯ m = mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m + mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ m

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
i✝ : ι
⊢ (mapRange (fun x_1 m' ↦ ⁅x + y, m'⁆) ⋯ m) i✝ =
    (mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m + mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ m) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x : L
m n : ⨁ (i : ι), M i
⊢ mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ (m + n) = mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m + mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ n

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x : L
m n : ⨁ (i : ι), M i
i✝ : ι
⊢ (mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ (m + n)) i✝ =
    (mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m + mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ n) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ (mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ m) =
    mapRange (fun x_1 m' ↦ ⁅⁅x, y⁆, m'⁆) ⋯ m + mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ (mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m)

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
i✝ : ι
⊢ (mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ (mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ m)) i✝ =
    (mapRange (fun x_1 m' ↦ ⁅⁅x, y⁆, m'⁆) ⋯ m + mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ (mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m))
      i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
i✝ : ι
⊢ ⁅t • x, m⁆ i✝ = (t • ⁅x, m⁆) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
i✝ : ι
⊢ ⁅x, t • m⁆ i✝ = (t • ⁅x, m⁆) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
⊢ (lof R ι M j).toFun ⁅x, m⁆ = ⁅x, (lof R ι M j).toFun m⁆

Tactic:
by
      ext i
      by_cases h : j = i
      · rw [← h]; simp
      · -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
        -- old proof `simp [lof, lsingle, h]`
        simp only [lof, lsingle, AddHom.toFun_eq_coe, lie_module_bracket_apply]
        -- The coercion in the goal is `DFunLike.coe (β := fun x ↦ Π₀ (i : ι), M i)`
        -- but the lemma is expecting `DFunLike.coe (β := fun x ↦ ⨁ (i : ι), M i)`
        erw [AddHom.coe_mk]
        simp [h]

Goal state after:
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
⊢ zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ (x + y) z =
    zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z + zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y z

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
i✝ : ι
⊢ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ (x + y) z) i✝ =
    (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z + zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y z) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
⊢ zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x (y + z) =
    zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x y + zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
i✝ : ι
⊢ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x (y + z)) i✝ =
    (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x y + zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x : ⨁ (i : ι), L i
⊢ zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x x = 0

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x : ⨁ (i : ι), L i
i✝ : ι
⊢ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x x) i✝ = 0 i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
⊢ zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y z) =
    zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x y) z +
      zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z)

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
i✝ : ι
⊢ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y z)) i✝ =
    (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x y) z +
        zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z))
      i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
c : R
x y : ⨁ (i : ι), L i
⊢ ⁅x, c • y⁆ = c • ⁅x, y⁆

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
c : R
x y : ⨁ (i : ι), L i
i✝ : ι
⊢ ⁅x, c • y⁆ i✝ = (c • ⁅x, y⁆) i✝
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
c : R
x y : ⨁ (i : ι), L i
⊢ ⁅x, c • y⁆ = c • ⁅x, y⁆

Tactic:
ext
      simp only [smul_apply, bracket_apply, lie_smul]

Goal state after:
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inl
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i : ι
y x : L i
⊢ ↑(f i) ⁅x, y⁆ = ⁅↑(f i) x, ↑(f i) y⁆

Tactic:
LieHom.coe_toLinearMap,

Goal state after:
case inl
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i : ι
y x : L i
⊢ (f i) ⁅x, y⁆ = ⁅(f i) x, (f i) y⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inr
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ 0 = ⁅↑(f j) x, ↑(f i) y⁆

Tactic:
LieHom.coe_toLinearMap,

Goal state after:
case inr
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ 0 = ⁅(f j) x, (f i) y⁆
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
⊢ M.det = 1

Tactic:
set A := M.toBlocks₁₁

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
⊢ M.det = 1
Module: Mathlib.Algebra.Lie.UniversalEnveloping

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
⊢ (fun F ↦ F.toLieHom.comp (ι R)) ((fun f ↦ (ringCon R L).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) f) = f

Tactic:
ext

Goal state after:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ((fun F ↦ F.toLieHom.comp (ι R)) ((fun f ↦ (ringCon R L).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) f)) x✝ = f x✝
Module: Mathlib.Algebra.Lie.UniversalEnveloping

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ((fun f ↦ (ringCon R L).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) ((fun F ↦ F.toLieHom.comp (ι R)) F)).comp
      (RingCon.mkₐ R (ringCon R L)) =
    F.comp (RingCon.mkₐ R (ringCon R L))

Tactic:
ext

Goal state after:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
x✝ : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)