mathlib-initiative/mathlib-tactics huggingface dataset:
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
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
⊢ A'ᵀ * C' = C'ᵀ * A'

Tactic:
by

Goal state after:
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
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
Y : Matrix l l k
hY_symm : Y.IsSymm
hY_det : IsUnit (A' + Y * C')
⊢ ∃ X, X.IsSymm ∧ X.map ⇑f = Y

Tactic:
by

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)
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
⊢ (toModule R ι L' fun i ↦ ↑(f i)) ⁅x, y⁆ = ⁅(toModule R ι L' fun i ↦ ↑(f i)) x, (toModule R ι L' fun i ↦ ↑(f i)) y⁆

Tactic:
by

Goal state after:
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
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C).det

Tactic:
by

Goal state after:
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
x y : L
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
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
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
⊢ fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D

Tactic:
by

Goal state after:
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
x y : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
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
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
Lx_mul : fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D
⊢ fromBlocks (A + X * C) (B + X * D) C D ∈ symplecticGroup l R

Tactic:
by

Goal state after:
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
⊢ ringCon R L ≤ RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom

Tactic:
by

Goal state after:
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
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
Lx_mul : fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D
h_fromBlocks_in : fromBlocks (A + X * C) (B + X * D) C D ∈ symplecticGroup l R
x✝ : Invertible (A + X * C)
⊢ (fromBlocks 1 X 0 1 * M).det = 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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) = F

Tactic:
by

Goal state after:
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
x : L
⊢ ((lift R) f) ((ι R) x) = f x

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
x : L
⊢ ((lift R) f) ((mkAlgHom R L) (ιₜ x)) = f x

Tactic:
by

Goal state after:
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
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
⊢ M.det = 1

Tactic:
by

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

Goal state before:
pp: 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
E : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x}
hUle : U ≤ ↑E
hmin : IsMin E
⊢ IsBot E

Tactic:
by

Goal state after:
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
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ⇑g ∘ ⇑(ι R) = ⇑f ↔ g = (lift R) f

Tactic:
by

Goal state after:
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
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)
⊢ (lift R).symm g₁ = (lift R).symm g₂

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
this : finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)
⊢ Ex ≤ ⟨engel K y, ⋯⟩

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a + b) (a + c)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b : lib R X
h : Rel R X a b
⊢ Rel R X (-a) (-b)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a - b) (a - c)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X a b
⊢ Rel R X (a - c) (b - c)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X (t • a) (t • b)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ Inhabited (FreeLieAlgebra R X)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x y z : FreeLieAlgebra R X),
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (x + y) z =
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x z + Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ y z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : Module.Finite K L
inst✝ : Infinite K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x y z : FreeLieAlgebra R X),
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x (y + z) =
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x y + Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x z

Tactic:
by

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

Goal state before:
pp: case mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) a) = 0

Tactic:
exact Quot.sound (Rel.lie_self a)

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x : FreeLieAlgebra R X), Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x y z : FreeLieAlgebra R X),
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ y z) =
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x y) z +
        Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ y (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x z)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (t : R) (x y : FreeLieAlgebra R X), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
h : Rel R X a b
⊢ (liftAux R f) a = (liftAux R f) b

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ ∀ (x y : FreeLieAlgebra R X),
    Quot.liftOn (x + y) ⇑(liftAux R f) ⋯ = Quot.liftOn x ⇑(liftAux R f) ⋯ + Quot.liftOn y ⇑(liftAux R f) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ ∀ (m : R) (x : FreeLieAlgebra R X),
    Quot.liftOn (m • x) ⇑(liftAux R f) ⋯ = (RingHom.id R) m • Quot.liftOn x ⇑(liftAux R f) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ ∀ {x y : FreeLieAlgebra R X},
    Quot.liftOn ⁅x, y⁆ ⇑(liftAux R f) ⋯ = ⁅Quot.liftOn x ⇑(liftAux R f) ⋯, Quot.liftOn y ⇑(liftAux R f) ⋯⁆

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ (fun F ↦ ⇑F ∘ of R)
      ((fun f ↦ { toFun := fun c ↦ Quot.liftOn c ⇑(liftAux R f) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }) f) =
    f

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (fun f ↦ { toFun := fun c ↦ Quot.liftOn c ⇑(liftAux R f) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ })
      ((fun F ↦ ⇑F ∘ of R) F) =
    F

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x : X
⊢ ((lift R) f) (of R x) = f x

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) (⇑F ∘ of R) = F

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)
⊢ (lift R).symm F₁ = (lift R).symm F₂

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))).comp
      ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)) =
    AlgHom.id R (FreeAlgebra R X)

Tactic:
by

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)).comp
      ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))) =
    AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm (x✝² + x✝¹), (decomposeLinearEquiv ℒ).symm x✝⁆ =
    (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝⁆ +
      (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝¹, (decomposeLinearEquiv ℒ).symm x✝⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm (x✝¹ + x✝)⁆ =
    (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝¹⁆ +
      (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝, (decomposeLinearEquiv ℒ).symm x✝⁆ = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ)
      ⁅(decomposeLinearEquiv ℒ).symm x✝²,
        (decomposeLinearEquiv ℒ).symm
          ((decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝¹, (decomposeLinearEquiv ℒ).symm x✝⁆)⁆ =
    (decomposeLinearEquiv ℒ)
        ⁅(decomposeLinearEquiv ℒ).symm
            ((decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝¹⁆),
          (decomposeLinearEquiv ℒ).symm x✝⁆ +
      (decomposeLinearEquiv ℒ)
        ⁅(decomposeLinearEquiv ℒ).symm x✝¹,
          (decomposeLinearEquiv ℒ).symm
            ((decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝⁆)⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x y : L
⊢ (decompose ℒ) ⁅x, y⁆ = ⁅(decompose ℒ) x, (decompose ℒ) y⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (decompose ℒ).symm ⁅x, y⁆ = ⁅(decompose ℒ).symm x, (decompose ℒ).symm y⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ : R
x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ 0 • x✝ = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² : R
x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ ⁅x✝¹, x✝² • x✝⁆ = x✝² • ⁅x✝¹, x✝⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
⊢ ∀ {x y : L},
    (↑(decomposeLinearEquiv ℒ)).toFun ⁅x, y⁆ =
      ⁅(↑(decomposeLinearEquiv ℒ)).toFun x, (↑(decomposeLinearEquiv ℒ)).toFun y⁆

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
i : ι
⊢ φ i ∈ Set.center R

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : (decompose ℒ).symm b ∈ ℒ k
⊢ b ∈ (lof R ι (fun x ↦ ↥(ℒ x)) k).range

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : (decompose ℒ).symm b ∈ ℒ k
⊢ (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
a b : R[M]
ha : a ∈ {a | ∀ m ∈ a.coeff.support, f m = i}
hb : b ∈ {a | ∀ m ∈ a.coeff.support, f m = i}
m : M
h : m ∈ (a + b).coeff.support
⊢ f m = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
m : M
h : m ∈ (coeff 0).support
⊢ f m = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
a : R[M]
⊢ a ∈ gradeBy R f i ↔ ↑a.coeff.support ⊆ f ⁻¹' {i}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a.coeff.support ⊆ {m}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a ∈ (lsingle m).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
⊢ single m r ∈ gradeBy R f (f m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (coeff 1).support
⊢ f m = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : a ∈ gradeBy R (⇑f) i
hb : b ∈ gradeBy R (⇑f) j
c : M
hc : c ∈ (a * b).coeff.support
⊢ f c = i + j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
⊢ SetLike.GradedMonoid (grade R)

Tactic:
by

Goal state after: