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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R A).Finite

Tactic:
rw [← AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv <| Pi.basisFun R n) A]
  exact Module.End.finite_spectrum _

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

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

Tactic:
descPochhammer_succ_left

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (descPochhammer ℤ (n + 1)).comp (X - 1) =
    X * (descPochhammer ℤ n).comp (X - 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
⊢ eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, ↑k = -r

Tactic:
refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
zero' : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n, ↑k = -r

case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, ↑k = -r
⊢ eval r (ascPochhammer R n) = 0
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i j : ι₁
hij : i ≠ j
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ j⁆ = 0

Tactic:
have hij' : eι i ≠ eι j := by aesop

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i j : ι₁
hij : i ≠ j
hij' : eι i ≠ eι j
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ j⁆ = 0
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: case mem
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₁
this : IsLieAbelian ↥H₁
u : ↥(prod eι b₁ b₂)
hu : u ∈ {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
⊢ ⁅(↑u).1, ↑x⁆ = 0

Tactic:
| mem u hu =>

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₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
hy : y ∈ prodCartan eι b₁ b₂
x : ↥H₁
this : IsLieAbelian ↥H₁
⊢ ⁅(↑y).1, ↑x⁆ = 0

Tactic:
induction hy using lieSpan_induction with

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: n : ℕ
v : Fin (n + 1) → ℤ
⊢ ↑n.superFactorial ∣ (vandermonde v).det

Tactic:
let m := inf' univ ⟨0, mem_univ _⟩ v

Goal state after:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
⊢ ↑n.superFactorial ∣ (vandermonde v).det
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]
hP : P.degree < ↑(#s)
⊢ (∑ i ∈ s, C (eval (v i) P) * Lagrange.basis s v i).coeff (#s - 1) =
    ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
finsetSum_coeff

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]
hP : P.degree < ↑(#s)
⊢ ∑ b ∈ s, (C (eval (v b) P) * Lagrange.basis s v b).coeff (#s - 1) =
    ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
x✝ : ∃ q, ∀ (i : ι), eval (x i) q = y i
i j : ι
hij : x i = x j
q : F[X]
hq : ∀ (i : ι), eval (x i) q = y i
⊢ y i = y j

Tactic:
rw [← hq, ← hq, hij]

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✝ : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
⊢ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) m ≤ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) n

Tactic:
intro y hy
    rw [LinearMap.mem_ker] at hy ⊢
    exact Module.End.pow_map_zero_of_le hmn hy

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ↑(Fintype.card ↑↑G) = Fintype.card ↥G • 1

Tactic:
nsmul_eq_mul,

Goal state after:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ↑(Fintype.card ↑↑G) = ↑(Fintype.card ↥G) * 1
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
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
q : K[X]
hq : ∀ (i : I), Polynomial.eval (μ i) q = fμ i
⊢ y ∈ (aeval s).range

Tactic:
refine ⟨q, v.ext fun i ↦ ?_⟩

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
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
q : K[X]
hq : ∀ (i : I), Polynomial.eval (μ i) q = fμ i
i : I
⊢ ((aeval s).toRingHom q) (v i) = y (v i)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
⊢ IsNilpotent (↥(derivedSeries R L 1)) M

Tactic:
have nilp_ext : IsNilpotent (derivedSeries A (A ⊗[R] L) 1) (A ⊗[R] M) :=
    isNilpotent_derivedSeries_of_traceForm_eq_zero_aux <| by simpa

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext : IsNilpotent (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)
⊢ IsNilpotent (↥(derivedSeries R L 1)) M
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
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨅ i, f i)

Tactic:
intro i x hx
  simp only [Ideal.mem_iInf] at hx ⊢
  exact fun j => h _ _ (hx j)

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
inst✝ : IsNoetherian R M
φ : End R M
⊢ [IsNilpotent φ, charpoly φ = X ^ finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0,
      (charpoly φ).natTrailingDegree = finrank R M].TFAE

Tactic:
tfae_have 1 → 2 := IsNilpotent.charpoly_eq_X_pow_finrank
  tfae_have 2 → 3
  | h, m => by
    use finrank R M
    suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
    simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly
  tfae_have 3 → 1
  | h => by
    obtain ⟨n, hn⟩ := Filter.eventually_atTop.mp <| φ.eventually_iSup_ker_pow_eq
    use n
    ext x
    rw [zero_apply, ← mem_ker, ← hn n le_rfl]
    obtain ⟨k, hk⟩ := h x
    rw [← mem_ker] at hk
    exact Submodule.mem_iSup_of_mem _ hk
  tfae_have 2 ↔ 4 := by
    rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
  tfae_finish

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h : ∀ (T S : Module.End R (n → R)), f (T ∘ₗ S) = f T * f S
⊢ f (T ∘ₗ S - S ∘ₗ T) = f T * f S - f S * f T

Tactic:
rw [map_sub, h, h]

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

Goal state before:
pp: R : 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
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
⊢ Polynomial.map (evalRingHom r)
      (Polynomial.map
        (↑(MvPolynomial.aeval fun i ↦ C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i)))
        ((↑φ).polyCharpoly (chooseBasis R L))) =
    charpoly (φ (r • y + x))

Tactic:
map_map

Goal state after:
R : 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
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
⊢ Polynomial.map
      ((evalRingHom r).comp
        ↑(MvPolynomial.aeval fun i ↦ C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i)))
      ((↑φ).polyCharpoly (chooseBasis R L)) =
    charpoly (φ (r • y + x))
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 (fromBlocks 1 0 0 (S l R))

Tactic:
simp [indefiniteDiagonal_assoc, S]

Goal state after:
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:
rw [Matrix.mul_assoc, Matrix.mul_adjugate, Matrix.mul_smul, Matrix.mul_one]

Goal state after:
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
inst✝ : Infinite K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
apply exists_isCartanSubalgebra_engel_of_finrank_le_card

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
inst✝ : Infinite K
⊢ ↑(finrank K L) ≤ #K
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x : FreeLieAlgebra R X), Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x x = 0

Tactic:
by rintro ⟨a⟩; exact Quot.sound (Rel.lie_self a)

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
m : M
h : m ∈ (coeff 0).support
⊢ f m = i

Tactic:
by cases h

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
⊢ f (ma + mb) = i + j

Tactic:
rw [map_add, ha ma hma, hb mb hmb]

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case mem
L : Type u_2
M : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
R : Type u_4
inst✝³ : CommRing R
inst✝² : LieAlgebra R L
inst✝¹ : Module R M
inst✝ : LieModule R L M
s : Set L
hs : ∀ x ∈ s, (trace R M) ((toEnd R L M) x) = 0
x u : L
hu : u ∈ s
⊢ (trace R M) ((toEnd R L M) u) = 0

Tactic:
| mem u hu =>

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
⊢ l.formPerm x = x ∨ l'.formPerm x = x

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
⊢ l.formPerm x = x ∨ l'.formPerm x = x

Tactic:
all_goals have := List.formPerm_apply_of_notMem ‹_›; tauto

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
⊢ (p.toList x).Nodup

Tactic:
have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
hc : (p.cycleOf x).IsCycle
⊢ (p.toList x).Nodup
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
hc : (p.cycleOf x).IsCycle
⊢ Function.Injective fun i ↦ (p.toList x)[↑i]

Tactic:
intro ⟨n, hn⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn : n < (p.toList x).length
⊢ ∀ ⦃a₂ : Fin (p.toList x).length⦄, (fun i ↦ (p.toList x)[↑i]) ⟨n, hn⟩ = (fun i ↦ (p.toList x)[↑i]) a₂ → ⟨n, hn⟩ = a₂
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
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
E : Extension R M L
y : M
z : E.L
⊢ Exists.choose ⋯ (E.proj z) - z ∈ E.incl.range

Tactic:
rw [E.IsExtension.exact]

Goal state after:
R : Type u_1
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
E : Extension R M L
y : M
z : E.L
⊢ Exists.choose ⋯ (E.proj z) - z ∈ LieIdeal.toLieSubalgebra R E.L E.proj.ker
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ (∑ k ∈ Finset.range n, if ↑i < k then f k else 0) = ∑ k, if ↑i < ↑k then f ↑k else 0

Tactic:
rw [← Fin.sum_univ_eq_sum_range]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_3
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
⊢ ∃ i, y = (fun i ↦ p ^ ↑i) i

Tactic:
obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h

Goal state after:
case refine_3
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
i : ℕ
i_le : i ≤ n
hi : Associated y (p ^ i)
⊢ ∃ i, y = (fun i ↦ p ^ ↑i) i
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑(d.symm (d ⟨p, ⋯⟩))) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

Tactic:
rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑⟨p, ⋯⟩) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
⊢ False

Tactic:
have : I.rootSpan ≤ LinearMap.ker (Dual.eval K H (coroot (α : Weight K H L))) := by
    rw [LieIdeal.rootSpan, Submodule.span_le]
    rintro _ ⟨γ, hγ, rfl⟩
    simp only [SetLike.mem_coe, LinearMap.mem_ker, Dual.eval_apply, rootSystem_root_apply]
    exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hγ hα_not

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
this : I.rootSpan ≤ LinearMap.ker ((Dual.eval K ↥H) (coroot ↑α))
⊢ False
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ x ≠ 0

pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ (algebraMap R K) x ∈ I

Tactic:
· rw [Ne, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]
    exact mul_ne_zero (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors z.2) y_ne_zero

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ (algebraMap R K) x ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ I * (1 / I) ≤ 1

Tactic:
rw [hI, div_zero, mul_zero]

Goal state after:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ 0 ≤ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

Tactic:
· simp [← coeToSubmodule_inj, div_of_ne_zero H, div_of_ne_zero (map_ne_zero _ H)]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
⊢ I / J = I * J⁻¹

Tactic:
obtain rfl | hJ := eq_or_ne J 0
    · simp [inv_zero']
    refine le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_)
    · suffices I / J * J ≤ I by
        simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this
      simp [FractionalIdeal.mul_le, mem_div_iff_of_ne_zero hJ]
    · rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0

Tactic:
simp only [← coeToSubmodule_inj, spanFinset_coe, coe_zero, Submodule.span_eq_bot,
    Set.mem_image, Finset.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Goal state after: