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

Goal state before:
pp: m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
by
  rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
    fromBlocks_submatrix_sum_swap_sum_swap]
  convert! fromBlocks₁₁ Bᴴ A hD <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
hq : ∀ (k : ι), q ∈ invtSubmodule ↑(P.reflection k)
⊢ p j

Tactic:
simp [← hq_mem, IsIrreducible.eq_top_of_invtSubmodule_reflection q hq hq₀]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (ascPochhammer ℕ n)) = eval (↑k) (ascPochhammer S n)

Tactic:
by
  rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case inl
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h : ↑n - 1 ≤ s
heq : ↑n - 1 = s
⊢ 0 ≤ eval s (descPochhammer S n)

pp: case inr
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h✝ : ↑n - 1 ≤ s
h : ↑n - 1 < s
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
· rw [← heq, descPochhammer_eval_eq_ascPochhammer,
      sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
    positivity

Goal state after:
case inr
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h✝ : ↑n - 1 ≤ s
h : ↑n - 1 < s
⊢ 0 ≤ eval s (descPochhammer S n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h : ↑n - 1 ≤ s
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
rcases eq_or_lt_of_le h with heq | h
  · rw [← heq, descPochhammer_eval_eq_ascPochhammer,
      sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
    positivity
  · exact (descPochhammer_pos h).le

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
n : ℕ
ih : ↑n - 1 ≤ s → (s - ↑n + 1) ^ n ≤ eval s (descPochhammer S n)
h : 0 ≤ s - ↑n
hsub1 : ↑n - 1 ≤ s
⊢ (s - (↑n + 1 - 1)) ^ n * (s - (↑n + 1 - 1)) ≤ eval s (descPochhammer S n) * (s - ↑n)

Tactic:
add_sub_cancel_right

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
n : ℕ
ih : ↑n - 1 ≤ s → (s - ↑n + 1) ^ n ≤ eval s (descPochhammer S n)
h : 0 ≤ s - ↑n
hsub1 : ↑n - 1 ≤ s
⊢ (s - ↑n) ^ n * (s - ↑n) ≤ eval s (descPochhammer S n) * (s - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : ↑n + 1 - 1 ≤ a
b : S
hb : ↑n + 1 - 1 ≤ b
hab : a ≤ b
⊢ (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b

Tactic:
add_sub_cancel_right

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : ↑n ≤ a
b : S
hb : ↑n ≤ b
hab : a ≤ b
⊢ (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
⊢ Function.RightInverse (fun r ↦ ⟨(interpolate s v) fun x ↦ if hx : x ∈ s then r ⟨x, hx⟩ else 0, ⋯⟩) fun f i ↦
    eval (v ↑i) ↑f

Tactic:
by
    intro f
    ext ⟨i, hi⟩
    simp only [eval_interpolate_at_node _ hvs hi]
    exact dif_pos hi

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x✝ : R
⊢ ((map f).comp C) x✝ = (C.comp f) x✝

Tactic:
apply map_C

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h✝ : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
⊢ False

Tactic:
rw [h, mul_zero] at hP

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h✝ : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = 0
h : P = 0
⊢ False
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 n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
⊢ φ * ψ ∈ weightedHomogeneousSubmodule R w (m + n)

Tactic:
c

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
⊢ coeff c (φ * ψ) ≠ 0 → (weight w) c = m + n
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : CommSemiring R
M : Matrix m n R
N : Matrix n o R
i : m
⊢ (M * N).toMvPolynomial i = (bind₁ N.toMvPolynomial) (M.toMvPolynomial i)

Tactic:
by
  simp only [toMvPolynomial, mul_apply, map_sum, Finset.sum_comm (γ := o), bind₁, aeval,
    AlgHom.coe_mk, coe_eval₂Hom, eval₂_monomial, algebraMap_apply, Algebra.algebraMap_self,
    RingHom.id_apply, C_apply, pow_zero, Finsupp.prod_single_index, pow_one, Finset.mul_sum,
    monomial_mul, zero_add]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case mpr
M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ m x = 0 → m x ≠ 0 → m x • w x = 0

Tactic:
· order

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

Goal state before:
pp: case h
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := ⋯
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⋯
hVW : IsCompl V W
x : M
n : ℕ
hx : (φ ^ n) x = 0
⊢ (φ ^ n) (φ x) = 0

Tactic:
← Module.End.mul_apply,

Goal state after:
case h
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : (φ ^ n) x = 0
⊢ (φ ^ n * φ) x = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := ⋯
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⋯
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ y_1, (φ ^ i) y_1 = (φ ^ n) y
⊢ (φ ^ n) (φ y) = φ ((φ ^ n) y)

Tactic:
← Module.End.mul_apply,

Goal state after:
case h
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ y_1, (φ ^ i) y_1 = (φ ^ n) y
⊢ (φ ^ n * φ) y = φ ((φ ^ n) y)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
i : ℕ
⊢ (eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (charpoly (φ x)).coeff i

Tactic:
by
  rw [polyCharpoly, polyCharpolyAux_coeff_eval]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
p : MvPolynomial σ R
⊢ (rename φ) ((homogeneousComponent n) p) = (homogeneousComponent n) ((rename φ) p)

Tactic:
induction p using MvPolynomial.induction_on' with
  | monomial d c =>
    rw [rename_monomial,
      homogeneousComponent_of_mem (isHomogeneous_monomial c rfl),
      homogeneousComponent_of_mem (isHomogeneous_monomial c (Finsupp.degree_mapDomain φ d))]
    split_ifs <;> simp [rename_monomial]
  | add p q hp hq => simp [map_add, hp, hq]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
⊢ c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
h : c ≤ f.rank
⊢ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s

case refine_2
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
⊢ (∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s) → c ≤ f.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
this : ∀ i < finrank K ↥E, χ.coeff i = 0
⊢ χ = X ^ finrank K ↥E

Tactic:
← lieCharpoly_natDegree K E x' u

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
this : ∀ i < (lieCharpoly K (↥E) x' u).natDegree, χ.coeff i = 0
⊢ χ = X ^ (lieCharpoly K (↥E) x' u).natDegree
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ ↥(typeD l R) ≃ₗ⁅R⁆ ↥(so' l l R)

Tactic:
by
  apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans
  apply LieEquiv.ofEq
  ext A
  rw [jd_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
    mem_skewAdjointMatricesLieSubalgebra_unit_smul]
  rfl

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
classical
  obtain ⟨L, L', D, hM0⟩ := Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec M
  set E := fun i ↦ if D i = 0 then 1 else (D i)⁻¹ with E_def
  set s : Finset m := .filter (fun i ↦ D i ≠ 0) .univ with s_def
  set V := diagonal E * (L.reverse.map (toMatrix ∘ .inv)).prod with V_def
  set U := (L'.reverse.map (toMatrix ∘ .inv)).prod with U_def
  have hUdet : IsUnit U.det := (isUnit_iff_isUnit_det _).1 <| isUnit_prod_comp_inverse _
  have hVdet : IsUnit V.det := by
    rw [V_def, det_mul, det_diagonal]
    exact IsUnit.mk0 _ (Finset.prod_ne_zero_iff.2 (by grind)) |>.mul <|
      (isUnit_iff_isUnit_det _).1 (isUnit_prod_comp_inverse _)
  have hM : V * M * U = diagonal (fun i ↦ if i ∈ s then 1 else 0) := by
    rw [V_def, U_def, hM0, mul_assoc, mul_assoc _ (L'.map _).prod, prod_mul_reverse_inv_prod,
      mul_one, ← mul_assoc, mul_assoc _ (L.reverse.map _).prod, reverse_inv_prod_mul_prod, mul_one]
    ext
    simp only [E_def, mul_diagonal, diagonal_apply, ite_mul, one_mul, zero_mul, s_def,
      Finset.mem_filter, Finset.mem_univ, true_and, ite_not]
    split_ifs with h1 h2 <;> first | rw [← h1, h2] | rw [← h1, inv_mul_cancel₀ h2] | rfl
  have hs : s.card = M.rank := by
    simp [← rank_mul_eq_right_of_isUnit_det V M hVdet, ← rank_mul_eq_left_of_isUnit_det U (V * M)
      hUdet, hM, rank_diagonal]
  set e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
    (Equiv.sumCompl (· ∈ s)).symm.trans <| (Finset.equivFinOfCardEq hs).sumCongr <|
      Fintype.equivFinOfCardEq <| by rw [Fintype.card_subtype_compl, Fintype.card_coe, hs] with he
  refine ⟨V, U, e, (isUnit_iff_isUnit_det _).2 hVdet, isUnit_prod_comp_inverse _, ?_⟩
  rw [hM, ← diagonal_one, ← diagonal_zero, fromBlocks_diagonal, submatrix_diagonal_equiv]
  refine congrArg _ (funext fun i ↦ ?_)
  split_ifs with hi <;> simp [he, hi]

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✝ f : L →ₗ⁅R⁆ A
⊢ (fun F ↦ F.toLieHom.comp (ι R)) ((fun f ↦ (ringCon R L).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) f) = f

Tactic:
ext
    -- Porting note: was
    -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
    --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_toLieHom,
    --   LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
    --   RingQuot.liftAlgHom_mkAlgHom_apply]
    simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom,
      UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]
    simp [UniversalEnvelopingAlgebra]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ (single m r).coeff.support
⊢ f x = f m

Tactic:
Finset.mem_singleton.mp (Finsupp.support_single_subset hx)

Goal state after:
M : Type u_1
ι : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ (single m r).coeff.support
⊢ f m = f m
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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x✝¹ x✝ : M
⊢ (ofProd c) (0, ⁅x✝¹, x✝⁆) = ⁅(ofProd c) (0, x✝¹), (ofProd c) (0, x✝)⁆

Tactic:
simp [trivial_lie_zero, bracket_ofTwoCocycle]

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) ⁅LinearMap.restrict ((toEnd R L V) z) hzU, (toEnd R A ↥U) a⁆ = 0

Tactic:
LinearMap.trace_lie

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⁆
⊢ 0 = 0
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
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
this : ⨆ i, U' i ≤ (T χ w).maxGenEigenspace 0
x : ↥U
⊢ ∃ n, (T χ w ^ n) x = 0

Tactic:
specialize this x.2

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
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
x : ↥U
this : ↑x ∈ (T χ w).maxGenEigenspace 0
⊢ ∃ n, (T χ w ^ n) x = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
⊢ (p.toList x).next y hy✝ = p y

Tactic:
obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p ^ k) x = y
⊢ (p.toList x).next y hy✝ = p y
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) s
hl : 2 ≤ s.length
⊢ (fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) ((fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) ⟨Quot.mk (⇑(IsRotated.setoid α)) s, ⋯⟩) =
    ⟨Quot.mk (⇑(IsRotated.setoid α)) s, ⋯⟩

Tactic:
simp only [Cycle.mk_eq_coe, Cycle.nodup_coe_iff, Cycle.mem_coe_iff,
      Cycle.formPerm_coe] at hn hx ⊢

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ ⟨s.formPerm.toCycle ⋯, ⋯⟩ = ⟨↑s, ⋯⟩