mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod' G) ≫ ε (F.prod' G)).1 = (𝟙 ((F.prod' G).obj (𝟙_ C))).1

pp: case h₂
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod' G) ≫ ε (F.prod' G)).2 = (𝟙 ((F.prod' G).obj (𝟙_ C))).2

Tactic:
· simp only [CategoryTheory.prod_comp_fst, prod'_ε_fst, prod'_η_fst, η_ε,
        prod_id, prod'_obj]

Goal state after:
case h₂
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod' G) ≫ ε (F.prod' G)).2 = (𝟙 ((F.prod' G).obj (𝟙_ C))).2
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ F.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              adj.counit.app X ▷ F.obj (G.obj (Y ⊗ Z)) ≫ X ◁ adj.counit.app (Y ⊗ Z)

Tactic:
← whisker_exchange,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ F.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              F.obj (G.obj X) ◁ adj.counit.app (Y ⊗ Z) ≫ adj.counit.app X ▷ (Y ⊗ Z)
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ MorphismProperty.bijective C (𝟙 X)

Tactic:
by
    delta MorphismProperty.bijective
    convert! bijective_id
    aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj X✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ μ G (F.obj x✝¹) (F.obj X✝)) ≫
      F.obj x✝¹ ◁ F.map x✝ =
    F.map (x✝¹ ◁ x✝) ≫
      (adj.homEquiv (x✝¹ ⊗ Y✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm, assoc, ← μ_natural_right]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ G.obj (F.obj x✝¹) ◁ G.map (F.map x✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝)) =
    (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      (x✝¹ ◁ x✝ ≫ (adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))
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
hx : (ι R) x = (Algebra.linearMap R (TensorAlgebra R M)) r
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0

Tactic:
Algebra.linearMap_apply,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : (ι R) x = (algebraMap R (TensorAlgebra R M)) r
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
⊢ (forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint

Tactic:
← Functor.isRightAdjoint_comp_iff_right e.inverse,

Goal state after:
R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
⊢ (e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ (counitAlgHom R A).comp (Algebra.ofId R A) = counitAlgHom R R

Tactic:
by ext

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ (Algebra.TensorProduct.map (Algebra.ofId R A) (Algebra.ofId R A)).comp (comulAlgHom R R) =
    (comulAlgHom R A).comp (Algebra.ofId R A)

Tactic:
by ext

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 Y' : ModuleCat S
g : Y ⟶ Y'
y : ↑Y
s : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y')) ((Hom.hom ((𝟭 (ModuleCat S)).map g ≫ ↟(app' f Y'))) y)) s =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y'))
        ((Hom.hom (↟(app' f Y) ≫ (restrictScalars f ⋙ coextendScalars f).map g)) y))
      s

Tactic:
by
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): previously simp [CoextendScalars.map_apply]
      simp only [Functor.id_map, Functor.id_obj, Functor.comp_map]
      change s • (g y) = g (s • y)
      rw [map_smul]

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

Goal state before:
pp: case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑X
⊢ (Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g)) (x✝ ⊗ₜ[R] y✝) =
    (Hom.hom ((ExtendRestrictScalarsAdj.counit f).app Y)) (x✝ ⊗ₜ[R] (ConcreteCategory.hom g) y✝)

Tactic:
ExtendRestrictScalarsAdj.Counit.map_hom_apply,

Goal state after:
case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑X
⊢ (Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g)) (x✝ ⊗ₜ[R] y✝) =
    (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (x✝ ⊗ₜ[R] (ConcreteCategory.hom g) y✝)
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
by rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a \ b) = f' a \ f' b

Tactic:
by simpa only [h] using map_sdiff f

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a \ b) = f' a \ f' b

Tactic:
by simpa only [h] using map_sdiff f

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
⊢ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f

Tactic:
by
  rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq]

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
by
  rw [ofComonObjCoalgebraStruct_comul]
  simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
by
  rw [ofComonObjCoalgebraStruct_comul]
  simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ Associated ((algebraMap R S) (sec x s).1) s

Tactic:
rw [← IsLocalization.Away.sec_spec, map_pow]
  exact associated_mul_unit_left _ _ <| .pow _ <| IsLocalization.Away.algebraMap_isUnit _

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
refine ⟨fun H x hx ↦ H x 0 (by simpa), fun H a n ha ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
a : R
n : ℕ
ha : f r ^ n * f a = 0
⊢ ∃ m, r ^ m * a = 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ (span s).ringCon ≤ I.ringCon ↔ s ⊆ ↑I

Tactic:
RingCon.gi _ |>.gc

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ (fun a b ↦ a - b ∈ s) ≤ ⇑I.ringCon ↔ s ⊆ ↑I
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:
case =>

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) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J

Tactic:
case =>

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
⊢ map (jacobson R M).mkQ (jacobson R M) = ⊥

Tactic:
mkQ_map_self

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ⊥ = ⊥
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
inst✝¹ : Nontrivial M
inst✝ : IsCoatomic (Submodule R M)
⊢ jacobson R M < ⊤

Tactic:
by
  obtain ⟨m, hm, -⟩ := (eq_top_or_exists_le_coatom (⊥ : Submodule R M)).resolve_left bot_ne_top
  exact (sInf_le <| Set.mem_ofPred.mpr hm).trans_lt hm.1.lt_top

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
constructor
  · intro h x hx
    rw [← h, Ideal.jacobson, mem_sInf] at hx
    push Not at hx
    exact hx
  · refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
    contrapose hx
    rw [Ideal.jacobson, mem_sInf]
    push Not
    exact h x hx

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ⨅ I ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}, I ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}

Tactic:
sInf_eq_iInf

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ⨅ I ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}, I ≤ ⨅ a ∈ {J | comap f K ≤ J ∧ J.IsMaximal}, a
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = Finsupp.single i ((Algebra.linearMap R Rₛ) 1)

Tactic:
Algebra.linearMap_apply,

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = Finsupp.single i ((algebraMap R Rₛ) 1)
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
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F✝ F' : C ⥤ D
G : D ⥤ E
F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C
x✝ : Discrete PUnit.{w + 1}
⊢ x✝ = (trivial (Discrete PUnit.{w + 1})).X

Tactic:
by ext

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ { l //
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ l = s.inl ∧
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
          (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
            (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = l }

Tactic:
refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩
    · ext
      · simp [PushoutCocone.condition]
      · simp
    · simp
    · intro m h₁ h₂
      dsimp at m h₁ h₂ ⊢
      ext
      · simpa using h₂
      · simp [← h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)

Tactic:
rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

Tactic:
rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
      ext (x : S)
      simp [mkUnder_right]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.left = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.left

Tactic:
exact h₁.uniq ((fst _ _).mapCone s) _ (by simp [← hm])

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ ∃ s', s' • m = 0

Tactic:
by
  simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: X : CommRingCat
f : X ⟶ of PUnit.{u + 1}
⊢ f = default

Tactic:
by ext

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
rw [← essentiallySmall_op_iff, op_unop]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
Z : Cᵒᵖ
y : (yoneda.obj (CostructuredArrow.mk (yonedaEquiv.symm (unop X✝).snd)).left).obj Z
⊢ (ConcreteCategory.hom
          ((yoneda.map (↑f.unop).unop ≫ (CostructuredArrow.mk (yonedaEquiv.symm (unop Y✝).snd)).hom).app Z)).toFun
      y =
    (ConcreteCategory.hom ((CostructuredArrow.mk (yonedaEquiv.symm (unop X✝).snd)).hom.app Z)).toFun y

Tactic:
simp [yonedaEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
d : ↑(F.obj c)
⊢ { base := 𝟙 { base := c, fiber := d }.base, fiber := eqToHom ⋯ ≫ 𝟙 d } = 𝟙 { base := c, fiber := d }

Tactic:
by
    dsimp
    congr
    simp only [Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X Y : WithInitial C
f : X ⟶ Y
⊢ ((map F).map f ≫
      match Y with
      | of x => η.app x
      | star => 𝟙 star) =
    (match X with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map f

Tactic:
match X, Y, f with
    | of x, of y, f => exact η.naturality f
    | star, of x, _ => rfl
    | star, star, _ => rfl

Goal state after: