mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
⊢ (if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
by_cases h₀ : k₀ = i₀

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : k₀ = i₀
⊢ (if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
⊢ (if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (projectiveResolutions C).map f ≫ Q.iso.hom = P.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ

Tactic:
rw [← cancel_epi (P.iso).inv, iso_inv_naturality_assoc f P Q φ comm,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case inst
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')

pp: case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂

Tactic:
· obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fg J'.2 (isNoetherian_def.mp hR _)
      exact ⟨CostructuredArrow.mk (⟨⟨⟨hk⟩⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩

Goal state after:
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂
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 F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
by
  rw [← cancel_mono (P.isoLeftDerivedToHomotopyCategoryObj G).hom, assoc, assoc,
      Iso.inv_hom_id, comp_id]
  dsimp [isoLeftDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
    NatTrans.leftDerivedToHomotopyCategory]
  rw [assoc]
  erw [id_comp, comp_id]
  obtain ⟨β, hβ⟩ := (HomotopyCategory.quotient _ _).map_surjective (iso P).hom
  rw [← hβ]
  dsimp
  simp only [← Functor.map_comp, NatTrans.mapHomologicalComplex_naturality]
  rfl

Goal state after:
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
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map 0 = 0

Tactic:
F.map_zero

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
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ 0 = 0
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 Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
⊢ ∀ (j_1 : ↑(p ⁻¹' {j})),
    Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) j_1 ≫
        e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
      s.inj j_1

Tactic:
by
      rintro ⟨⟨i, j'⟩, h⟩
      by_cases hi : i = 0
      · subst hi
        simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h
        subst h
        simp
      · apply IsInitial.hom_ext
        exact mapBifunctorObjSingle₀ObjIsInitial _ _ _ _ hi

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 : 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 Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫
      e.inv.app (Y' j) ≫
        (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ =
    e.inv.app (Y j) ≫
      (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫
        (𝟙 (F.obj ((single₀ I).obj X 0))).app (Y j) ≫
          (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯

Tactic:
NatTrans.id_app,

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 : 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 Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫
      e.inv.app (Y' j) ≫
        (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ =
    e.inv.app (Y j) ≫
      (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫
        𝟙 ((F.obj ((single₀ I).obj X 0)).obj (Y j)) ≫
          (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃

Tactic:
rw [h.comm₃]

Goal state after:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

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₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃

Tactic:
simp only [d, δ_toCycles_assoc, toCycles_πE_descE]

Goal state after:
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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (X.H n).map (twoδ₂Toδ₁ f g fg h) ≫ X.toCycles f g fg h n = 0

Tactic:
simp [← cancel_mono (X.iCycles f g n)]

Goal state after:
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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (Cofork.ofπ (cokernel.π (X.cokernelSequenceCycles f g fg h n).f) ⋯).π ≫ (X.cokernelIsoCycles f g fg h n).hom =
    Cofork.π (CokernelCofork.ofπ (X.cokernelSequenceCycles f g fg h n).g ⋯)

Tactic:
simp [← cancel_mono (X.iCycles f g n)]

Goal state after:
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 : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
n : ℕ
⊢ Submodule.map (f ^ n) f.range < Submodule.map (f ^ n) ⊤

Tactic:
refine Submodule.map_strictMono_of_injective (Module.End.iterate_injective s n) (Ne.lt_top ?_)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
n : ℕ
⊢ f.range ≠ ⊤
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:
by
  rw [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]

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₂
y : L₂
hy : y ∈ (Submodule.map (↑f) K.toSubmodule).toAddSubsemigroup
x' : L
hx' : x' ∈ ↑K.toSubmodule
⊢ ⁅↑f x', y⁆ ∈ (Submodule.map (↑f) K.toSubmodule).carrier

Tactic:
rcases hy with ⟨y', hy', rfl⟩

Goal state after:
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₂
x' : L
hx' : x' ∈ ↑K.toSubmodule
y' : L
hy' : y' ∈ ↑K.toSubmodule
⊢ ⁅↑f x', ↑f y'⁆ ∈ (Submodule.map (↑f) K.toSubmodule).carrier
Module: Mathlib.Algebra.Lie.Ideal

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I : LieIdeal R L
x y : L
a✝ : x ∈ (↑I).carrier
hy : y ∈ (↑I).carrier
⊢ y ∈ I

Tactic:
exact 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'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
by
  rw [f.idealRange_eq_map]
  exact LieIdeal.map_mono le_top

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 N' : LieSubmodule R L M
⊢ ∀ {x : L} {m : M}, m ∈ (↑N ⊔ ↑N').carrier → ⁅x, m⁆ ∈ (↑N ⊔ ↑N').carrier

Tactic:
by
        rintro x m (hm : m ∈ (N : Submodule R M) ⊔ (N' : Submodule R M))
        change ⁅x, m⁆ ∈ (N : Submodule R M) ⊔ (N' : Submodule R M)
        rw [Submodule.mem_sup] at hm ⊢
        obtain ⟨y, hy, z, hz, rfl⟩ := hm
        exact ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩

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
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ↑(⨆ i, N i) = ↑⊤ ↔ ⨆ i, N i = ⊤

Tactic:
toSubmodule_inj

Goal state after:
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 = ⊤
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ e.range = ⊤

Tactic:
by
  rw [LieModuleHom.range_eq_top]
  exact e.surjective

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x).leadingCoeff = p.leadingCoeff

Tactic:
rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]

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

Goal state before:
pp: case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
this : r.natDegree ≤ 0
⊢ p = p * 1

Tactic:
mul_one

Goal state after:
case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
this : r.natDegree ≤ 0
⊢ p = p
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✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : (minpoly A x).degree ≤ 0
⊢ eval₂ (algebraMap A B) x 1 = 0

Tactic:
by simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.map (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
Submodule.map_span

Goal state after:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
hx : (Polynomial.aeval x) p = 0
⊢ p = p * 1

Tactic:
mul_one

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
hx : (Polynomial.aeval x) p = 0
⊢ p = p
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ↑((minpoly A x).natDegree * 1) ≤ ↑q.natDegree

Tactic:
mul_one

Goal state after:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ ↑(q.natDegree * 1)
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree

Tactic:
mul_one

Goal state after:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ ↑q.natDegree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
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 σ
⊢ ∀ (q : K[X]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree

Tactic:
· intro q hq hs
    rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]
    intro H
    rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs
    simp_rw [← AlgEquiv.pow_toLinearMap] at hs
    apply hq.ne_zero
    simpa using Fintype.linearIndependent_iff.mp
      (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_toAlgHom_injective).comp _
        (Subtype.val_injective.comp ((finEquivPowers hσ).injective)))
      (q.coeff ∘ (↑)) hs ⟨_, H⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C p * C (X - C a) + q * (X - C b) = P

Tactic:
rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1) * 1) = 1

Tactic:
mul_one

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1)) = 1
Module: Mathlib.FieldTheory.Perfect

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

Tactic:
toFinset_subset

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ⊆ p ^ n • f.roots
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Free R S
x : R
⊢ x ^ finrank R S * 1 = x ^ finrank R S

Tactic:
mul_one

Goal state after:
R : Type u_5
S : Type u_6
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Free R S
x : R
⊢ x ^ finrank R S = x ^ finrank R S
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:
by
  cases subsingleton_or_nontrivial F
  · have := Module.subsingleton F K
    exact ⟨1, monic_one, Subsingleton.elim _ _⟩
  · exact of_not_not (h.ne_zero <| minpoly.eq_zero ·)

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : f = 0
⊢ p = 0

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : ¬f = 0
⊢ p = 0

Tactic:
· exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp))

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : ¬f = 0
⊢ p = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ C p ≠ 0

Tactic:
rwa [Ne, C_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det = ((LinearMap.toMatrix b b') f).det * 1

Tactic:
mul_one

Goal state after:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det = ((LinearMap.toMatrix b b') f).det
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]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ ∑ b, ((monomial ↑b) (x b)).coeff ↑i = x i

Tactic:
simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

Goal state after: