mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : ∀ (i : I), f ⟨μ i, ⋯⟩ = 0
i : I
⊢ f ⟨↑⟨μ i, ⋯⟩, ⋯⟩ = 0

Tactic:
exact this i

Goal state after:
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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
disj : Disjoint p₁.ker p₂.ker
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
this : I₁ ≠ ⊤
⊢ Injective ⇑p₁

Tactic:
replace this := (IsSimple.eq_bot_or_eq_top I₁).resolve_right this
      rw [LieIdeal.map_eq_bot_iff] at this
      rw [← p₁.ker_eq_bot, disj.eq_bot_of_le this]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ P.degree < ↑(#s)

Tactic:
hdegree

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ ↑(#s - 1) < ↑(#s)
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
⊢ φ.range.toSubmodule ≤ Submodule.comap ((ad K (End K M)) (φ x)) φ.range.toSubmodule

Tactic:
rintro - ⟨w, rfl⟩

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
w : L
⊢ ↑φ w ∈ Submodule.comap ((ad K (End K M)) (φ x)) φ.range.toSubmodule
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ ℤ n).coeff (Fintype.card n) = 1

Tactic:
rw [← univ_natDegree ℤ n]

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ ℤ n).coeff (univ ℤ n).natDegree = 1
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
⊢ Submodule.IsHomogeneous (span {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}) 𝒜

Tactic:
refine Ideal.homogeneous_span _ _ fun x hx => ?_

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
x : A
hx : x ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}
⊢ IsHomogeneousElem 𝒜 x
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R 1 ^ (n + 1) ≤ homogeneousSubmodule σ R (n + 1)

Tactic:
pow_add,

Goal state after:
case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R 1 ^ n * homogeneousSubmodule σ R 1 ^ 1 ≤ homogeneousSubmodule σ R (n + 1)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x.IsHomogeneous n
⊢ x ∈ homogeneousSubmodule σ R 1 ^ n

Tactic:
induction hx using IsWeightedHomogeneous.induction_on with
    | zero => simp
    | add p q _ _ hp hq => exact Submodule.add_mem _ hp hq
    | monomial d r hr =>
      convert! monomial_mem_homogeneousSubmodule_pow_degree _ _
      rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d ((weightedHomogeneousComponent w 0) φ) = coeff d (C (coeff 0 φ))

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]

Goal state after:
case inr.hnc
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬(weight w) d = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = 0

Tactic:
obtain rfl | hd := eq_or_ne d 0

Goal state after:
case h.inl
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
⊢ coeff 0 (((finSuccEquiv R N) F).coeff n) = 0

case h.inr
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : d ≠ 0
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) (decompose' R w φ) = φ

Tactic:
conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) (decompose' R w φ) =
    ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : Invertible P
⊢ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)

Tactic:
by
    ext A
    suffices P.lieConj h A ∈ skewAdjointMatricesSubmodule J ↔
        A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P) by
      simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
      exact this
    simp [Matrix.IsSkewAdjoint, J.isAdjointPair_equiv _ _ P (isUnit_of_invertible P)]

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

Goal state before:
pp: R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : Fintype n
J : Matrix n n R
inst✝² : DecidableEq n
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (e A)ᵀ = e Aᵀ
A : Matrix m m R
⊢ J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A

Tactic:
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, ← h,
      ← Function.Injective.eq_iff e.injective, map_mul, AlgEquiv.apply_symm_apply, map_neg]

Goal state after:
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
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • S l R) ↔ A ∈ ↑(so' l l R)

Tactic:
mem_skewAdjointMatricesLieSubalgebra_unit_smul

Goal state after:
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
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (S l R) ↔ A ∈ ↑(so' l l R)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)
⊢ lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank

Tactic:
cRank,

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)
⊢ lift.{um, max uR um₀} (Module.rank R ↥(span R (range (A.submatrix r id).col))) ≤ lift.{um₀, max uR um} A.cRank
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
h : LinearIndependent R (col 1)
⊢ cRank 1 = lift.{uR, um} #m

Tactic:
cRank,

Goal state after:
m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
h : LinearIndependent R (col 1)
⊢ Module.rank R ↥(span R (range (col 1))) = lift.{uR, um} #m
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case inl
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : IsEmpty n
⊢ cRank 0 = 0

Tactic:
cRank,

Goal state after:
case inl
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : IsEmpty n
⊢ Module.rank R ↥(span R (range (col 0))) = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case inr
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : Nonempty n
⊢ cRank 0 = 0

Tactic:
cRank,

Goal state after:
case inr
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : Nonempty n
⊢ Module.rank R ↥(span R (range (col 0))) = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : (Matrix n n R)ˣ
this : (↑A * ↑A⁻¹).rank ≤ (↑A).rank
⊢ Fintype.card n ≤ (↑A).rank

Tactic:
← Units.val_mul,

Goal state after:
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : (Matrix n n R)ˣ
this : (↑(A * A⁻¹)).rank ≤ (↑A).rank
⊢ Fintype.card n ≤ (↑A).rank
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
A : Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • fromBlocks 1 0 0 (S l R))

Tactic:
mem_skewAdjointMatricesLieSubalgebra_unit_smul

Goal state after:
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
A : Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (fromBlocks 1 0 0 (S l R))
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
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 ⋯))
⊢ (diagonal fun i ↦ if i ∈ s then 1 else 0) = (fromBlocks (diagonal fun x ↦ 1) 0 0 0).submatrix ⇑e ⇑e

Tactic:
← diagonal_zero,

Goal state after:
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 ⋯))
⊢ (diagonal fun i ↦ if i ∈ s then 1 else 0) = (fromBlocks (diagonal fun x ↦ 1) 0 0 (diagonal fun x ↦ 0)).submatrix ⇑e ⇑e
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
hrw : insert 0 (range (diagonal w).col) = insert 0 (range w')
⊢ (diagonal w).cRank = lift.{uR, um} #{ i // w i ≠ 0 }

Tactic:
cRank,

Goal state after:
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
hrw : insert 0 (range (diagonal w).col) = insert 0 (range w')
⊢ Module.rank R ↥(span R (range (diagonal w).col)) = lift.{uR, um} #{ i // w i ≠ 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
h : ↑(finrank K L) ≤ #K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
obtain ⟨x, hx⟩ := exists_isRegular_of_finrank_le_card K L h
  use x
  refine ⟨?_, normalizer_engel _ _⟩
  apply isNilpotent_of_forall_le_engel
  intro y hy
  set Ex : {engel K z | z ∈ engel K x} := ⟨engel K x, x, self_mem_engel _ _, rfl⟩
  suffices IsBot Ex from @this ⟨engel K y, y, hy, rfl⟩
  apply engel_isBot_of_isMin h (engel K x) Ex le_rfl
  rintro ⟨_, y, hy, rfl⟩ hyx
  suffices finrank K (engel K x) ≤ finrank K (engel K y) by
    suffices engel K y = engel K x from this.ge
    apply LieSubalgebra.toSubmodule_injective
    exact Submodule.eq_of_le_of_finrank_le hyx this
  rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]
  apply rank_le_finrank_engel

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✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : a ∈ gradeBy R (⇑f) i
hb : b ∈ gradeBy R (⇑f) j
ma : M
hma : ma ∈ a.coeff.support
mb : M
hmb : mb ∈ b.coeff.support
hc : ma + mb ∈ (a * b).coeff.support
⊢ i + f mb = i + j

Tactic:
hb mb hmb

Goal state after:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : a ∈ gradeBy R (⇑f) i
hb : b ∈ gradeBy R (⇑f) j
ma : M
hma : ma ∈ a.coeff.support
mb : M
hmb : mb ∈ b.coeff.support
hc : ma + mb ∈ (a * b).coeff.support
⊢ i + j = i + j
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ l.formPerm.Disjoint l'.formPerm ↔ l.Disjoint l'

Tactic:
disjoint_iff_eq_or_eq,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ (∀ (x : α), l.formPerm x = x ∨ l'.formPerm x = x) ↔ l.Disjoint l'
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑[l.attach.dedup.length] = {l.length}

pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ (x : { x // x ∈ l }), l.attach ≠ [x]

Tactic:
dedup_eq_self.mpr hl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑[l.attach.length] = {l.length}

α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ (x : { x // x ∈ l }), l.attach ≠ [x]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k) x)).length
hn' : n < ((p.toList x).rotate k).length
⊢ (p ^ n) ((p ^ k) x) = (p ^ (n + k)) x

Tactic:
pow_add,

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k) x)).length
hn' : n < ((p.toList x).rotate k).length
⊢ (p ^ n) ((p ^ k) x) = (p ^ n * p ^ k) x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Tactic:
have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl
  have hs : l.formPerm.support = l.toFinset := by
    refine support_formPerm_of_nodup _ hn ?_
    rintro _ rfl
    simp at hl
  rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
  · refine ext_getElem (by simp) fun k hk hk' => ?_
    simp only [get_eq_getElem, getElem_iterate, iterate_eq_pow, formPerm_pow_apply_getElem _ hn,
      zero_add, Nat.mod_eq_of_lt hk']
  · simp [hs]

Goal state after: