mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
hz : z ∈ engel K ↑v
⊢ (LieSubmodule.Quotient.mk' E) z = 0

Tactic:
]

Goal state after:
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
hz : z ∈ engel K ↑v
⊢ (LieSubmodule.Quotient.mk' E) z = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker =
    finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker

Tactic:
]

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
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
hz : ∃ n, ((ad K L) ↑v ^ n) z = 0
z' : Q := (LieSubmodule.Quotient.mk' E) z
⊢ ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0

Tactic:
]

Goal state after:
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
hz : ∃ n, ((ad K L) ↑v ^ n) z = 0
z' : Q := (LieSubmodule.Quotient.mk' E) z
⊢ ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ finrank R ↥A.mulVecLin.range = finrank R ↥A.mulVecLin.range

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case intro
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ finrank R ↥(span R (range A.row)) = finrank R ↥(span R (range A.row))

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
⊢ finrank R ↥(span R (range M.row)) = finrank R ↥(span R (range M.row))

Tactic:
]

Goal state after:
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
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 : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0

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
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 : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0
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
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 : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)

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
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 : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ finrank R ↥((toLin en em) B).range ≤ finrank R ↥((toLin em el) A).ker

Tactic:
]

Goal state after:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ finrank R ↥((toLin en em) B).range ≤ finrank R ↥((toLin em el) A).ker
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (replicateCol (Fin 1) w) ∘ₗ toLin' (replicateRow (Fin 1) v)).rank ≤ 1

Tactic:
]

Goal state after:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (replicateCol (Fin 1) w) ∘ₗ toLin' (replicateRow (Fin 1) v)).rank ≤ 1
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ 1 = 1

Tactic:
]

Goal state after:
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.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 : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, y⁆, a x⁆ + ⁅y, ⁅z, a x⁆⁆) - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆) - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - (⁅⁅z, y⁆, a x⁆ + ⁅y, ⁅z, a x⁆⁆) - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0

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
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, y⁆, a x⁆ + ⁅y, ⁅z, a x⁆⁆) - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆) - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - (⁅⁅z, y⁆, a x⁆ + ⁅y, ⁅z, a x⁆⁆) - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0
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.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 : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ a (-⁅x, ⁅y, z⁆⁆) + a ⁅z, ⁅y, x⁆⁆ = a (-⁅x, ⁅y, z⁆⁆) + a ⁅z, ⁅y, x⁆⁆

Tactic:
]

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

Goal state before:
pp: 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)
h : (d₂₃ R L M) a = 0
x y z : L
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

Tactic:
]

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)
h : (d₂₃ R L M) a = 0
x y z : L
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

Tactic:
]

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)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ -(-(a ⁅x, y⁆) z + (a ⁅x, z⁆) y) = (a ⁅x, y⁆) z + -(a ⁅x, z⁆) y

Tactic:
]

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)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ -(-(a ⁅x, y⁆) z + (a ⁅x, z⁆) y) = (a ⁅x, y⁆) z + -(a ⁅x, z⁆) y
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
x y z : L
⊢ -(a ⁅x, y⁆) z + -(a y) ⁅x, z⁆ - -((a ⁅x, y⁆) z + (a y) ⁅x, z⁆) = 0

Tactic:
]

Goal state after:
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)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
x y z : L
⊢ -(a ⁅x, y⁆) z + -(a y) ⁅x, z⁆ - -((a ⁅x, y⁆) z + (a y) ⁅x, z⁆) = 0
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.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_2
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
heq' : f (A + X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f Q + Y * f P) * f U⁻¹
⊢ (IsUnit (f Vᵀ) ∧ IsUnit (f Q + Y * f P)) ∧ IsUnit (f U⁻¹)

Tactic:
]

Goal state after:
case refine_2
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
heq' : f (A + X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f Q + Y * f P) * f U⁻¹
⊢ (IsUnit (f Vᵀ) ∧ IsUnit (f Q + Y * f P)) ∧ IsUnit (f U⁻¹)