mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (NatTrans.leftDerivedToHomotopyCategory α).app X ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)

Tactic:
dsimp [isoLeftDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
    NatTrans.leftDerivedToHomotopyCategory]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) =
    ((F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex))) ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
j : J
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)

Tactic:
by
  simp [mapBifunctorLeftUnitorCofan]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
⊢ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) =
    (mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ ≫ (mapBifunctorRightUnitor F Y e p hp X').inv

Tactic:
mapBifunctorRightUnitor_inv_naturality,

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
⊢ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) =
    (mapBifunctorRightUnitor F Y e p hp X).hom ≫
      (mapBifunctorRightUnitor F Y e p hp X).inv ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y))
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ X.toCycles f g fg h n ≫ X.cyclesMap f g f' g' α n = (X.H n).map β ≫ X.toCycles f' g' fg' h' n

Tactic:
rw [← cancel_mono (X.iCycles f' g' n), Category.assoc, Category.assoc, toCycles_i,
    X.cyclesMap_i f g f' g' α (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n rfl,
    toCycles_i_assoc, ← Functor.map_comp, ← Functor.map_comp]
  congr 1
  ext
  · dsimp
    rw [hβ₀]
    exact naturality' α 0 1
  · dsimp
    rw [hβ₁, Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A x₂ hx₂
  dsimp at x₂ hx₂
  obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    (X.kernelSequenceOpcyclesE_exact f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).exact_up_to_refinements
      (X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ (by simpa using hx₂ =≫ biprod.fst)) (by
        dsimp
        rw [← X.fromOpcyles_δ f₁ f₂ f₃ f₂₃ h₂₃ n₁ n₂,
          X.liftOpcycles_fromOpcycles_assoc]
        simpa using hx₂ =≫ biprod.snd)
  dsimp at x₁ hx₁
  refine ⟨A₁, π₁, inferInstance, x₁, ?_⟩
  dsimp
  rw [← reassoc_of% hx₁, liftOpcycles_fromOpcycles]

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

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
⊢ IsZero ((X.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
exact HasSpectralSequence.isZero_H_obj_mk₁_i₀_le r r' pq hpq n hn

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ ((X.homologyDataIdId f (n₀ - 1) n₀ n₁ ⋯ ⋯).left.cyclesIso.inv ≫
        (X.cyclesIso (𝟙 i₀) f (𝟙 i₁) (n₀ - 1) n₀ n₁ ⋯ hn₁).hom) ≫
      X.iCycles (𝟙 i₀) f n₀ =
    (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)

Tactic:
simp only [Category.assoc, cyclesIso_hom_i, homologyDataIdId_left_i,
    ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles, ← Functor.map_id]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (𝟙 (mk₁ f)) = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ (r ^ n • LinearMap.id).range ↔ x ∈ (r ^ m • LinearMap.id).range
⊢ ∃ y, r ^ n.succ • y = r ^ n • x

Tactic:
by simpa using hn n.succ n.le_succ (r ^ n • x)

Goal state after:
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₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Subsingleton (LieSubalgebra R ↥⊥)

Tactic:
by
  apply subsingleton_of_bot_eq_top
  ext ⟨x, hx⟩; change x ∈ ⊥ at hx; rw [LieSubalgebra.mem_bot] at hx; subst hx
  simp only [mem_bot, mem_top, iff_true]
  rfl

Goal state after:
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✝ N' N O : LieSubmodule R L M
h : (fun s ↦ (↑s).carrier) N = (fun s ↦ (↑s).carrier) O
⊢ N = O

Tactic:
cases N

Goal state after:
case mk
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' O : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = (fun s ↦ (↑s).carrier) O
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = O
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ (p %ₘ minpoly A x).degree < (minpoly A x).degree

Tactic:
exact degree_modByMonic_lt _ (monic hx)

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
z₁ : L'
h₁ : z₁ ∈ map f I₁
z₂ : L'
h₂ : z₂ ∈ map f I₂
⊢ ⁅↑⟨z₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L'
h₂ : z₂ ∈ map f I₂
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
⊢ ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : ⊥ < ↑d
⊢ 0 < d

Tactic:
first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d

Tactic:
first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

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
⊢ pb.minpolyGen.Monic

Tactic:
nontriviality A
  apply (monic_X_pow _).sub_of_left _
  rw [degree_X_pow]
  exact degree_sum_fin_lt _

Goal state after:
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
S' : Type u_7
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ ↑e (pb.basis i) = e pb.gen ^ ↑i

Tactic:
pb.basis_eq_pow,

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
S' : Type u_7
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ ↑e (pb.gen ^ ↑i) = e pb.gen ^ ↑i
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
this✝ : CharZero F
this : f.natDegree = 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f

Tactic:
have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'

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
this✝ : f.natDegree = 0
this : f.natDegree ≠ 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
⊢ PerfectField K

Tactic:
obtain hp | ⟨hp⟩ := ‹ExpChar K p›

Goal state after:
case zero
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : ExpChar K 1
inst✝ : PerfectRing K 1
⊢ PerfectField K

case prime
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ PerfectField K
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
⊢ IsIntegral F x

Tactic:
cases subsingleton_or_nontrivial F

Goal state after:
case inl
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Subsingleton F
⊢ IsIntegral F x

case inr
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Nontrivial F
⊢ IsIntegral F x
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
μ : R
⊢ (f - (algebraMap R (End R M)) μ).IsSemisimple ↔ f.IsSemisimple

Tactic:
suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp [mem_invtSubmodule, isSemisimple_iff, this]

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
μ : R
⊢ ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p)))))
      (1 ⊗ₜ[R] root p) (Polynomial.map (↑includeRight) p) =
    0

Tactic:
Polynomial.eval₂_map

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂
      ((↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))).comp
        ↑includeRight)
      (1 ⊗ₜ[R] root p) p =
    0
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
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
⊢ Ideal.map (of (minpoly R pb.gen)) I =
    Ideal.map (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv) (Ideal.map (algebraMap R S) I)

Tactic:
by rw [Ideal.map_map,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]

Goal state after:
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, IsNilpotent (-(r - x)) ∧ (aeval r) P = 0

Tactic:
isNilpotent_neg_iff

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, IsNilpotent (r - x) ∧ (aeval r) P = 0
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
⊢ (exp D) (x * y) = (exp D) x * (exp D) y

Tactic:
let DR : Module.End R (B ⊗[R] B) := D.rTensor B

Goal state after:
R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
⊢ (exp D) (x * y) = (exp D) x * (exp D) y
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
x : L
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Tactic:
Subtype.forall'

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
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, 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
inst✝ : IsSolvable L
h : IsSolvable ↥⊤
⊢ ⊤ ≤ radical R L

Tactic:
exact le_sSup h

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 : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k

Tactic:
apply le_antisymm (map_lowerCentralSeries_le k f)

Goal state after:
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 : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
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
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
m : M
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)

Tactic:
exact iterate_toEnd_mem_lowerCentralSeries₂ R L M x y m k

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
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]
    simp

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent (↥⊤) M

Tactic:
apply this M

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := ⋯
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := ⋯
hs : s.Nonempty
this : ⊤ ∈ s
⊢ ∀ (x : ↥⊤), IsNilpotent ((toEnd R (↥⊤) M) x)
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, (g • l x * (toFun G F) x g' - l x • (toFun G F) x g') = 0 g'

Tactic:
rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, g • l x * (toFun G F) x g' = ∑ x ∈ s, l x • (toFun G F) x g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ minpoly G F x ∣ f

Tactic:
by
  classical
  rw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly,
    ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ _, prodXSubSMul]
  refine
    Fintype.prod_dvd_of_coprime
      (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x) fun y =>
      QuotientGroup.induction_on y fun g => ?_
  rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.def, MulAction.ofQuotientStabilizer_mk,
    Polynomial.eval_smul',
    ← IsInvariantSubring.coe_subtypeHom' G (FixedPoints.subfield G F).toSubring,
    ← MulSemiringActionHom.coe_polynomial, ← map_smul, smul_polynomial,
    MulSemiringActionHom.coe_polynomial, IsInvariantSubring.coe_subtypeHom',
    Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K = adjoin F S

Tactic:
apply toSubalgebra_injective
  rw [h]
  refine (adjoin_eq_algebra_adjoin F _ fun x ↦ ?_).symm
  rw [← h]
  exact K.inv_mem

Goal state after: