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
h : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ Dᵀ * A - Bᵀ * C = 1

Tactic:
simpa using

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
h : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ Dᵀ * A - Bᵀ * C = 1
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
m m₀ : Type um
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).cRank ≤ A.cRank

Tactic:
simpa using

Goal state after:
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
m m₀ : Type um
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).cRank ≤ A.cRank
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n
A : Matrix m n R
⊢ #↑(range A.col) ≤ ↑(Fintype.card n)

Tactic:
simpa using

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n
A : Matrix m n R
⊢ #↑(range (of.symm Aᵀ)) ≤ ↑(Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite n → A.eRank ≤ ENat.card n
hfin : ¬Finite n
⊢ Infinite ?m.33

Tactic:
simpa using

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite n → A.eRank ≤ ENat.card n
hfin : ¬Finite n
⊢ Infinite ?m.33
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite m → A.eRank ≤ ENat.card m
hfin : ¬Finite m
⊢ Infinite ?m.33

Tactic:
simpa using

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite m → A.eRank ≤ ENat.card m
hfin : ¬Finite m
⊢ Infinite ?m.33
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ lift.{um₀, max uR um} A.cRank ≤ lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank

Tactic:
simpa using

Goal state after:
m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ lift.{um₀, max uR um} A.cRank ≤ lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n₀ : Type un₀
R : Type uR
m₀ : Type um
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ (A.submatrix ⇑em ⇑en).cRank = A.cRank

Tactic:
simpa using

Goal state after:
m : Type um
n₀ : Type un₀
R : Type uR
m₀ : Type um
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ (A.submatrix ⇑em ⇑en).cRank = A.cRank
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 : ∃ m, m ≠ 0 ∧ ((toEnd K (↥U) Q) (0 • u + x')) m = 0
⊢ ∃ z, z ≠ 0 ∧ ⁅x', z⁆ = 0

Tactic:
simpa using

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 : ∃ m, m ≠ 0 ∧ ((toEnd K (↥U) Q) (0 • u + x')) m = 0
⊢ ∃ z, ¬z = 0 ∧ ⁅x', z⁆ = 0
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ᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : A *ᵥ (f U • x) ∘ ⇑s = 0
heq2 : C *ᵥ (f U • x) ∘ ⇑s = 0
⊢ (fun g ↦ g ∘ ⇑s) (f U • x) = (fun g ↦ g ∘ ⇑s) (f U • 0)

Tactic:
simpa using

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ᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : A *ᵥ (f U • x) ∘ ⇑s = 0
heq2 : C *ᵥ (f U • x) ∘ ⇑s = 0
⊢ (f U *ᵥ x) ∘ ⇑s = 0
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
a : ↥(twoCochain R L M)
x y : L
⊢ (a y) x + (a x) y = 0

Tactic:
simpa using

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
a : ↥(twoCochain R L M)
x y : L
⊢ (a y) x + (a x) y = 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✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).rank = A.rank

Tactic:
simpa using

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).rank = A.rank
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✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fintype m
A : Matrix m n R
⊢ (A * Aᵀ).rank = A.rank

Tactic:
simpa using

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fintype m
A : Matrix m n R
⊢ (A * Aᵀ).rank = A.rank
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
z' : Q := (LieSubmodule.Quotient.mk' E) z
⊢ z' = 0

Tactic:
have hz' : ∃ n : ℕ, (toEnd K U Q v ^ n) z' = 0 := by
    rw [mem_engel_iff] at hz
    obtain ⟨n, hn⟩ := hz
    use n
    apply_fun LieSubmodule.Quotient.mk' E at hn
    rw [map_zero] at hn
    rw [← hn]
    clear hn
    induction n with
    | zero => simp only [z', pow_zero, Module.End.one_apply]
    | succ n ih => rw [pow_succ', pow_succ', Module.End.mul_apply, ih]; rfl

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

Goal state before:
pp: case inl
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
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
hn₀ : n = 0
⊢ z' = 0

Tactic:
simpa using

Goal state after:
case inl
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
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
hn₀ : n = 0
⊢ 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)
x y z : ⨁ (i : ι), L i
i✝ : ι
⊢ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x (y + z)) i✝ =
    (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x y + zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z) i✝

Tactic:
simp only [zipWith_apply, add_apply, lie_add]

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:
Lx_mul,

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)
⊢ (fromBlocks (A + X * C) (B + X * D) C D).det = 1
Module: Mathlib.Algebra.Lie.UniversalEnveloping

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ((lift R) f) ((mkAlgHom R L) (ιₜ x)) = f x

Tactic:
simpa using

Goal state after:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ((lift R) f) ((mkAlgHom R L) (ιₜ x)) = f x
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:
simpa using

Goal state after:
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)
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:
simpa using

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 (a + -b) (a + -c)
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:
simpa using

Goal state after:
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)
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 rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; change Quot.mk _ _ = Quot.mk _ _; simp_rw [add_mul]

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✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd (i * j))))
      ⟨single (Multiplicative.toAdd (i * j)) 1, ⋯⟩ =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd i))) ⟨single (Multiplicative.toAdd i) 1, ⋯⟩ *
      (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd j))) ⟨single (Multiplicative.toAdd j) 1, ⋯⟩

Tactic:
simpa using

Goal state after:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd i + Multiplicative.toAdd j)))
      ⟨single (Multiplicative.toAdd i + Multiplicative.toAdd j) 1, ⋯⟩ =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd i) + f (Multiplicative.toAdd j)))
      ⟨single (Multiplicative.toAdd i + Multiplicative.toAdd j) 1, ⋯⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
this : Function.Bijective ⇑(lmap fun x ↦ Submodule.toBaseChange S (ℳ x))
⊢ (lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ((of (fun i ↦ S ⊗[R] ↥(ℳ i)) i) x) =
    (lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ((of (fun i ↦ S ⊗[R] ↥(ℳ i)) i) y)

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
this : Function.Bijective ⇑(lmap fun x ↦ Submodule.toBaseChange S (ℳ x))
⊢ (of (fun x ↦ ↥(Submodule.baseChange S (ℳ x))) i) ((Submodule.toBaseChange S (ℳ i)) x) =
    (of (fun x ↦ ↥(Submodule.baseChange S (ℳ x))) i) ((Submodule.toBaseChange S (ℳ i)) y)
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : N = ⊤
x : L
hx : x ∈ radical k L
m : M
⊢ ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m

Tactic:
simpa using

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : N = ⊤
x : L
hx : x ∈ radical k L
m : M
⊢ ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : N = ⊤
x : L
hx : x ∈ radical k L
m : M
hm : ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m
⊢ ((toEnd k L M) x) m = (χ ⟨x, hx⟩ • LinearMap.id) m

Tactic:
simpa using

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : N = ⊤
x : L
hx : x ∈ radical k L
m : M
hm : ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m
⊢ ⁅x, m⁆ = χ ⟨x, hx⟩ • m
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : ∀ (x : L) (hx : x ∈ radical k L), (toEnd k L M) x = χ ⟨x, hx⟩ • LinearMap.id
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id

Tactic:
have aux : radical k L = center k L := by
    refine le_antisymm (fun x hx ↦ (mem_maxTrivSubmodule k L L x).mpr ?_) (center_le_radical k L)
    intro y
    simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), LieHom.map_lie, hχ _ hx, lie_smul,
      (toEnd k L M y).commute_id_right.lie_eq]

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : ∀ (x : L) (hx : x ∈ radical k L), (toEnd k L M) x = χ ⟨x, hx⟩ • LinearMap.id
aux : radical k L = center k L
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id