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

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

Tactic:
or_false,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : C (x - y)⁻¹ = 0
⊢ x = y
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
⊢ (-1) ^ ↑0 * W 0 0 * (W.submatrix succ (succAbove 0)).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

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
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.succAbove).det = 0

Tactic:
· rw [succAbove_zero, hW_eq, det_mul_column, ih]
    simp only [Nat.succ_eq_add_one, coe_ofNat_eq_mod, Nat.zero_mod,
      pow_zero, show W 0 0 = w 0 ^ n by simp [W, projVandermonde_apply], one_mul, hr]
    field_simp
    simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_fin, Function.comp_apply]
    field_simp
    simp only [prod_univ_succ, Ioi_zero_eq_map, Finset.prod_map, coe_succEmb, prod_Ioi_succ]

Goal state after:
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
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.succAbove).det = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) ((interpolate s v) r) = r i

Tactic:
rw [interpolate_apply, eval_finsetSum, ← add_sum_erase _ _ hi]
  simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, mul_one, add_eq_left]
  refine sum_eq_zero fun j H => ?_
  rw [eval_basis_of_ne (mem_erase.mp H).1 hi, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k

Tactic:
rw [vandermonde_apply, vandermonde_apply, h₁]

Goal state after:
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
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₂
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Tactic:
obtain ⟨k, hk⟩ : ∃ a, ∀ b ≥ a, Codisjoint (LinearMap.ker (dx ^ b)) (LinearMap.range (dx ^ b)) :=
    eventually_atTop.mp <| dx.eventually_codisjoint_ker_pow_range_pow

Goal state after:
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 : ℕ
hk : ∀ b ≥ k, Codisjoint (dx ^ b).ker (dx ^ b).range
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ (map g) ((bind₂ f) φ) = (bind₂ ((map g).comp f)) φ

Tactic:
by
  simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]
  congr 1 with : 1
  simp only [Function.comp_apply, map_X]

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

Goal state before:
pp: case h.inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H := { toFun := fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → K n = K m
y : ↥H
m : ℕ
hm : ((ad R L) ↑x ^ m) ↑y = 0
hmn : n ≤ m
this : ∀ (k : ℕ), ((ad R L) ↑x ^ k) ↑y = 0 ↔ y ∈ K k
⊢ ((ad R L) ↑x ^ n) ↑y = ↑(0 y)

Tactic:
rwa [this, ← hn m hmn, ← this] at hm

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ derivative (nodal (insert i t) v) = ∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v

Tactic:
rw [nodal_insert_eq_nodal hit, derivative_mul, IH, derivative_sub, derivative_X, derivative_C,
      sub_zero, one_mul, sum_insert hit, mul_sum, erase_insert hit, add_right_inj]
    refine sum_congr rfl fun j hjt => ?_
    rw [t.erase_insert_of_ne (ne_of_mem_of_not_mem hjt hit).symm,
      nodal_insert_eq_nodal (mem_of_mem_erase.mt hit)]

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

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
q : K[X]
hq : (aeval ((ad K (End K M)) (φ x))) q = (ad K (End K M)) y
⊢ ((aeval ((ad K (End K M)) (φ x))) q) z ∈ φ.range

Tactic:
apply q.aeval_apply_smul_mem_of_le_comap hz _ ?_

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
q : K[X]
hq : (aeval ((ad K (End K M)) (φ x))) q = (ad K (End K M)) y
⊢ φ.range.toSubmodule ≤ Submodule.comap ((ad K (End K M)) (φ x)) φ.range.toSubmodule
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
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w) d ≠ n
⊢ coeff d φ = 0

Tactic:
by
  have aux := mt (@hφ d) hd
  rwa [Classical.not_not] at aux

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ = X ^ finrank R M

Tactic:
by
  rw [← sub_eq_zero]
  apply IsNilpotent.eq_zero
  rw [finrank_eq_card_chooseBasisIndex]
  apply Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
  exact h.map (LinearMap.toMatrixAlgEquiv (chooseBasis R M))

Goal state after:
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
⊢ m ∉ DFinsupp.support x → (weightedHomogeneousComponent w m) ↑(x m) = 0

Tactic:
rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_zero]

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

Goal state before:
pp: m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ (toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })

Tactic:
by
  have hIJ : IsCompl { i : m | w i ≠ 0 } { i : m | w i = 0 } := isCompl_compl.symm
  have B₁ := iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) hIJ (Set.toFinite _)
  rw [LinearMap.rank, range_diagonal, B₁, ← @rank_fun' K]
  exact iInfKerProjEquiv K (fun _ ↦ K) hIJ.disjoint hIJ.codisjoint.top_le |>.rank_eq

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a ∈ {A | A * J l R * Aᵀ = J l R}
hb : b ∈ {A | A * J l R * Aᵀ = J l R}
⊢ a * b ∈ {A | A * J l R * Aᵀ = J l R}

Tactic:
simp only [Set.mem_ofPred_eq, transpose_mul] at *

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * b * J l R * (bᵀ * aᵀ) = J l R
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
hi : 0 < r
α : K
⊢ (LinearMap.charpoly ((toEnd K ↥U ↥E) (α • u + x'))).coeff 0 = 0

Tactic:
← constantCoeff_apply,

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
hi : 0 < r
α : K
⊢ constantCoeff (LinearMap.charpoly ((toEnd K ↥U ↥E) (α • u + x'))) = 0
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 : (LinearMap.charpoly ((toEnd K (↥U) Q) (0 • u + x'))).coeff 0 = (evalRingHom 0) 0
⊢ ∃ z, z ≠ 0 ∧ ⁅x', z⁆ = 0

Tactic:
← constantCoeff_apply,

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 (LinearMap.charpoly ((toEnd K (↥U) Q) (0 • u + x'))) = (evalRingHom 0) 0
⊢ ∃ z, z ≠ 0 ∧ ⁅x', 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
M : Matrix m n R
h : LinearIndependent R M.row
⊢ M.rank = Fintype.card m

Tactic:
M.rank_eq_finrank_span_row,

Goal state after:
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)) = Fintype.card m
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ψ : (LinearMap.charpoly ((toEnd K (↥U) Q) (α • u + x'))).coeff 0 ≠ 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:
← constantCoeff_apply,

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ψ : constantCoeff (LinearMap.charpoly ((toEnd K (↥U) Q) (α • u + x'))) ≠ 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.Free

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

Tactic:
rintro t ⟨a⟩ ⟨c⟩

Goal state after:
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) a, t • Quot.mk (Rel R X) c⁆ = t • ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) c⁆
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case of
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (congrLinearEquiv (decomposeTensorEquiv ℳ N))
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N)
        (↑(LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)) =
    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩

Tactic:
LinearEquiv.coe_rTensor,

Goal state after:
case of
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (congrLinearEquiv (decomposeTensorEquiv ℳ N))
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N)
        ((rTensor N ↑(decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)) =
    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
⊢ Function.Injective ⇑(inl ψ)

Tactic:
intro; simp [inl]

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
r : R
x y : ofTwoCocycle c
⊢ (⁅((ofProd c).symm x).1, ((ofProd c).symm (r • y)).1⁆,
      (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (r • y)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (r • y)).2⁆ -
        ⁅((ofProd c).symm (r • y)).1, ((ofProd c).symm x).2⁆) =
    r •
      (ofProd c).symm.toFun
        ((ofProd c)
          (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
            (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
              ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆))

Tactic:
by simp [← smul_add, smul_sub]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x (x :: y :: l)[k]

Tactic:
use k

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ ((x :: y :: l).formPerm ^ ↑k) x = (x :: y :: l)[k]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hx : (p.cycleOf x ^ m.succ) x ≠ x
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ (m + 1)) x → 0 = m + 1

Tactic:
cycleOf_pow_apply_self

Goal state after:
case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hx : (p ^ m.succ) x ≠ x
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ (m + 1)) x → 0 = m + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
n : ℕ
hx : (p.cycleOf x ^ n.succ) x ≠ x
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm✝ : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ 0) x → n + 1 = 0

Tactic:
cycleOf_pow_apply_self

Goal state after:
case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
n : ℕ
hx : (p ^ n.succ) x ≠ x
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm✝ : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ 0) x → n + 1 = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s ↦ (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ∀ (y : { s // s.Nodup ∧ s.Nontrivial }), (fun s ↦ (↑s).formPerm ⋯ = f) y → y = ⟨s, ⋯⟩

Tactic:
· rintro ⟨t, ht, ht'⟩ ht''
    simpa using hs' ⟨t, ht⟩ ht''

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
A : Array R
hn : n = k + 1
⊢ birdDet n A = (-1) ^ k * (stepEntry n A)^[k] (BirdDet.get n A) 0 0

Tactic:
subst hn

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Array R
⊢ birdDet (k + 1) A = (-1) ^ k * (stepEntry (k + 1) A)^[k] (BirdDet.get (k + 1) A) 0 0