mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ ((quotUliftToQuot F).comp (quotToQuotUlift F)) ((Quot.ι F j) a) = (AddMonoidHom.id (Quot F)) ((Quot.ι F j) a)

Tactic:
rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ (ι R) x = (algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
    have : IsCentralScalar R M := ⟨fun r m => rfl⟩
    have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
    rw [h, AlgHom.commutes] at hf0
    have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
    exact this.symm.imp_left Eq.symm
  · rintro ⟨rfl, rfl⟩
    rw [map_zero, map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁

Tactic:
rw [Equiv.symm_apply_eq]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ 𝟙 R₁ = (conjugateEquiv adj₁ adj₁) (𝟙 L₁)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map
          ((fun x_1 ↦ x.fst •> x_1) ∘ fun x ↦
            (List.take x.2 (List.map fst xs)).prod •> (x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod))
          xs.zipIdx).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •>
              (List.take x_1.2 (List.map fst xs)).prod •> (x_1.1.snd <• (List.drop (x_1.2 + 1) (List.map fst xs)).prod))
          xs.zipIdx).sum

Tactic:
exact add_comm _ _

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1

Tactic:
have := sum_tmul_counit_eq repr

Goal state after:
R : Type u
A : Type v
ι : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a ι
this : ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃) (α ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) =
    (mateEquiv adj₁ adj₂) α ≫ᵥ (mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((conjugateEquiv adj₂ adj₃) β)).natTrans.app b

Tactic:
unfold vComp hComp at vcomp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
            (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)) =
    TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
      ((R₁.associator G (𝟭 C)).inv ≫
        whiskerRight ((mateEquiv adj₁ adj₂) α).natTrans (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).hom ≫
            H.whiskerLeft ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)).natTrans ≫
              (H.associator (𝟭 D) R₃).inv)
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((conjugateEquiv adj₂ adj₃) β)).natTrans.app b
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃) ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ β) =
    (mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ᵥ (mateEquiv adj₂ adj₃) β
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Tactic:
unfold vComp hComp at vcomp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          (𝟭 A).whiskerLeft β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).hom ≫
            (𝟭 B).whiskerLeft ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).inv)
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
⊢ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr) = ⊤

Tactic:
by
  refine top_unique fun x hx => ?_; clear hx
  rw [← x.inl_fst_add_inr_snd_eq]
  refine add_mem ?_ ?_
  · exact le_sup_left (α := Subalgebra S _) <| Set.mem_range_self x.fst
  · exact le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y : ModuleCat S
y1 y2 : ↑Y
s : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
          { toFun := fun s ↦ s • (y1 + y2), map_add' := ⋯, map_smul' := ⋯ }))
      s =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y1, map_add' := ⋯, map_smul' := ⋯ } +
          (CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y2, map_add' := ⋯, map_smul' := ⋯ }))
      s

Tactic:
by
        simp [smul_add]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
      Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄) =
    (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
      (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv

Tactic:
ext M m

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ (extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
      Functor.whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂) ≫ (extendScalars f₁₂).leftUnitor.hom =
    𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))

Tactic:
ext M m

Goal state after:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
              Functor.whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂) ≫
                (extendScalars f₁₂).leftUnitor.hom).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom ((𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))).app M)) (1 ⊗ₜ[R₁] m)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ (extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫
      (extendScalars f₁₂).whiskerLeft (extendScalarsId R₂).hom ≫ (extendScalars f₁₂).rightUnitor.hom =
    𝟙 (extendScalars ((RingHom.id R₂).comp f₁₂))

Tactic:
ext M m

Goal state after:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫
              (extendScalars f₁₂).whiskerLeft (extendScalarsId R₂).hom ≫ (extendScalars f₁₂).rightUnitor.hom).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom ((𝟙 (extendScalars ((RingHom.id R₂).comp f₁₂))).app M)) (1 ⊗ₜ[R₁] m)
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
⊢ ↑(TensorProduct.comm S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ comul = comul

Tactic:
by
    ext x y
    dsimp
    conv_rhs => rw [← comm_comul _ x, ← comm_comul _ y]
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
h : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → z ∈ I
x : R
hx : x ∈ s
⊢ x ∈ ↑I

Tactic:
simpa only [I, SetLike.mem_coe, mem_mk'] using subset_closure hx

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ jacobson R (M ⧸ jacobson R M) = ⊥

Tactic:
by
  rw [jacobson_quotient_of_le le_rfl, mkQ_map_self]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ x ∈ I.toTwoSided ↔ x ∈ I

Tactic:
by
  simp [toTwoSided]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ↑I.toTwoSided = ↑I

Tactic:
by
  simp [toTwoSided]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • N.subtype.range

Tactic:
range_subtype

Goal state after:
case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • N
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = N.subtype.range

Tactic:
range_subtype

Goal state after:
case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = N
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
b x : R
hx : f x = 0
⊢ ∃ n, (a * b) ^ n * x = 0

Tactic:
obtain ⟨n, hn⟩ := H x hx

Goal state after:
S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
b x : R
hx : f x = 0
n : ℕ
hn : a ^ n * x = 0
⊢ ∃ n, (a * b) ^ n * x = 0
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
⊢ 1 ∈ J

Tactic:
have : 1 - s * b ∈ 𝔪₀ := by
        rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr
        rw [sbyr, ← mul_assoc] at y𝔪
        simp [𝔪₀, sub_mul, y𝔪]

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this : 1 - s * b ∈ 𝔪₀
⊢ 1 ∈ J
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : (comap (Quotient.mk I) ⊥).jacobson = comap (Quotient.mk I) ⊥
⊢ I.jacobson = I

Tactic:
← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : (RingHom.ker (Quotient.mk I)).jacobson = RingHom.ker (Quotient.mk I)
⊢ I.jacobson = I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : (comap (Quotient.mk I) ⊥).radical = (comap (Quotient.mk I) ⊥).jacobson
⊢ I.radical = I.jacobson

Tactic:
← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : (RingHom.ker (Quotient.mk I)).radical = (RingHom.ker (Quotient.mk I)).jacobson
⊢ I.radical = I.jacobson
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g

Tactic:
have := hI.isIso_to f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
· cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
· cases h_1
        apply (H _ h).hom_ext

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ 𝟙 (𝟙_ C) ≫ f.hom = η

Tactic:
← trivial_mon_one,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ η ≫ f.hom = η
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit (F.mapCone (limitConeOfTerminalAndPullbacks K).cone)

Tactic:
apply
          isBinaryProductOfIsTerminalIsPullback _ _ (isLimitOfHasTerminalOfPreservesLimit F)

Goal state after:
case hc
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit
    (PullbackCone.mk ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.left })
      ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.right }) ⋯)

case f
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.left } ⟶ F.obj (⊤_ C)

case g
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.right } ⟶ F.obj (⊤_ C)