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
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✝

Tactic:
;

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
x✝⁴ : R
x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ x✝⁴ • ⁅x✝², (x✝³ x✝¹) x✝⁆ - x✝⁴ • ⁅x✝¹, (x✝³ x✝²) x✝⁆ + x✝⁴ • ⁅x✝, (x✝³ x✝²) x✝¹⁆ - x✝⁴ • (x✝³ ⁅x✝², x✝¹⁆) x✝ +
        x✝⁴ • (x✝³ ⁅x✝², x✝⁆) x✝¹ -
      x✝⁴ • (x✝³ ⁅x✝¹, x✝⁆) x✝² =
    x✝⁴ •
      (⁅x✝², (x✝³ x✝¹) x✝⁆ - ⁅x✝¹, (x✝³ x✝²) x✝⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆ - (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝⁆) x✝¹ -
        (x✝³ ⁅x✝¹, x✝⁆) x✝²)

Tactic:
;

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
⊢ x✝⁴ • ⁅x✝², (x✝³ x✝¹) x✝⁆ - x✝⁴ • ⁅x✝¹, (x✝³ x✝²) x✝⁆ + x✝⁴ • ⁅x✝, (x✝³ x✝²) x✝¹⁆ - x✝⁴ • (x✝³ ⁅x✝², x✝¹⁆) x✝ +
        x✝⁴ • (x✝³ ⁅x✝², x✝⁆) x✝¹ -
      x✝⁴ • (x✝³ ⁅x✝¹, x✝⁆) x✝² =
    x✝⁴ •
      (⁅x✝², (x✝³ x✝¹) x✝⁆ - ⁅x✝¹, (x✝³ x✝²) x✝⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆ - (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝⁆) x✝¹ -
        (x✝³ ⁅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
x✝⁴ : R
x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ x✝⁴ • ⁅x✝², (x✝³ x✝¹) x✝⁆ +
      (-1 • x✝⁴ • ⁅x✝¹, (x✝³ x✝²) x✝⁆ +
        (x✝⁴ • ⁅x✝, (x✝³ x✝²) x✝¹⁆ +
          (-1 • x✝⁴ • (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝⁴ • (x✝³ ⁅x✝², x✝⁆) x✝¹ + -1 • x✝⁴ • (x✝³ ⁅x✝¹, x✝⁆) x✝²)))) =
    x✝⁴ •
      (⁅x✝², (x✝³ x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (x✝³ x✝²) x✝⁆ +
          (⁅x✝, (x✝³ x✝²) x✝¹⁆ + (-1 • (x✝³ ⁅x✝², x✝¹⁆) x✝ + ((x✝³ ⁅x✝², x✝⁆) x✝¹ + -1 • (x✝³ ⁅x✝¹, x✝⁆) x✝²)))))

Tactic:
;

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
⊢ x✝⁴ • ⁅x✝², (x✝³ x✝¹) x✝⁆ +
      (-1 • x✝⁴ • ⁅x✝¹, (x✝³ x✝²) x✝⁆ +
        (x✝⁴ • ⁅x✝, (x✝³ x✝²) x✝¹⁆ +
          (-1 • x✝⁴ • (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝⁴ • (x✝³ ⁅x✝², x✝⁆) x✝¹ + -1 • x✝⁴ • (x✝³ ⁅x✝¹, x✝⁆) x✝²)))) =
    x✝⁴ •
      (⁅x✝², (x✝³ x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (x✝³ x✝²) x✝⁆ +
          (⁅x✝, (x✝³ x✝²) x✝¹⁆ + (-1 • (x✝³ ⁅x✝², x✝¹⁆) x✝ + ((x✝³ ⁅x✝², x✝⁆) x✝¹ + -1 • (x✝³ ⁅x✝¹, x✝⁆) x✝²)))))
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
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d + e, f⁆ a = (⁅d, f⁆ + ⁅e, f⁆) a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d + e, f⁆ a = (⁅d, f⁆ + ⁅e, f⁆) a
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
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (f a) + e (f a) - (f (d a) + f (e a)) = d (f a) - f (d a) + (e (f a) - f (e a))

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (f a) + e (f a) - (f (d a) + f (e a)) = d (f a) - f (d a) + (e (f a) - f (e a))
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
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d, e + f⁆ a = (⁅d, e⁆ + ⁅d, f⁆) a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d, e + f⁆ a = (⁅d, e⁆ + ⁅d, f⁆) a
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
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (e a) + d (f a) - (e (d a) + f (d a)) = d (e a) - e (d a) + (d (f a) - f (d a))

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (e a) + d (f a) - (e (d a) + f (d a)) = d (e a) - e (d a) + (d (f a) - f (d a))
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
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ ⁅d, d⁆ a = 0 a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ ⁅d, d⁆ a = 0 a
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
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ d (d a) - d (d a) = 0 a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ d (d a) - d (d a) = 0 a
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
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ 0 = 0 a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ 0 = 0 a
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
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d, ⁅e, f⁆⁆ a = (⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆) a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d, ⁅e, f⁆⁆ a = (⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆) a
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
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (e (f a)) - d (f (e a)) - (e (f (d a)) - f (e (d a))) =
    d (e (f a)) - e (d (f a)) - (f (d (e a)) - f (e (d a))) + (e (d (f a)) - e (f (d a)) - (d (f (e a)) - f (d (e a))))

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ d (e (f a)) - d (f (e a)) - (e (f (d a)) - f (e (d a))) =
    d (e (f a)) - e (d (f a)) - (f (d (e a)) - f (e (d a))) + (e (d (f a)) - e (f (d a)) - (d (f (e a)) - f (d (e a))))
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
D1 D2 : Derivation R A A
a✝ : A
r : R
d e : Derivation R A A
a : A
⊢ ⁅d, r • e⁆ a = (r • ⁅d, e⁆) a

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
r : R
d e : Derivation R A A
a : A
⊢ ⁅d, r • e⁆ a = (r • ⁅d, e⁆) a
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
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = x✝² (x✝¹ x✝) - x✝¹ (x✝² x✝) + x✝¹ (x✝² x✝)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = x✝² (x✝¹ x✝) - x✝¹ (x✝² x✝) + x✝¹ (x✝² x✝)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h.succ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
ih : ((toEnd K (↥U) Q) v ^ n) z' = (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)
⊢ ((toEnd K (↥U) Q) v) ((LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)) =
    (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v * (ad K L) ↑v ^ n) z)

Tactic:
;

Goal state after:
case h.succ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
ih : ((toEnd K (↥U) Q) v ^ n) z' = (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)
⊢ ((toEnd K (↥U) Q) v) ((LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)) =
    (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v * (ad K L) ↑v ^ n) z)
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: 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
hx : x ∈ couple R A A'
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2

Tactic:
;

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
hx : x ∈ couple R A A'
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: 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
hx : x ∈ couple R A A'
a : A
⊢ (⇑x.1 ∘ ⇑(Algebra.ofId A A')) a = (⇑(Algebra.ofId A A') ∘ ⇑x.2) a

Tactic:
;

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
hx : x ∈ couple R A A'
a : A
⊢ (⇑x.1 ∘ ⇑(Algebra.ofId A A')) a = (⇑(Algebra.ofId A A') ∘ ⇑x.2) a
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: 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
hx : ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
⊢ x ∈ couple R A A'

Tactic:
;

Goal state after:
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
hx : ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
⊢ x ∈ couple R A A'
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: 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
hx : ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
a : A
⊢ ((compAlgebraMapL R A A' A') x.1) a = ((Algebra.ofId A A').toLinearMap.compDer x.2) a

Tactic:
;

Goal state after:
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
hx : ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
a : A
⊢ ((compAlgebraMapL R A A' A') x.1) a = ((Algebra.ofId A A').toLinearMap.compDer x.2) a
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
  · intro hx; ext a; exact congrArg (· a) hx
  · intro hx; ext a; exact congrArg (· a) hx

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
⊢ f Vᵀ * Y * f V * C.submatrix ⇑s.symm ⇑s.symm =
    Vᵀ.submatrix ⇑s.symm ⇑s.symm * Y * V.submatrix ⇑s.symm ⇑s.symm * C.submatrix ⇑s.symm ⇑s.symm

Tactic:
;

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
⊢ f Vᵀ * Y * f V * C.submatrix ⇑s.symm ⇑s.symm =
    Vᵀ.submatrix ⇑s.symm ⇑s.symm * Y * V.submatrix ⇑s.symm ⇑s.symm * C.submatrix ⇑s.symm ⇑s.symm
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
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✝

Tactic:
;

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
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✝

Tactic:
;

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: case pos
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
i : ι
h : j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) j = ⁅x, (lof R ι M j).toFun m⁆ j

Tactic:
;

Goal state after:
case pos
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
i : ι
h : j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) j = ⁅x, (lof R ι M j).toFun m⁆ j
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✝ : LieDerivation R L L
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ({ toFun := ⇑(LinearMap.lTensor A ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
        { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ })
      a✝

Tactic:
;

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✝ : LieDerivation R L L
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ({ toFun := ⇑(LinearMap.lTensor A ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
        { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ })
      a✝