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

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ 0 ^ (k + l) = 0 ^ k * 0 ^ l

Tactic:
pow_add

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (k + l) = A ^ k * A ^ l

Tactic:
pow_add

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ k * A ^ l = A ^ k * A ^ l
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑u⁻¹ ^ (k + 1) = (↑u)⁻¹ ^ (k + 1)

Tactic:
coe_units_inv

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ (↑u)⁻¹ ^ (k + 1) = (↑u)⁻¹ ^ (k + 1)
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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : (algebraMap S R) (cartanMatrixIn S b).det ≠ 0
aux : (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
ne_eq,

Goal state after:
ι : 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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : ¬(algebraMap S R) (cartanMatrixIn S b).det = 0
aux : (Matrix.diagonal fun i ↦ (B.form (P.root ↑i)) (P.root ↑i)).Nondegenerate
⊢ (cartanMatrixIn S b).Nondegenerate
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 ι
i j : ↥b.support
h : i ≠ j
⊢ ↑i ≠ ↑j

Tactic:
ne_eq,

Goal state after:
ι : 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 ι
i j : ↥b.support
h : i ≠ j
⊢ ¬↑i = ↑j
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✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ (4 - b.cartanMatrix).det ≠ 0

Tactic:
ne_eq,

Goal state after:
ι : 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✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬(4 - b.cartanMatrix).det = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (n : ℕ) (a : R),
    ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x →
      ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x

Tactic:
intro n a hna

Goal state after:
case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x
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
k : ↥b.support
x : M
l : ↥b.support
hl : p l
hx : P.root ↑l ∈ ⇑P.root ∘ Subtype.val '' {i | p i}
hk : (P.coroot' ↑k) (P.root ↑l) ≠ 0
⊢ b.cartanMatrix k l ≠ 0

Tactic:
ne_eq,

Goal state after:
ι : 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
k : ↥b.support
x : M
l : ↥b.support
hl : p l
hx : P.root ↑l ∈ ⇑P.root ∘ Subtype.val '' {i | p i}
hk : (P.coroot' ↑k) (P.root ↑l) ≠ 0
⊢ ¬b.cartanMatrix k l = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
f : End R M
inst✝² : IsDomain R
inst✝¹ : Module.Finite R M
inst✝ : IsTorsionFree R M
h : minpoly R f ≠ 0
⊢ {μ | f.HasEigenvalue μ} ⊆ (minpoly R f).rootSet R

Tactic:
simp [Set.subset_def, hasEigenvalue_iff_isRoot, mem_rootSet, h]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * 2 ^ (2 * n) * (2 * n)! =
    ((∏ i ∈ range (2 * n), (2 * i + 1)!) * 2 ^ n) ^ 2 * (2 * n)!

Tactic:
pow_mul',

Goal state after:
n : ℕ
⊢ (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * (2 ^ n) ^ 2 * (2 * n)! =
    ((∏ i ∈ range (2 * n), (2 * i + 1)!) * 2 ^ n) ^ 2 * (2 * n)!
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
i j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ ((f (Sum.inl i)) fun i ↦ ↑(P.pairingIn ℤ i j)) ≠ 0

Tactic:
ne_eq,

Goal state after:
case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
i j : ι
hj : j ∈ b.support
hj₀ : ¬P.pairingIn ℤ j i = 0
⊢ ((f (Sum.inl i)) fun i ↦ ↑(P.pairingIn ℤ i j)) ≠ 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ (n + 1) = (ascPochhammer ℤ (n + 1)).comp (X - (↑n + 1 - 1))

Tactic:
add_sub_cancel_right,

Goal state after:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ (n + 1) = (ascPochhammer ℤ (n + 1)).comp (X - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑n + 1 - 1)) (ascPochhammer R (n + 1))

Tactic:
add_sub_cancel_right,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - ↑n) (ascPochhammer R (n + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
n m : ℕ
⊢ descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)

Tactic:
by
  induction m with
  | zero => simp
  | succ m ih =>
    rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ eval (↑n) (descPochhammer R k) * ↑n - ↑k * eval (↑n) (descPochhammer R k) = ↑((n - k) * n.descFactorial k)

Tactic:
← Nat.cast_comm n,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ ↑n * eval (↑n) (descPochhammer R k) - ↑k * eval (↑n) (descPochhammer R k) = ↑((n - k) * n.descFactorial k)
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 : ↑n + 1 - 1 ≤ s
⊢ (s - ↑(n + 1) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))

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 : ↑n ≤ s
⊢ (s - ↑(n + 1) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
R' : Type u_3
inst✝ : CommRing R'
φ : R →+* R'
v w : Fin n → R
⊢ (projVandermonde (fun i ↦ φ (v i)) fun i ↦ φ (w i)) = φ.mapMatrix (projVandermonde v w)

Tactic:
by
  ext i j
  simp [projVandermonde_apply]

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 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ (sSup (range fun i ↦ s i)).toIdeal = ⨆ i, (s i).toIdeal

Tactic:
toIdeal_sSup,

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 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ ⨆ s_1 ∈ range fun i ↦ s i, s_1.toIdeal = ⨆ i, (s i).toIdeal
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ weightedTotalDegree 1 p = 0 ↔ p.IsHomogeneous 0

Tactic:
← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous 1 p 0 ↔ p.IsHomogeneous 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ X a ^ b * (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ (b + degree f)

Tactic:
pow_add

Goal state after:
case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ X a ^ b * (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ b * homogeneousSubmodule σ R 1 ^ degree f
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
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m 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 := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : (φ ^ n) x = 0
⊢ ↑((restrict φ hφV ^ n) ⟨x, ⋯⟩) = (φ ^ n) x

Tactic:
generalize_proofs h'

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
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : (φ ^ n) x = 0
h' : x ∈ φ.maxGenEigenspace 0
⊢ ↑((restrict φ hφV ^ n) ⟨x, h'⟩) = (φ ^ n) x
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
⊢ J l R * -J l R = 1

Tactic:
Matrix.mul_neg,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ -(J l R * J l R) = 1
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
rw [mem_iff'] at hA

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ B * A * A.adjugate = A.det • B

Tactic:
Matrix.mul_assoc,

Goal state after:
m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ B * (A * A.adjugate) = A.det • B
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case pos
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∈ s
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j

Tactic:
rw [Fintype.sum_eq_single (⟨i, hi⟩ : {x // x ∈ s})
        fun a ha => by rw [if_neg fun he => ha (Subtype.ext he), zero_mul], if_pos rfl, one_mul]

Goal state after:
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ψ : 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

Tactic:
ne_eq,

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.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
s : Finset K
hs : r ≤ s.card
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) v ^ k) z' ≠ 0

Tactic:
apply Nat.find_min hz'; lia

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

Goal state before:
pp: case zero
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
w : A
x : V
U : Submodule R V := ⨆ k, U' k
hx : x ∈ U.carrier
⊢ Submodule.map (T χ w) (U' 0) ≤ U

Tactic:
simp [U']

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  rw [next_getElem _ hl, formPerm_apply_getElem _ hl]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ (fun x ↦ l₁.formPerm) ≍ fun x ↦ l₂.formPerm

Tactic:
by
    apply Function.hfunext
    · ext
      exact h.nodup_iff
    · intro h₁ h₂ _
      exact heq_of_eq (formPerm_eq_of_isRotated h₁ h)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
a : A
ha : a ∈ (F (x + y)).support
⊢ a ∈ u

Tactic:
replace ha : F x a + F y a ≠ 0 := by simpa using ha
          grind

Goal state after: