mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)

Tactic:
by
  by_cases hx : IsIntegral A x
  · refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
        ?_ fun q qmo hq => ?_).symm
    · simp [aeval_comp]
    · have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0 := by
        simpa [aeval_comp] using hq
      have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X this
      simp_all
  · rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
    · simp only [natDegree_zero, pow_zero, mul_zero]
    · exact IsIntegral.neg_iff.not.mpr hx

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ x₁ - x₂ ≡ y₁ - y₂ [SMOD U]

Tactic:
by
  rw [SModEq.def] at hxy₁ hxy₂ ⊢
  simp_rw [Quotient.mk_sub, hxy₁, hxy₂]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ minpoly K σ.toLinearMap = minpoly K ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

Tactic:
apply congr_arg
    ext
    simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ((Quotient.mk (map C I)).comp C) a = 0

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ (Quotient.mk (map C I)) (C a) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) a = 0

Tactic:
← sum_monomial_eq a

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) (a.sum fun n a ↦ (monomial n) a) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ ((C.comp (Quotient.mk I)) (a.coeff n)).coeff m = coeff 0 m

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ (C ((Quotient.mk I) (a.coeff n))).coeff m = coeff 0 m
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
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
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

Tactic:
simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]
    convert! pb.aeval_minpolyGen
    rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]

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

Goal state before:
pp: case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((C.comp (Ideal.Quotient.mk I)) r) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)

Tactic:
RingHom.comp_apply,

Goal state after:
case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (C ((Ideal.Quotient.mk I) r)) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ (mk X) X = 0

Tactic:
mk_self

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
s : Finset M
hs : Basis (↥s) R M
⊢ Free R M

Tactic:
exact Module.Free.of_basis hs

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ Free R M

pp: case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ Free R M

Tactic:
· rcases H with ⟨s, ⟨hs⟩⟩
    exact Module.Free.of_basis hs

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ Free R M
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
H : derivative f = 0
HF : CharP F 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f

Tactic:
have := CharP.charP_to_charZero F

Goal state after:
case inl
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
H : derivative f = 0
HF : CharP F 0
this : CharZero F
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime.inl
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
f✝ : K[X]
hf : Irreducible f✝
h : f✝.Separable
⊢ f✝.Separable

Tactic:
assumption

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.succ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
n : ℕ
g : F[X]
hg4 : g.Separable
hg : Irreducible ((expand F (p ^ n)) g)
hgf : (expand F p) ((expand F (p ^ n)) g) = f
hg1 : ((expand F (p ^ n)) g).natDegree * p = N.succ
hg2 : ((expand F (p ^ n)) g).natDegree ≠ 0
hg3 : ((expand F (p ^ n)) g).natDegree < N.succ
⊢ (expand F (p ^ (n + 1))) g = f

Tactic:
rw [← hgf, expand_expand, pow_succ']

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots ≤ p • f.roots

Tactic:
convert! ← roots_expand_pow_map_iterateFrobenius_le p 1 f <;> apply pow_one

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✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i ↦ (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)

Tactic:
unfold B

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✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (toMatrix
        ((Pi.basis fun x ↦ b).reindex
          ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M))))
        ((Pi.basis fun x ↦ b).reindex
          ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))))
      (pi fun i ↦ f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i ↦ (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : 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 : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rw [eq_comm]

Goal state after:
case neg
𝕜 : 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 : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • ((mk f).comp C) x = ((mk f).comp C) (a • x)

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • (mk f) (C x) = ((mk f).comp C) (a • x)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • (mk f) (C x) = ((mk f).comp C) (a • x)

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • (mk f) (C x) = (mk f) (C (a • x))
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (mk f) f = 0

Tactic:
mk_self

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ 0 = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : ((mk f).comp C) p = 0
⊢ p = 0

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : (mk f) (C p) = 0
⊢ p = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
r : R
⊢ (map f p q h) ((of p) r) = (of q) (f r)

Tactic:
simp [map]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
⊢ (map f p q h) (root p) = root q

Tactic:
simp [map]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (basisFun R ι).det = detRowAlternating

Tactic:
by
  ext M
  rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose, det]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: 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
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)) q = 0

Tactic:
RingHom.comp_apply,

Goal state after:
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
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) ((mk q) q) = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hli
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
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K fun i ↦ root f ^ ↑i

Tactic:
← minpoly_eq

Goal state after:
case hli
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
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K fun i ↦ root f ^ ↑i
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hsp
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
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ y ∈ Submodule.span K (Set.range fun i ↦ root f ^ ↑i)

Tactic:
← minpoly_eq

Goal state after:
case hsp
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
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ y ∈ Submodule.span K (Set.range fun i ↦ root f ^ ↑i)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case inr
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
this :
  ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : End K M}
    (t : K), f.IsSemisimple → t ≠ 0 → (t • f).IsSemisimple
ht : ¬t ≠ 0
⊢ (t • f).IsSemisimple

pp: M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
⊢ (t • f).IsSemisimple

Tactic:
· simp [not_not.mp ht]

Goal state after:
M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
⊢ (t • f).IsSemisimple
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inr
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j l : n
⊢ (bQ.repr (W.mkQ (e ((bW.sumQuot bQ) (Sum.inr l))))) j =
    (bQ.repr ((W.mapQ W e he) (Submodule.Quotient.mk ((bW.sumQuot bQ) (Sum.inr l))))) j

Tactic:
W.mapQ_apply

Goal state after:
case inr.inr
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j l : n
⊢ (bQ.repr (W.mkQ (e ((bW.sumQuot bQ) (Sum.inr l))))) j =
    (bQ.repr (Submodule.Quotient.mk (e ((bW.sumQuot bQ) (Sum.inr l))))) j
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
D D1✝ D2✝ : LieDerivation R L M
a b : L
D1 D2 : LieDerivation R L M
h : (fun D ↦ D.toFun) D1 = (fun D ↦ D.toFun) D2
⊢ D1 = D2

Tactic:
cases D1

Goal state after:
case mk
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2✝ : LieDerivation R L M
a b : L
D2 : LieDerivation R L M
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h : (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = D2
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case succ
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 + 1) ∣
    (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

Tactic:
refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)

Goal state after:
case succ.refine_1
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 + 1) ∣
    (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)

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 + 1) ∣
    (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: 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))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu : ((aeval r₁) (derivative P) + u * (r₂ - r₁)) * (r₂ - r₁) = 0
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂

Tactic:
this.mul_right_eq_zero,

Goal state after:
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))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu : r₂ - r₁ = 0
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : 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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this : hasBracketAux x ∘ₗ hasBracketAux y = hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x
⊢ (hasBracketAux x) ((hasBracketAux y) t) = (hasBracketAux ⁅x, y⁆) t + (hasBracketAux y) ((hasBracketAux x) t)

Tactic:
rw [← LinearMap.comp_apply, this]

Goal state after:
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : 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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this : hasBracketAux x ∘ₗ hasBracketAux y = hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x
⊢ (hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x) t =
    (hasBracketAux ⁅x, y⁆) t + (hasBracketAux y) ((hasBracketAux x) t)
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Module ℚ A
B : Type u_2
F : Type u_3
inst✝³ : Ring B
inst✝² : FunLike F A B
inst✝¹ : RingHomClass F A B
inst✝ : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
hk' : f a ^ k = 0
⊢ f (exp a) = exp (f a)

Tactic:
simp [exp_eq_sum hk, exp_eq_sum hk', map_rat_smul]

Goal state after: