mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ ∀ (i : Fin (n + 1)), projVandermonde v w i 0 = W i 0

Tactic:
simp [W]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : C (x - y)⁻¹ = 0 ∨ X - C y = 0
⊢ x = y

Tactic:
X_sub_C_ne_zero,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : C (x - y)⁻¹ = 0 ∨ False
⊢ x = y
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ (s.sup fun b ↦ (C (r b) * Lagrange.basis s v b).degree) ≤ ↑(#s - 1)

Tactic:
Finset.sup_le_iff

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ b ∈ s, (C (r b) * Lagrange.basis s v b).degree ≤ ↑(#s - 1)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
h₁ : range b₁.e = range (⇑p₁ ∘ prodE eι b₁ b₂)
h₂ : range b₁.f = range (⇑p₁ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₁ (range b₁.e ∪ range b₁.f) ≤ lieSpan R L₁ (⇑p₁ '' (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))

Tactic:
image_union,

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
h₁ : range b₁.e = range (⇑p₁ ∘ prodE eι b₁ b₂)
h₂ : range b₁.f = range (⇑p₁ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₁ (range b₁.e ∪ range b₁.f) ≤ lieSpan R L₁ (⇑p₁ '' range (prodE eι b₁ b₂) ∪ ⇑p₁ '' range (prodF eι b₁ b₂))
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₂ (range b₂.e ∪ range b₂.f) ≤ lieSpan R L₂ (⇑p₂ '' (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))

Tactic:
image_union,

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₂ (range b₂.e ∪ range b₂.f) ≤ lieSpan R L₂ (⇑p₂ '' range (prodE eι b₁ b₂) ∪ ⇑p₂ '' range (prodF eι b₁ b₂))
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ engel R 0

Tactic:
mem_engel_iff,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, ((ad R L) 0 ^ n) x = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
a : Finset ι
ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)
⊢ Set.InjOn v ↑a

Tactic:
grind [hvs'.mono]

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

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Tactic:
revert hy

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
y : ↥N
⊢ y ∈ (dx ^ (k + 1)).ker → ((ad R L) x ^ (k + 1)) (N.subtype y) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m})
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d = m}
a : R
⊢ motive (C a * AddMonoidAlgebra.single d 1) ⋯

Tactic:
simpa only [single_eq_monomial, ← MvPolynomial.C_mul_monomial] using monomial _ (a * 1) hd

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal =
    (⨆ i, { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }).toIdeal

Tactic:
Ideal.toIdeal_homogeneousHull_eq_iSup,

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I) =
    (⨆ i, { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }).toIdeal
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ Finite.toFinset ⋯ → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
intro hm

Goal state after:
case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ Finite.toFinset ⋯
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ x m = 0 → (weightedHomogeneousComponent w m) ↑(x m) = 0

Tactic:
intro hm

Goal state after:
case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : x m = 0
⊢ (weightedHomogeneousComponent w m) ↑(x m) = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
x✝ : m
⊢ col 1 x✝ = Pi.single x✝ 1

Tactic:
simp [funext_iff, one_apply, Pi.single_apply]

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

Goal state before:
pp: case h.refine_1
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
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ r ≤ (s \ t).card

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
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ ∀ α ∈ s \ t, eval α (constantCoeff ψ) ≠ 0

Tactic:
· refine le_trans ?_ (Finset.le_card_sdiff _ _)
      omega

Goal state after:
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
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ ∀ α ∈ s \ t, eval α (constantCoeff ψ) ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case pos
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
i : m
hi : i ∈ s
⊢ 1 = ((Sum.elim (fun x ↦ 1) fun x ↦ 0) ∘ ⇑e) i

Tactic:
simp [he, hi]

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

Goal state before:
pp: case neg
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
i : m
hi : i ∉ s
⊢ 0 = ((Sum.elim (fun x ↦ 1) fun x ↦ 0) ∘ ⇑e) i

Tactic:
simp [he, hi]

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✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (Aᴴ * A).mulVecLin.ker = A.mulVecLin.ker

Tactic:
by
  ext x
  simp only [LinearMap.mem_ker, mulVecLin_apply, conjTranspose_mul_self_mulVec_eq_zero]

Goal state after:
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 em el) A).range + finrank R ↥((toLin en em) B).range ≤
    finrank R ↥((toLin em el) A).range + finrank R ↥((toLin em el) A).ker

Tactic:
add_le_add_iff_left

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.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝¹ : A
l : L
x✝ : A
l' : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ ⊗ₜ[R] l, x✝ ⊗ₜ[R] l'⁆ =
    ⁅x✝¹ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l')⁆ - ⁅x✝ ⊗ₜ[R] l', (LinearMap.rTensor L ↑d) (x✝¹ ⊗ₜ[R] l)⁆

Tactic:
simp [← lie_skew l' l, -lie_skew, add_tmul, tmul_neg]

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:
← Function.comp_apply (f := lift R f) (g := ι R) (x := x),

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) ∘ ⇑(ι R)) x = f x
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 : FreeLieAlgebra R X →ₗ⁅R⁆ L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
F' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  F.toNonUnitalAlgHom.comp (mk R)
⊢ ((fun f ↦ { toFun := fun c ↦ Quot.liftOn c ⇑(liftAux R f) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ })
        ((fun F ↦ ⇑F ∘ of R) F))
      (Quot.mk (Rel R X) a) =
    F (Quot.mk (Rel R X) a)

Tactic:
exact NonUnitalAlgHom.congr_fun (lib.lift_comp_of R F') a

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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
⊢ (T χ w) (((toEnd R L V) z ^ (n + 1)) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
have H : ∀ w, ⁅w, (π z ^ n) v⁆ = (T χ w) ((π z ^ n) v) + χ w • ((π z ^ n) v) := by simp

Goal state after:
case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
H : ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v
⊢ (T χ w) (((toEnd R L V) z ^ (n + 1)) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}
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
h : ∀ (x : L), (LinearMap.trace k M) ((toEnd k L M) x) = 0
⊢ HasTrivialRadical k L

Tactic:
by
  have : finrank k M ≠ 0 := (finrank_pos_iff.mpr <| nontrivial_of_isIrreducible k L M).ne'
  obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M
  rw [hasTrivialRadical_iff, (hasCentralRadical_iff k L).mp inferInstance, LieSubmodule.eq_bot_iff]
  intro x hx
  specialize h x
  rw [h' x] at hx
  obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx
  suffices t = 0 by simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), ← ht, this]
  simpa [this, ← ht] using h

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
x : ↥E.proj.ker
⊢ (fun m ↦ ⟨E.incl m, ⋯⟩) ((⇑(Equiv.ofInjective ⇑E.incl ⋯).symm ∘ ⇑(IsExtension.kerEquivRange E.incl E.proj)) x) = x

Tactic:
simpa [Subtype.ext_iff] using! Equiv.apply_ofInjective_symm E.incl_injective _

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
hres : (toEnd R A ↥U) ⁅z, a⁆ = ⁅LinearMap.restrict ((toEnd R L V) z) hzU, (toEnd R A ↥U) a⁆
⊢ (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0

Tactic:
hres,

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
hres : (toEnd R A ↥U) ⁅z, a⁆ = ⁅LinearMap.restrict ((toEnd R L V) z) hzU, (toEnd R A ↥U) a⁆
⊢ (LinearMap.trace R ↥U) ⁅LinearMap.restrict ((toEnd R L V) z) hzU, (toEnd R A ↥U) a⁆ = 0