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

Goal state before:
pp: case neg
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
⊢ (single j ⁅x, m⁆) i = ⁅x, (single j m) i⁆

Tactic:
]

Goal state after:
case neg
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
⊢ (single j ⁅x, m⁆) i = ⁅x, (single j m) i⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Tactic:
]

Goal state after:
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
j : ι
y : L j
k : ι
hij : k ≠ j
x : L k
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ 0 = 0

Tactic:
]

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
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ ((toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) x) y =
    ((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x) ∘ₗ toModule R ι L' fun i ↦ ↑(f i)) y

Tactic:
]

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)
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)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ ((toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) x) y =
    ((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x) ∘ₗ toModule R ι L' fun i ↦ ↑(f i)) y
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr
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
α : K
hsψ : ¬∃ m, m ≠ 0 ∧ ((toEnd K (↥U) Q) (α • u + x')) m = 0
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
⊢ z' = 0

Tactic:
]

Goal state after:
case inr
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
α : K
hsψ : ¬∃ m, m ≠ 0 ∧ ((toEnd K (↥U) Q) (α • u + x')) m = 0
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
⊢ z' = 0
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
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f') (-⁅(of L i) y, x⁆) = -⁅(toModule R ι L' f') ((of L i) y), (toModule R ι L' f') x⁆

Tactic:
]

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)
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)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f') (-⁅(of L i) y, x⁆) = -⁅(toModule R ι L' f') ((of L i) y), (toModule R ι L' f') x⁆
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
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f' ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) x =
    ((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y)) ∘ₗ toModule R ι L' f') x

Tactic:
]

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)
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)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f' ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) x =
    ((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y)) ∘ₗ toModule R ι L' f') x
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)
⊢ F'.det = (fromBlocks (A.map ⇑f) (B.map ⇑f) (C.map ⇑f) (D.map ⇑f)).det

Tactic:
]

Goal state after:
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)
⊢ F'.det = (fromBlocks (A.map ⇑f) (B.map ⇑f) (C.map ⇑f) (D.map ⇑f)).det
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
⊢ f.mapMatrix Cᵀ * f.mapMatrix A = f.mapMatrix Cᵀ * f.mapMatrix A

Tactic:
]

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 : Matrix l l R
hX_symm : X.IsSymm
hXY : X.map ⇑f = Y
⊢ ((IsLocalRing.residue R).mapMatrix A + Y * (IsLocalRing.residue R).mapMatrix C).det ≠ 0

Tactic:
]

Goal state after:
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 : Matrix l l R
hX_symm : X.IsSymm
hXY : X.map ⇑f = Y
⊢ ((IsLocalRing.residue R).mapMatrix A + Y * (IsLocalRing.residue R).mapMatrix C).det ≠ 0
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:
]

Goal state after:
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)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h.refine_2
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
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) (α • u + x')) (((toEnd K (↥U) Q) v ^ k) z') = ((toEnd K (↥U) Q) v) (((toEnd K (↥U) Q) v ^ k) z')

Tactic:
]

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 * M.toBlocks₁₁ + X * M.toBlocks₂₁) (1 * M.toBlocks₁₂ + X * M.toBlocks₂₂)
      (0 * M.toBlocks₁₁ + 1 * M.toBlocks₂₁) (0 * M.toBlocks₁₂ + 1 * M.toBlocks₂₂) =
    fromBlocks (A + X * C) (B + X * D) C D

Tactic:
]

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₁₁
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 * M.toBlocks₁₁ + X * M.toBlocks₂₁) (1 * M.toBlocks₁₂ + X * M.toBlocks₂₂)
      (0 * M.toBlocks₁₁ + 1 * M.toBlocks₂₁) (0 * M.toBlocks₁₂ + 1 * M.toBlocks₂₂) =
    fromBlocks (A + X * C) (B + X * D) C D
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 1 X 0 1 * M ∈ symplecticGroup l R

Tactic:
]

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₁₁
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 1 X 0 1 * M ∈ symplecticGroup l R
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
⊢ Rel R L ≤ ⇑(RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom)

Tactic:
]

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
⊢ Rel R L ≤ ⇑(RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom)
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)
⊢ 1 = 1

Tactic:
]

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
⊢ f x = f x

Tactic:
]

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)
h_main : M.det = 1
⊢ M.det = 1

Tactic:
]

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₁₁
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)
h_main : M.det = 1
⊢ M.det = 1
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 (b + a) (c + a)

Tactic:
]

Goal state after:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (b + a) (c + a)
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 • 1) • a) ((t • 1) • b)

Tactic:
]

Goal state after:
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 • 1) • a) ((t • 1) • b)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h
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
⊢ rank K L ≤ finrank K ↥(engel K y)

Tactic:
]

Goal state after:
case h
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
⊢ rank K L ≤ finrank K ↥(engel K y)
Module: Mathlib.Algebra.Lie.Free

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

Tactic:
]

Goal state after:
R : Type u
X : Type v
inst✝ : CommRing R
⊢ Inhabited (Quot (FreeLieAlgebra.Rel R X))
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) (t • a • c) = Quot.mk (Rel R X) (t • a • c)

Tactic:
]

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

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ = (liftAux R f) (a + b)

Tactic:
]

Goal state after:
case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ = (liftAux R f) (a + b)
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ = (liftAux R f) ((RingHom.id R) t • a)

Tactic:
]

Goal state after:
case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ = (liftAux R f) ((RingHom.id R) t • a)