mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)).hom ≫
      (w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) =
    (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)).hom

Tactic:
ext; exact StructuredArrow.w φ.left

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ L.whiskerLeft (RF.rightDerivedNatTrans RF' α α' W τ) = τ ≫ α'

Tactic:
by
  dsimp only [rightDerivedNatTrans]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X

Tactic:
by
  dsimp only [rightDerivedNatTrans]
  simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
Y : C
eY : Q.obj L ≅ (singleFunctor C b).obj Y
p q : ℤ
φ₁ φ₂ : (shiftFunctor (DerivedCategory C) p).obj (Q.obj K) ⟶ (shiftFunctor (DerivedCategory C) q).obj (Q.obj L)
h :
  (fun φ ↦
        ((singleFunctors C).shiftIso p (a - p) a ⋯).inv.app X ≫
          (shiftFunctor (DerivedCategory C) p).map eX.inv ≫
            φ ≫ (shiftFunctor (DerivedCategory C) q).map eY.hom ≫ ((singleFunctors C).shiftIso q (b - q) b ⋯).hom.app Y)
      φ₁ =
    (fun φ ↦
        ((singleFunctors C).shiftIso p (a - p) a ⋯).inv.app X ≫
          (shiftFunctor (DerivedCategory C) p).map eX.inv ≫
            φ ≫ (shiftFunctor (DerivedCategory C) q).map eY.hom ≫ ((singleFunctors C).shiftIso q (b - q) b ⋯).hom.app Y)
      φ₂
⊢ φ₁ = φ₂

Tactic:
by simpa [cancel_epi, cancel_mono] using h

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).smallShiftedHomMap
      ((F.mapCochainComplexSingleFunctor 0).app X) ((F.mapCochainComplexSingleFunctor 0).app Y)
      (SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) 0 mk₀._proof_1
        ((CochainComplex.singleFunctor C 0).map f)) =
    SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 mk₀._proof_1
      ((CochainComplex.singleFunctor D 0).map (F.map f))

Tactic:
(F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (.up ℤ)).smallShiftedHomMap_mk₀
    ((F.mapCochainComplexSingleFunctor 0).app X) ((F.mapCochainComplexSingleFunctor 0).app Y)
    (0 : ℤ) rfl

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 ⋯
      (((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
        (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.map
            ((CochainComplex.singleFunctor C 0).map f) ≫
          ((F.mapCochainComplexSingleFunctor 0).app Y).hom) =
    SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 mk₀._proof_1
      ((CochainComplex.singleFunctor D 0).map (F.map f))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
⊢ mapExactFunctor F = ⇑homEquiv₀.symm ∘ F.map ∘ ⇑homEquiv₀

Tactic:
ext x
  rcases (Ext.mk₀_bijective X Y).2 x with ⟨y, hy⟩
  simp [← hy, Ext.mapExactFunctor_mk₀, Ext.homEquiv₀]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ (K.stupidTrunc e).IsStrictlySupported e

Tactic:
by
  dsimp [stupidTrunc]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (({ app := fun P ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } ≫
            { app := fun P ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }).app
        P).f =
    ((𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G)).app P).f

Tactic:
simpa only [hom_ext_iff, G.map_comp, G.map_id] using! G.congr_map P.decomp_p.symm

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
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)

Tactic:
erw [id_comp, comp_id]

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 =
    (F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: case h₁
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
⊢ app' (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) 1 homMk₁._proof_5 =
    app' (β ≫ twoδ₁Toδ₀ f' g' fg' h') 1 homMk₁._proof_5

Tactic:
· dsimp
    rw [hβ₁, Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)

Tactic:
rw [X.cyclesMap_id]; infer_instance

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

Goal state before:
pp: case refine_2
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₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ 𝟙 A ≫ z =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀

Tactic:
· rw [← cancel_mono (X.iCycles f₂ f₃ n₀), id_comp, assoc,
      X.cyclesMap_i _ _ _ _ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) (𝟙 _) n₀ (by cat_disch),
      Functor.map_id, comp_id, liftCycles_i]

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₀ : ℤ
⊢ ∀ (r : ℤ) (pq pq' : ℤ × ℤ),
    (ComplexShape.up' (r, 1 - r)).Rel pq pq' →
      autoParam (2 ≤ r) SpectralSequenceDataCore._auto_16 → WithBotTop.coe (pq.2 - r + 2) = WithBotTop.coe (pq'.2 + 1)

Tactic:
by rintro r pq hr rfl _; simp; lia

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₀ : ℤ
⊢ ∀ (r : ℤ) (pq pq' : ℤ × ℤ),
    (ComplexShape.up' (r, 1 - r)).Rel pq pq' →
      autoParam (2 ≤ r) SpectralSequenceDataCore._auto_20 → WithBotTop.coe pq.2 = WithBotTop.coe (pq'.2 + r - 1)

Tactic:
by rintro r pq hr rfl _; simp; lia

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.f₃₄

Tactic:
have : Epi sq.flip.f₁₃ := by dsimp; infer_instance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
this : Epi sq.flip.f₁₃
⊢ Epi sq.f₃₄
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
⊢ False

Tactic:
let I x := Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)

Goal state after:
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
⊢ False
Module: Mathlib.Algebra.Lie.Subalgebra

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

Tactic:
exact lie_mem _ (subset_lieSpan hm)

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
s : Set L
x : L
hx : x ∈ lieSpan R L s
⊢ ⟨x, hx⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
induction hx using lieSpan_induction with
  | mem u hu => exact subset_lieSpan <| by simpa
  | zero => exact zero_mem _
  | add u v _ _ hu hv => revert hu hv; exact add_mem
  | smul t u _ hu => revert hu; exact LieSubalgebra.smul_mem _ _
  | lie u v _ _ hu hv => revert hu hv; exact LieSubalgebra.lie_mem _

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

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

Tactic:
constructor <;>
    apply mono_lie_right

Goal state after:
case left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ N ≤ N ⊔ N'

case right
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ N' ≤ N ⊔ N'
Module: Mathlib.Algebra.Lie.Submodule

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

Tactic:
exact lie_mem _ (subset_lieSpan hm)

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
s : Set M
⊢ lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0

Tactic:
rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]

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 : LieSubmodule R L M
⊢ N ≤ sSup ((fun x ↦ lieSpan R L {x}) '' ↑N)

Tactic:
simp_rw [← toSubmodule_le_toSubmodule, sSup_toSubmodule, Set.mem_image, SetLike.mem_coe]

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
N : LieSubmodule R L M
⊢ ↑N ≤ sSup {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}
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₂ : LieSubmodule R L M
⊢ comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥

Tactic:
by
  simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule,
    inf_toSubmodule]
  rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]

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
hx : IsIntegral A x
⊢ (minpoly A x).Monic

Tactic:
by
  delta minpoly
  rw [dif_pos hx]
  exact (degree_lt_wf.min_mem _ hx).1

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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤ p.degree

Tactic:
refine le_of_not_gt <| degree_lt_wf.not_lt_min _ ?_

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ p ∈ fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case hp3
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]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * (C p.leadingCoeff⁻¹).leadingCoeff = 1

Tactic:
leadingCoeff_C,

Goal state after:
case hp3
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]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * p.leadingCoeff⁻¹ = 1
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]
hq : q.Monic
hs : ∑ i, q.coeff ↑i • σ.toLinearMap ^ ↑i = 0
H : q.natDegree < orderOf σ
⊢ False

Tactic:
simp_rw [← AlgEquiv.pow_toLinearMap] at hs

Goal state after:
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]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x, q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ False
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ a, pb.gen ∣ b - (algebraMap A B) a

Tactic:
simpa [← Ideal.mem_span_singleton, ← mk_eq_zero, mk_sub, sub_eq_zero] using! pb.exists_smodEq b

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inl
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Subsingleton A
⊢ 0 = (aeval y) 0

Tactic:
aeval_zero

Goal state after:
case inl
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Subsingleton A
⊢ 0 = 0
Module: Mathlib.Algebra.Squarefree.Basic

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

Tactic:
by
  rw [Squarefree, not_forall]
  exact ⟨0, by simp⟩

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n

Tactic:
rw [iterateFrobeniusEquiv_eq_pow]; exact (inv_pow _ _).symm

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ count (s ^ p ^ n) (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤
    p ^ n * rootMultiplicity (s ^ p ^ n) f

Tactic:
← rootMultiplicity_expand_pow,

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ count (s ^ p ^ n) (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤
    rootMultiplicity s ((expand R (p ^ n)) f)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
h : IsUnit g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
rw [isUnit_iff] at h

Goal state after:
case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
h : ∃ r, IsUnit r ∧ C r = g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u_1
L : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring L
inst✝ : Algebra F L
S : Subalgebra F L
⊢ Algebra.IsSeparable F ↥S ↔ ∀ x ∈ S, IsSeparable F x

Tactic:
by
  simp_rw [Algebra.isSeparable_def, Subtype.forall,
    ← isSeparable_map_iff S.val Subtype.val_injective, coe_val]

Goal state after:
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 : f ∣ C p
⊢ p = 0

Tactic:
by_cases h : f = 0

Goal state after:
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

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.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw : LinearMap.mulRight K a = (Algebra.lsmul K K (Module.End K V)) (MulOpposite.op a)
⊢ (Polynomial.aeval (LinearMap.mulRight K a)) (minpoly K a) = 0

Tactic:
rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_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 * ((LinearMap.toMatrix b' b) ↑(b'.equiv b (Equiv.refl ι))).det

Tactic:
LinearMap.toMatrix_basis_equiv,

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 * Matrix.det 1