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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤

Tactic:
by
  -- A little off-by-one cleanup first:
  rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
  · use n + 1
    rintro (_ | m) p
    · cases p
    · apply w
      exact Nat.succ_le_succ_iff.mp p
  obtain ⟨n, w⟩ := monotone_stabilizes (partialSups (OrderDual.toDual ∘ f))
  refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
  simpa only [partialSups_add_one] using! (w (m + 1) <| le_add_right p).symm.trans <| w m p

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

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
M : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
x y : L₁
m : M
⊢ ⁅f x, ⁅f y, m⁆⁆ = ⁅f ⁅x, y⁆, m⁆ + ⁅f y, ⁅f x, m⁆⁆

Tactic:
simp only [lie_lie, sub_add_cancel, LieHom.map_lie]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range

Tactic:
refine eventually_atTop.mpr ⟨n, fun m hm ↦ codisjoint_iff.mpr ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
⊢ (f ^ m).ker ⊔ (f ^ m).range = ⊤
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ (lieSpan R L ↑p).toSubmodule → ⁅x, m⁆ ∈ (lieSpan R L ↑p).toSubmodule

Tactic:
mem_toSubmodule

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ lieSpan R L ↑p → ⁅x, m⁆ ∈ (lieSpan R L ↑p).toSubmodule
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.idealRange = I

Tactic:
rw [LieHom.idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, incl_range, toLieSubalgebra_toSubmodule,
    LieSubmodule.coe_lieSpan_submodule_eq_iff]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ∃ N, ↑N = ↑I
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ ↑(lieSpan R L ↑p)

Tactic:
mem_toSubmodule

Goal state after:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
m : M
hm : m ∈ p
⊢ ⁅x, m⁆ ∈ lieSpan R L ↑p
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m : M
hm : m ∈ ↑N
N' : Submodule R M
hN' : ∀ m ∈ N, ↑(lieSpan R L {m}) ≤ N'
⊢ m ∈ N'

Tactic:
exact hN' _ hm (subset_lieSpan rfl)

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆

Tactic:
by
  rw [le_inf_iff]; constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ pb.minpolyGen.Monic

Tactic:
apply (monic_X_pow _).sub_of_left _

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ (∑ i, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < (X ^ pb.dim).degree
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.lmul A S) pb.gen =
    (LinearMap.toMatrix pb.basis pb.basis).symm
      (Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0)

Tactic:
LinearMap.toMatrix_symm

Goal state after:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.lmul A S) pb.gen =
    (Matrix.toLin pb.basis pb.basis)
      (Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse ⇑(Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
    ⇑(eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))

Tactic:
by
    rintro ⟨f⟩
    refine Polynomial.induction_on' f ?_ ?_
    · intro p q hp hq
      simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, map_add, Quotient.lift_mk,
        coe_eval₂RingHom] at hp hq ⊢
      rw [hp, hq]
    · intro n a
      simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk,
        Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk,
        coe_eval₂RingHom, map_pow, eval₂_C, RingHom.coe_comp, map_mul, eval₂_X,
        Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ↑2 ≤ emultiplicity a r → IsUnit a ↔ ¬emultiplicity a r ≤ 1 → IsUnit a

Tactic:
not_le,

Goal state after:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ↑2 ≤ emultiplicity a r → IsUnit a ↔ 1 < emultiplicity a r → IsUnit a
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mpr.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
hu : ¬IsUnit 0
⊢ emultiplicity 0 x ≤ 1

pp: case mpr.inr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
⊢ emultiplicity a x ≤ 1

Tactic:
· simp [x0]

Goal state after:
case mpr.inr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
⊢ emultiplicity a x ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h1 : ∀ x ∈ insert a s, ∀ y ∈ insert a s, x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ x ∈ insert a s, (f x).Separable
⊢ (∏ x ∈ insert a s, f x).Separable

Tactic:
simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2

Goal state after:
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (∏ x ∈ insert a s, f x).Separable
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
rcases H with ⟨s, ⟨b⟩⟩
      rw [← det_toMatrix b f, ← det_toMatrix (b.map e), toMatrix_comp (b.map e) b (b.map e),
        toMatrix_comp (b.map e) b b, ← Matrix.mul_assoc, Matrix.det_conj_of_mul_eq_one]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
this :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]},
    Irreducible f →
      0 < p →
        ∀ (n₁ n₂ : ℕ),
          n₁ ≤ n₂ →
            ∀ (g₁ : F[X]),
              g₁.Separable →
                (expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : g₁.Separable
Hg₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
⊢ (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂

Tactic:
Hg₂

Goal state after:
case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
this :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]},
    Irreducible f →
      0 < p →
        ∀ (n₁ n₂ : ℕ),
          n₁ ≤ n₂ →
            ∀ (g₁ : F[X]),
              g₁.Separable →
                (expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : g₁.Separable
Hg₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
Hg₂ : (expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Tactic:
Fintype.card_eq_nat_card,

Goal state after:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits
⊢ Nat.card (S →ₐ[K] L) = pb.dim
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by
    rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]; rfl

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₁
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
x✝ : K
⊢ (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)).comp C) x✝ = ((mk f).comp C) x✝

Tactic:
simp only [RingHom.comp_apply, mk_C, lift_of]
      rfl

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * C f.leadingCoeff⁻¹
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)

Tactic:
have deg_f' : f'.natDegree = f.natDegree := by
    rw [natDegree_mul hf, natDegree_C, add_zero]
    · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * C f.leadingCoeff⁻¹
deg_f' : f'.natDegree = f.natDegree
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p → ∃ a_2 ≤ p, ∃ (x : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), ⟨a ⊓ a_2, ⋯⟩ = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
exists_and_right,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p → ∃ a_2 ≤ p, (∃ (x : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), ⟨a ⊓ a_2, ⋯⟩ = ⊥) ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
i : ℕ
hk : f ^ i = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i_1, ∃ (_ : i_1 ≤ i), (f ^ i_1) x = x_1}
hi : i ≤ i
⊢ f ((f ^ i) x) ∈ {x_1 | ∃ i_1, ∃ (_ : i_1 ≤ i), (f ^ i_1) x = x_1}

Tactic:
· exact ⟨i, by simp [hk]⟩

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
by
  rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply,
    RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
    Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk, ←
    RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
    quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk,
    quotMapOfEquivQuotMapCMapMk_symm_mk]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆

Tactic:
by
  rw [LieDerivation.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i !)⁻¹ * ↑(i ! / (j ! * (i - j)!)) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹

Tactic:
Nat.cast_div (Nat.factorial_mul_factorial_dvd_factorial hj) (by positivity)

Goal state after:
case calc_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i !)⁻¹ * (↑i ! / ↑(j ! * (i - j)!)) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
x : L
⊢ (IsNilpotent.exp ↑D).toFun ((fun x ↦ (IsNilpotent.exp (-↑D)) x) x) = x

Tactic:
by
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ← LinearMap.comp_apply,
        ← Module.End.mul_eq_comp, h.exp_mul_exp_neg_self, Module.End.one_apply]

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommRing R
L : Type v
M : Type w
N : Type w₁
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x : L
m : M
n : N
⊢ (hasBracketAux x) (m ⊗ₜ[R] n) = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆

Tactic:
simp only [hasBracketAux, LinearMap.rTensor_tmul, toEnd_apply_apply,
      LinearMap.add_apply, LinearMap.lTensor_tmul]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ x ∈ H.toSubmodule

Tactic:
mem_toSubmodule

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ x ∈ H
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s

Tactic:
intro k₁ k₂ h₁₂ h₁

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
⊢ k₂ ∈ s
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (m • (C r * X ^ (n + 1))) = m • eval x (C r * X ^ (n + 1))

Tactic:
smul_mul',

Goal state after:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (m • C r * m • X ^ (n + 1)) = m • eval x (C r * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ m • r * (m • x) ^ (n + 1) = m • (r * x ^ (n + 1))

Tactic:
smul_mul',

Goal state after:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ m • r * (m • x) ^ (n + 1) = m • r * m • x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ X - g • C (ofQuotientStabilizer G x g') = X - C (g • ofQuotientStabilizer G x g')

Tactic:
Polynomial.smul_C

Goal state after:
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ X - C (g • ofQuotientStabilizer G x g') = X - C (g • ofQuotientStabilizer G x g')
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ map (↑g) (m • (C b * X ^ (n + 1))) = m • map (↑g) (C b * X ^ (n + 1))

Tactic:
smul_mul',

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ map (↑g) (m • C b * m • X ^ (n + 1)) = m • map (↑g) (C b * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = m • (C (↑g b) * X ^ (n + 1))

Tactic:
smul_mul',

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = m • C (↑g b) * m • X ^ (n + 1)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂

Tactic:
by
  convert! lcs_add_le_iff (R := R) (L := L) (M := M) 0 k
  rw [zero_add]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m✝ : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
m : M
f : ↥(subfield M F)
f' : F
⊢ m • (↑f * f') = ↑f * m • f'

Tactic:
smul_mul',

Goal state after:
M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m✝ : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
m : M
f : ↥(subfield M F)
f' : F
⊢ m • ↑f * m • f' = ↑f * m • f'