mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D₁
inst✝⁵ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
X₁ : C₁
e : L.functor.obj X₁ ≅ ρ.X₁
⊢ W₂ (R.functor.preimage (iso.hom.app X₁ ≫ B.functor.map e.hom ≫ ρ.w))

Tactic:
simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]
      refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
      exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso e) (Iso.refl _)

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
⊢ ∃ L i, ∃ (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n

Tactic:
have : L.IsGE n := by
    have hK : K.IsGE n := inferInstance
    rw [← DerivedCategory.isGE_Q_obj_iff] at hK ⊢
    exact DerivedCategory.TStructure.t.isGE_of_iso (asIso (DerivedCategory.Q.map i)) n

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this✝ : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
this : L.IsGE n
⊢ ∃ L i, ∃ (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
X : C₁
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor.obj X)

Tactic:
let e : W₂.Q.obj _ ≅ (Φ.localizedFunctor W₁.Q W₂.Q).obj _ := ((Φ.catCommSq W₁.Q W₂.Q).iso).app X

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
X : C₁
e : W₂.Q.obj (Φ.functor.obj X) ≅ (Φ.localizedFunctor W₁.Q W₂.Q).obj (W₁.Q.obj X) :=
  (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).app X
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor.obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
this : K.obj.IsGE n
L : CochainComplex C ℤ
w✝¹ : L.IsStrictlyGE n
e : K.obj ≅ DerivedCategory.Q.obj L
M : CochainComplex.Plus (InjectiveObject C)
w✝ : M.obj.IsStrictlyGE n
i : { obj := L, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj M
hi : CochainComplex.Plus.quasiIso C i
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)

Tactic:
have : QuasiIso i.hom := by assumption

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
this✝ : K.obj.IsGE n
L : CochainComplex C ℤ
w✝¹ : L.IsStrictlyGE n
e : K.obj ≅ DerivedCategory.Q.obj L
M : CochainComplex.Plus (InjectiveObject C)
w✝ : M.obj.IsStrictlyGE n
i : { obj := L, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj M
hi : CochainComplex.Plus.quasiIso C i
this : QuasiIso i.hom
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((shiftFunctor C 0).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
    ((shiftFunctorZero C S).app X.obj).hom ≫ ((𝟭 (DifferentialObject S C)).obj X).d

Tactic:
← NatTrans.naturality

Goal state after:
case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((shiftFunctor C 0).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
    (CategoryTheory.shiftFunctor C 0).map ((𝟭 (DifferentialObject S C)).obj X).2 ≫
      (shiftFunctorZero C S).hom.app ((CategoryTheory.shiftFunctor C 1).obj ((𝟭 (DifferentialObject S C)).obj X).1)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain ((singleFunctor C p).obj X) K n
p' q' : ℤ
hpq' : p' + n = q'
hp : p' = p
⊢ ((fun f ↦ fromSingleMk f h)
          ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain ((singleFunctor C p).obj X) K n
p' q' : ℤ
hpq' : p' + n = q'
hp : ¬p' = p
⊢ ((fun f ↦ fromSingleMk f h)
          ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

Tactic:
· aesop

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain ((singleFunctor C p).obj X) K n
p' q' : ℤ
hpq' : p' + n = q'
hp : ¬p' = p
⊢ ((fun f ↦ fromSingleMk f h)
          ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α)).v
      p' q' hpq' =
    α.v p' q' hpq'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K ((singleFunctor C q).obj X) n
p' q' : ℤ
hpq' : p' + n = q'
hq : q' = q
⊢ ((fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K ((singleFunctor C q).obj X) n
p' q' : ℤ
hpq' : p' + n = q'
hq : ¬q' = q
⊢ ((fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

Tactic:
· aesop

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K ((singleFunctor C q).obj X) n
p' q' : ℤ
hpq' : p' + n = q'
hq : ¬q' = q
⊢ ((fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α)).v
      p' q' hpq' =
    α.v p' q' hpq'
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
inst✝ : IsIdempotentComplete D
⊢ (functorExtension₂ C D).IsEquivalence

Tactic:
rw [← karoubiUniversal₂_functor_eq]

Goal state after:
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
inst✝ : IsIdempotentComplete D
⊢ (karoubiUniversal₂ C D).functor.IsEquivalence
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Abelian 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
F : C ⥤ D
inst✝ : F.Additive
⊢ HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0 ≫ Q.fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F ≫ F.map f

Tactic:
simp only [← cancel_epi (HomologicalComplex.pOpcycles _ _), ← F.map_comp, comm,
    HomologicalComplex.p_opcyclesMap_assoc, Functor.mapHomologicalComplex_map_f,
    pOpcycles_comp_fromLeftDerivedZero', pOpcycles_comp_fromLeftDerivedZero'_assoc]

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

Tactic:
dsimp [mapBifunctorRightUnitor]
  erw [CofanMapObjFun.ιMapObj_iso_inv]
  rw [mapBifunctorRightUnitorCofan_inj]

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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
by
  have : IsIso (shortComplexMap X f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂) := by
    apply +allowSynthFailures ShortComplex.isIso_of_isIso <;> assumption
  dsimp [map]
  infer_instance

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

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ = -⁅x, m⁆

Tactic:
← sub_eq_zero,

Goal state after:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ - -⁅x, m⁆ = 0
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m⁆ = -⁅x, m⁆

Tactic:
← sub_eq_zero,

Goal state after:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m⁆ - -⁅x, m⁆ = 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).right.homologyIso =
    (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso

Tactic:
by
  ext1
  simp [ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso]

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

Tactic:
have : Jac ^ n * N = N := n.rec (by rw [Jac.pow_zero, N.one_mul])
      fun n hn ↦ by rwa [Jac.pow_succ, mul_assoc, eq]

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
⊢ False
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: 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)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ I x = N

Tactic:
refine ((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)

Goal state after:
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)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ Jac * I x = I x
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆

Tactic:
← sub_eq_zero,

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) - (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) = 0
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
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
rw [← SetLike.mem_coe, lieSpan, coe_sInf]
  exact Set.mem_iInter₂

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
⊢ map f (I ⊔ f.ker) = map f I

Tactic:
refine le_antisymm ?_ (LieIdeal.map_mono le_sup_left)

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f (I ⊔ f.ker) ≤ map f I
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mpr
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 ≠ ⊥ → Nontrivial ↥N

Tactic:
contrapose!

Goal state after:
case mpr
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
⊢ Subsingleton ↥N → N = ⊥
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
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
hdir

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
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ ∀ (y : L) (x : ↥I) (x_1 : ↥I), ⁅↑x, ↑x_1⁆ = y → y = 0

Tactic:
refine
    ⟨fun h z x y hz =>
      hz.symm.trans
        (((I : LieSubalgebra R L).coe_bracket x y).symm.trans
          ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
      fun h => ⟨fun x y => ((I : LieSubalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩

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 : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m

Tactic:
use ⁅((⟨x₁, hx₁⟩ : I) : L), (n : N)⁆

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆ ∧ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m
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
⊢ minpoly A x = 1

Tactic:
by
  nontriviality A
  have := minpoly.min A x monic_one (Subsingleton.elim _ _)
  rw [degree_one] at this
  rcases le_or_gt (minpoly A x).degree 0 with h | h
  · rwa [(monic ⟨1, monic_one, by simp [eq_iff_true_of_subsingleton]⟩ :
           (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h
  · exact (this.not_gt h).elim

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
S : Type u_2
inst✝³ : Ring S
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module S M
U : Submodule R M
V : Submodule S M
h : U.toAddSubgroup ≤ V.toAddSubgroup
x y : M
hxy : x ≡ y [SMOD U]
⊢ x ≡ y [SMOD V]

Tactic:
by
  simp only [SModEq, Submodule.Quotient.eq] at hxy ⊢
  exact h hxy

Goal state after:
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
h✝ : Subsingleton B
⊢ Submodule.Quotient.mk b = Submodule.Quotient.mk ((algebraMap A B) 0)

Tactic:
Subsingleton.eq_zero b,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Subsingleton B
⊢ Submodule.Quotient.mk 0 = Submodule.Quotient.mk ((algebraMap A B) 0)
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)) (C a) = 0

Tactic:
Quotient.eq_zero_iff_mem

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ C a ∈ map C I
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
⊢ (norm R) x = 1

Tactic:
refine norm_eq_one_of_not_exists_basis _ (mt ?_ h) _
  rintro ⟨s, ⟨b⟩⟩
  exact Module.Finite.of_basis b

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n = (of (X ^ n - C a)) a

Tactic:
← sub_eq_zero,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n - (of (X ^ n - C a)) a = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case cons.refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
i : ι
hi : i ∈ s
⊢ IsRelPrime (f a) (f i)

Tactic:
exact (hs.right i (by simp [hi]) fun h ↦ ha (h ▸ hi)).left

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
hf : f.Separable
hfg : g ∣ f
⊢ g.Separable

Tactic:
rcases hfg with ⟨f', rfl⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
g f' : R[X]
hf : (g * f').Separable
⊢ g.Separable
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible ((expand R p) f)

Tactic:
rw [polynomial_expand_eq]
  exact not_irreducible_pow (Fact.out : p.Prime).ne_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
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
⊢ LinearMap.det (prodMap f f') = LinearMap.det f * LinearMap.det f'

Tactic:
← det_toMatrix (b.prod b'),

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
⊢ ((toMatrix (b.prod b') (b.prod b')) (prodMap f f')).det = LinearMap.det f * LinearMap.det f'