mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n : M
x y : L
f : M →ₗ[R] N
⊢ { toFun := fun m ↦ ⁅x + y, f m⁆ - f ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext n
    simp only [add_lie, coe_mk, AddHom.coe_mk, add_apply, map_add]
    abel

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
a : R
ha : a ∈ R⁰
⊢ IsUnit a

Tactic:
isUnit_iff_isRegular_of_mulOpposite,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
a : R
ha : a ∈ R⁰
⊢ IsRegular a
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
a : R
⊢ IsUnit a ↔ a ∈ R⁰

Tactic:
isUnit_iff_isRegular_of_mulOpposite,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
a : R
⊢ IsRegular a ↔ a ∈ R⁰
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
⊢ IsUnit.submonoid R = R⁰

Tactic:
by
  ext; simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ IsZero ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (homOfLE ⋯)))

Tactic:
apply Y.isZero₁_of_isThirdQuadrant

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ WithBotTop.coe 0 < coreE₂Cohomological.i₁ (p, q)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L'' : LieSubalgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
h :
  (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ } =
    (fun L' ↦ L'.carrier) L''
⊢ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ } = L''

Tactic:
rcases L'' with ⟨⟨⟩⟩

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
h :
  (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹, lie_mem' := lie_mem'✝¹ } =
    (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹, lie_mem' := lie_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ }
Module: Mathlib.Algebra.Lie.OfAssociative

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
inst✝ : LieModule R L M
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo ⇑(((toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N

Tactic:
by
  rw [Module.End.coe_pow]
  exact MapsTo.iterate (fun m hm ↦ N.sub_mem (N.lie_mem hm) (N.smul_mem _ hm)) k

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

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : ↑⟨y, hy⟩ ∈ K
⊢ ⁅↑⟨x, hx⟩, ↑⟨y, hy⟩⁆ ∈ K

Tactic:
exact h' x y hx hy'

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
⊢ f.IsIdealMorphism

Tactic:
rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
    LieIdeal.top_toLieSubalgebra]

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

Goal state before:
pp: case refine_4
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
⊢ ∀ x ∈ Submodule.span R s, ⁅y, x⁆ ∈ Submodule.span R s → ⁅y, t • x⁆ ∈ Submodule.span R s

Tactic:
m''

Goal state after:
case refine_4
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
m'' : M
⊢ m'' ∈ Submodule.span R s → ⁅y, m''⁆ ∈ Submodule.span R s → ⁅y, t • m''⁆ ∈ Submodule.span R s
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ ↑f (z₁ + z₂) ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
rw [map_add, f.coe_toLinearMap, LieHom.mem_ker.mp hz₂, add_zero]

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ f z₁ ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)
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
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ⨆ i, ↑(N i) = ⊤ ↔ ⨆ i, N i = ⊤

Tactic:
by
  rw [← iSup_toSubmodule, ← top_toSubmodule (L := L), toSubmodule_inj]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
hf : ⁅x, (↑f).toFun m⁆ = (↑f).toFun ⁅x, m⁆
⊢ (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆

Tactic:
exact hf.symm

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ False

Tactic:
have eq_one : minpoly A x = 1 := by
    rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
    convert C_1 (R := A)
    simpa only [ndeg_eq_zero.symm] using! (monic hx).leadingCoeff

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
eq_one : minpoly A x = 1
⊢ False
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
rw [← I.incl_idealRange]

Goal state after:
case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x✝ x : R
⊢ (aeval x✝) ((fun a ↦ C a) x) = x

Tactic:
by
    exact eval_C

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
this : C (i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ (mapRingHom i) f = C (i y)
⊢ C y - f ∈ RingHom.ker (mapRingHom i)

Tactic:
rw [RingHom.mem_ker, map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R[X]
⊢ IsField R

Tactic:
apply (quotientSpanXSubCAlgEquiv 0).symm.toMulEquiv.isField

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R[X]
⊢ IsField (R[X] ⧸ span {X - C 0})
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ (aeval x) (minpoly A pb.gen) = 0 ↔ (Equiv.refl B) x ∈ (minpoly A pb.gen).aroots B

Tactic:
rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ (aeval x) (minpoly A pb.gen) = 0 ↔ (aeval x) (map (algebraMap A B) (minpoly A pb.gen)) = 0

R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ map (algebraMap A B) (minpoly A pb.gen) ≠ 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
by_cases h : IsIntegral K x; swap
  · rw [minpoly.eq_zero h, natDegree_zero]
    exact linearIndependent_empty_type
  refine Fintype.linearIndependent_iff.2 fun g hg i => ?_
  simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg
  apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_gt).mtr
  · simp_rw [← C_mul_X_pow_eq_monomial]
    exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _
  · apply_fun lcoeff K i at h0
    simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0
    exact (if_pos <| Finset.mem_univ _).symm.trans h0

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬Squarefree 0

Tactic:
Squarefree,

Goal state after:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬∀ (x : R), x * x ∣ 0 → IsUnit x
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x : R
h0 : x ≠ 0
h : IsRadical x
⊢ Squarefree x

Tactic:
by
  rintro z ⟨w, rfl⟩
  specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩
  rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h
  rw [mul_assoc, mul_ne_zero_iff] at h0; exact h0.2

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

Goal state before:
pp: n : ℤ
⊢ Squarefree n.natAbs ↔ Squarefree n

Tactic:
Squarefree,

Goal state after:
n : ℤ
⊢ (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ (f * g).Separable

Tactic:
rw [separable_def, derivative_mul]

Goal state after:
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g) (derivative f * g + f * derivative g)
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
⊢ annIdealGenerator 𝕜 a = p

Tactic:
by
  by_cases h : p = 0
  · rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
  · rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
    rw [eq_comm]
    apply eq_of_monic_of_associated p_monic _ p_gen
    apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ f = 0

Tactic:
simpa [h] using f.eq_smul_basis_det e

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ ((b.reindex e).toMatrix v).det = b.det (v ∘ ⇑e)

Tactic:
toMatrix_reindex',

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ ((reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e))).det = b.det (v ∘ ⇑e)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₁
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]
hg : g.Monic
i : Fin g.natDegree
⊢ i ∉ Finset.univ → (monomial ↑i) (Pi.single i 1 i) = 0

Tactic:
· intros
      have := Finset.mem_univ i
      contradiction

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
⊢ a.IsSemisimple

Tactic:
let S := AdjoinRoot ((minpoly K g).map <| algebraMap K R)

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
⊢ a.IsSemisimple
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case succ.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ ((aeval x) P ^ 2 ^ n) ^ 2 ∣
    Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) ^ 2 * (aeval (P.newtonMap^[n] x)) P ^ 2

Tactic:
exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd ih 2) _

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)

Tactic:
apply dvd_nsmul_of_dvd

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ y ^ p

Tactic:
← neg_neg y,

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (- -y) ^ p
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
n : ℕ
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L n = ⊤

Tactic:
cases n

Goal state after:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L 0 = ⊤

case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
n✝ : ℕ
⊢ derivedSeries R L (n✝ + 1) = ⊤
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))

Tactic:
intro a₃

Goal state after:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
⊢ ∀ (y : M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (a₃ ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (a₃ ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (a₃ ⊗ₜ[R] y))
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
⊢ ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
induction l with
  | zero =>
    simp only [add_zero, LieIdeal.lcs_succ, pow_zero, Module.End.one_eq_id,
      Submodule.map_id]
    exact le_sup_of_le_left hIM
  | succ l ih =>
    simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]
    refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
    · rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]
      grw [coe_map_toEnd_le]
    · norm_cast
      gcongr
      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

Goal state after:
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
k : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
inst✝² : LieModule R L M₂
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
⊢ ∃ k, lowerCentralSeries ℤ L M k = ⊥

Tactic:
use 1; simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
⊢ ∀ {x y : L ⧸ f.ker}, (↑f).quotKerEquivRange ⁅x, y⁆ = ⁅(↑f).quotKerEquivRange x, (↑f).quotKerEquivRange y⁆

Tactic:
intro x y
      induction x using Submodule.Quotient.induction_on
      induction y using Submodule.Quotient.induction_on
      rw [← SetLike.coe_eq_coe, LieSubalgebra.coe_bracket f.range]
      simp only [← LieSubmodule.Quotient.mk_bracket, LinearMap.quotKerEquivRange_apply_mk,
        coe_toLinearMap, map_lie]

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

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hnp : _root_.IsNilpotent ((toEnd R L M) x)
hIM : LieModule.IsNilpotent (↥I) M
⊢ LieModule.IsNilpotent L M

Tactic:
by
  obtain ⟨n, hn⟩ := hnp
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R I M
  have hk' : I.lcs M k = ⊥ := by
    simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]
  suffices ∀ l, lowerCentralSeries R L M (l * n) ≤ I.lcs M l by
    rw [isNilpotent_iff R]
    use k * n
    simpa [hk'] using this k
  intro l
  induction l with
  | zero => simp
  | succ l ih => exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih

Goal state after: