mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

pp: case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : b ≤ a
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Tactic:
· rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
      rw [tsub_eq_zero_iff_le.mpr h, zero_add]

Goal state after:
case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : b ≤ a
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)
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
s : Finset ι
v : ι → F
c : F
f : ι → F
⊢ ∑ x ∈ s, (c • f) x • Lagrange.basis s v x = ∑ x ∈ s, ((RingHom.id F) c * f x) • Lagrange.basis s v x

Tactic:
Pi.smul_apply,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v : ι → F
c : F
f : ι → F
⊢ ∑ x ∈ s, (c • f x) • Lagrange.basis s v x = ∑ x ∈ s, ((RingHom.id F) c * f x) • Lagrange.basis s v x
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✝ : Nontrivial L₂
this✝³ : Fintype ι₁
this✝² : Fintype ι₂
this✝¹ : H₁.IsCartanSubalgebra
this✝ : H₂.IsCartanSubalgebra
this : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
⊢ False

Tactic:
have (x : H₁ × H₂) (hx) : ⟨(x.1, x.2), hx⟩ ∈ prodCartan eι b₁ b₂ := by
    rw [← mem_toLieSubmodule, ← rootSpace_zero_eq, LieModule.mem_genWeightSpace]
    refine fun ⟨y, hy⟩ ↦ ⟨1, ?_⟩
    simpa [Subtype.ext_iff] using ⟨lie_fst_eq_zero_of_mem_prodCartan eι b₁ b₂ hy x.fst,
      lie_snd_eq_zero_of_mem_prodCartan eι b₁ b₂ hy x.snd⟩

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₂
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✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
⊢ False
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)

Tactic:
simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars ⊆ (∏ i ∈ d.support, f i ^ d i).vars

Tactic:
simp only [Finset.empty_union, vars_C, Finset.Subset.refl]

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
i : ι
hi : i ∈ s
⊢ (∏ x ∈ s.erase i, C (v i - v x)⁻¹) * ∏ x ∈ s.erase i, (X - C (v x)) =
    (∏ x ∈ s.erase i, C (v i - v x)⁻¹) * nodal (s.erase i) v

Tactic:
nodal

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
w : σ → M
m : M
a b : MvPolynomial σ R
ha : a ∈ {x | IsWeightedHomogeneous w x m}
hb : b ∈ {x | IsWeightedHomogeneous w x m}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c b ≠ 0
⊢ (weight w) c = m

Tactic:
exact hb h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
⊢ m = n

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
  rw [← hm hd, ← hn hd]

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 𝒜
i : ι
r : A
x✝ : r ∈ ⊤
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊤

Tactic:
by simp only [Submodule.mem_top]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
⊢ m = n

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
  rw [← hm hd, ← hn hd]

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

Goal state before:
pp: 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
⊢ V = ⨆ n, ker (φ ^ n)

Tactic:
simp [V, ← Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_nat]

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

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = 0
⊢ F = 0

Tactic:
apply eq_zero_of_forall_eval_eq_zero_of_le_card hF h

Goal state after:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = 0
⊢ ↑n ≤ #R
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
ι' : Type u_6
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✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree

Tactic:
by
  apply le_antisymm <;> apply nilRankAux_le

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

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
simp [Pso, indefiniteDiagonal, h, one_apply]

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

Goal state before:
pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
simp [Pso, indefiniteDiagonal, h, one_apply]

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
i : R
hi : i * i = -1
⊢ ↥(so' p q R) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)

Tactic:
apply
    (skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i)
        (invertiblePso p q R hi)).trans

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
i : R
hi : i * i = -1
⊢ ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ A.eRank ≤ ENat.card n

Tactic:
wlog hfin : Finite n
  · simp [ENat.card_eq_top.2 (by simpa using hfin)]
  have _ := Fintype.ofFinite n
  rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_natCast]
  exact A.cRank_le_card_width

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
⊢ M.rank = Fintype.card m

Tactic:
rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑d), map_add' := ⋯, map_smul' := ⋯ } ⁅x, y⁆ =
    ⁅x, { toFun := ⇑(LinearMap.rTensor L ↑d), map_add' := ⋯, map_smul' := ⋯ } y⁆ -
      ⁅y, { toFun := ⇑(LinearMap.rTensor L ↑d), map_add' := ⋯, map_smul' := ⋯ } x⁆

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk]
        refine x.induction_on (by simp) (fun _ l ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
        · refine y.induction_on (by simp) (fun _ l' ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
          · simp [← lie_skew l' l, -lie_skew, add_tmul, tmul_neg]
          · simp [h1, h2, sub_add_sub_comm]
        · simp [h1, h2, sub_add_sub_comm]

Goal state after:
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
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
⊢ fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D

Tactic:
rw [← M.fromBlocks_toBlocks, fromBlocks_multiply]

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
⊢ fromBlocks (1 * M.toBlocks₁₁ + X * M.toBlocks₂₁) (1 * M.toBlocks₁₂ + X * M.toBlocks₂₂)
      (0 * M.toBlocks₁₁ + 1 * M.toBlocks₂₁) (0 * M.toBlocks₁₂ + 1 * M.toBlocks₂₂) =
    fromBlocks (A + X * C) (B + X * D) C D
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd (Multiplicative.ofAdd m))))
      (r • ⟨single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m r, ⋯⟩

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Goal state after:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ GradedMonoid.mk (f (Multiplicative.toAdd (Multiplicative.ofAdd m)))
      (r • ⟨single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    GradedMonoid.mk (f m) ⟨single m r, ⋯⟩
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) (⟨single m b, ⋯⟩ + ⟨y, h2⟩) =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ⋯
⊢ GradedMonoid.mk (f m) (⟨single m b, ⋯⟩ + ⟨y, h2⟩) = GradedMonoid.mk (f m) ⟨single m b + y, hmby⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

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

Tactic:
rw [← length_attach] at hn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inr
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
⊢ χ ⁅z, a⁆ = 0

Tactic:
have trace_za_zero : (LieModule.toEnd R A _ ⁅z, a⁆).trace R U = 0 := by
    have hres : LieModule.toEnd R A U ⁅z, a⁆ = ⁅(π z).restrict hzU, LieModule.toEnd R A U a⁆ := by
      ext ⟨x, hx⟩
      change ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆
      simp only [leibniz_lie z a, add_sub_cancel_right]
    rw [hres, LinearMap.trace_lie]

Goal state after:
case inr
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
⊢ χ ⁅z, a⁆ = 0
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
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) (l.formPerm.cycleOf (l.get ⟨0, ⋯⟩)).support.card = l

Tactic:
hc.cycleOf_eq (mem_support.mp _),

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.formPerm.support.card = l

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.get ⟨0, ⋯⟩ ∈ l.formPerm.support
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
f : L₁ →ₗ⁅σ₁₂⁆ L₂
g : L₂ →ₗ⁅σ₂₃⁆ L₃
x✝¹ : A₁
x✝ : L₁
⊢ (σ₂₃.comp σ₁₂) ⁅x✝, x✝¹⁆ = ⁅(g.comp f.toLieHom) x✝, (σ₂₃.comp σ₁₂) x✝¹⁆

Tactic:
by simp [f.apply_lie, g.apply_lie]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
b : Associates M
hb : b ∈ normalizedFactors r
⊢ b = c 1

Tactic:
refine
        eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
          (dvd_of_mem_normalizedFactors hb)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
h : I = 0
x : P
hx : x ∈ I
⊢ x = 0

Tactic:
simpa [h, mem_zero_iff] using hx

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Ideal R
⊢ ↑(I * J) = ↑I * ↑J

Tactic:
by
  simp only [mul_def]
  exact coeToSubmodule_injective (coeSubmodule_mul _ _ _)

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

Goal state before:
pp: ⊢ E₈.det = 1

Tactic:
simp only [E₈, norm_det]

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

Goal state before:
pp: n : ℕ
⊢ (A n).IsSimplyLaced

Tactic:
by
  intro i j h
  simp only [A, of_apply]
  grind

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_zero_weight : H.toLieSubmodule.incl y ∈ genWeightSpace L 0
⊢ ⇑χ = ⇑χ + 0

Tactic:
ext h

Goal state after:
case e'_4
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_zero_weight : H.toLieSubmodule.incl y ∈ genWeightSpace L 0
h : ↥H
⊢ χ h = (⇑χ + 0) h
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
⊢ y * b ∈ J

Tactic:
apply hle

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := ⋯
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
⊢ y * b ∈ (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ I = 1

Tactic:
simp_rw [@SetLike.ext_iff _ _ _ I 1, mem_one_iff]

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ ∀ (x : L), x ∈ I ↔ ∃ x', (algebraMap K L) x' = x