mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x + y) • mk m s = mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s) + y • mk m s

Tactic:
smul_def T y,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x + y) • mk m s =
    mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s) +
      mk ((IsLocalization.sec S y).1 • m) ((IsLocalization.sec S y).2 * s)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) =
    ((fun α_1 ↦ FreeAbelianGroup.of α_1) ∘ fun l ↦ ↑l) L

Tactic:
simp only [AddMonoidHom.coe_coe, comp_apply, FreeAbelianGroup.lift_apply_of]

Goal state after:
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ (FreeMonoid.lift FreeCommRing.of) L = FreeAbelianGroup.of ↑L
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ 1 • 1 • s • m = 1 • s • m

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x y : LocalizedModule S M
⊢ r • x = y ↔ x = Localization.mk 1 ⟨r, hr⟩ • y

Tactic:
induction x using induction_on with
  | h m s =>
    induction y using induction_on with
    | h n t =>
      rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]
      simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]
      fconstructor
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mk 0 1 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x y : A), mk (x + y) 1 = mk x 1 + mk y 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x y : M
⊢ mk (x + y) 1 = mk x 1 + mk y 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ (fun f ↦ T.η.app X ≫ f.f) ((fun f ↦ { f := T.map f ≫ Y.a, h := ⋯ }) f) = f

Tactic:
dsimp only [forget_obj]
            rw [← T.η.naturality_assoc, Y.unit]
            apply Category.comp_id

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ T.η.app X ≫ retraction (T.η.app X) = 𝟙 ((𝟭 C).obj X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ T.map (inv f.f) ≫ A.a = B.a ≫ inv f.f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₁ ≅ T₂
⊢ 𝟙 T₁ = h.hom ≫ h.inv

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₁ ≅ T₂
⊢ h.inv ≫ h.hom = 𝟙 T₂

Tactic:
by simp

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
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this : c • s • g m' = c • s' • g m
⊢ IsUnit ⋯.unit.inv

Tactic:
by simp

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)
⊢ section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 ((𝟭 C).obj X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
A : (prodComonad X).Coalgebra
⊢ (((𝟭 (prodComonad X).Coalgebra).obj A).a ≫
        (prodComonad X).map (Iso.refl ((𝟭 (prodComonad X).Coalgebra).obj A).A).hom) ≫
      prod.fst =
    ((Iso.refl ((𝟭 (prodComonad X).Coalgebra).obj A).A).hom ≫ ((coalgebraToOver X ⋙ overToCoalgebra X).obj A).a) ≫
      prod.fst

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
A : (coprodMonad X).Algebra
⊢ coprod.inl ≫
      (coprodMonad X).map (Iso.refl ((𝟭 (coprodMonad X).Algebra).obj A).A).hom ≫
        ((algebraToUnder X ⋙ underToAlgebra X).obj A).a =
    coprod.inl ≫ ((𝟭 (coprodMonad X).Algebra).obj A).a ≫ (Iso.refl ((𝟭 (coprodMonad X).Algebra).obj A).A).hom

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
x₁ x₂ : M
e : (↑R f) x₁ = (↑R f) x₂
⊢ ∃ c, c • x₁ = c • x₂

Tactic:
obtain ⟨⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩, hc⟩ := h.3 e
    exact ⟨⟨r, hr⟩, by simpa [Submonoid.smul_def] using hc⟩

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

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
X Y Z : Under R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom (f ≫ g))).toUnder =
    (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).toUnder ≫
      (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)).toUnder

Tactic:
simp [Algebra.TensorProduct.map_id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacksAlong f
x : Over X
y : Over Y
u : (map f).obj x ⟶ y
⊢ Hom.left u ≫ y.hom = x.hom ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
Z : C
⊢ ((star Y).obj Z).hom = prod.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
Z : C
⊢ (pullback.congrHom ⋯ ⋯ ≪≫ pullbackSymmetry prod.fst f ≪≫ pullbackProdFstIsoProd f Z).hom ≫ ((star X).obj Z).hom =
    ((star Y ⋙ pullback f).obj Z).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
v : x ⟶ (map f).obj y
⊢ x.hom ≫ Hom.right v = f ≫ y.hom

Tactic:
by simp

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

Goal state before:
pp: R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ofHom (algebraMap R S) ≫ (Iso.refl (of S)).hom = (Iso.refl (of R)).hom ≫ ofHom (algebraMap R S)

Tactic:
by simp

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

Goal state before:
pp: R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ofHom (algebraMap R A) ≫ (Iso.refl (of A)).hom = (Iso.refl (of R)).hom ≫ ofHom (algebraMap R A)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
x✝¹ : C
x✝ : D
⊢ ∀ (Y' : D) (g : x✝ ⟶ Y') (h : (⊥_ StructuredArrow x✝¹ G).right ⟶ x✝),
    (leftAdjointOfStructuredArrowInitialsAux G x✝¹ Y') (h ≫ g) =
      (leftAdjointOfStructuredArrowInitialsAux G x✝¹ x✝) h ≫ G.map g

Tactic:
by simp

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

Goal state before:
pp: X : CommRingCat
⊢ ∀ (x y : ↑X), (↑1).toFun (x + y) = (↑1).toFun x + (↑1).toFun y

Tactic:
by simp

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

Goal state before:
pp: X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ∀ (x y : ↑X), (↑1).toFun (x + y) = (↑1).toFun x + (↑1).toFun y

Tactic:
by simp

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
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_surj : Function.Surjective ⇑h
s : ↥S
x : M
⊢ ((map S f g) h) (mk' f x s) = Function.uncurry (mk' g) (h x, s)

Tactic:
by simp

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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l ↦ l ∘ₗ f = f) y → y = e
⊢ (fun l ↦ l ∘ₗ f = f) ↑(LinearEquiv.refl R (LocalizedModule S M))

Tactic:
by simp

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_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
by
  have := (iso_apply_mk S (mkLinearMap S M₁) (g m) s).symm
  rw [iso_localizedModule_eq_refl, refl_apply] at this
  simpa [map, lift, iso_localizedModule_eq_refl S M₀]

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ IsLimit (equalizerFork f g)

Tactic:
by
  fapply Fork.IsLimit.mk'
  intro s
  use ofHom <| s.ι.hom.codRestrict _ fun x => (ConcreteCategory.congr_hom s.condition x :)
  constructor
  · ext
    rfl
  · intro m hm
    ext x
    exact Subtype.ext <| RingHom.congr_fun (congrArg Hom.hom hm) x

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ (ConcreteCategory.hom (F.map (𝟙 zero))) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x) =
    (ConcreteCategory.hom (F.map (𝟙 zero))) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
by simp

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ (ConcreteCategory.hom (F.map (𝟙 (op one)))) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x) =
    (ConcreteCategory.hom (F.map (𝟙 (op one)))) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ ∀ {Y Z : J} (g : Y ⟶ Z), c.π.app Y ≫ F.map ((𝟭 J).map g) = c.π.app Z

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
j : J
⊢ (((const J).obj (Under.mk (𝟙 c.pt))).obj j).hom ≫ c.π.app j =
    ((c.toStructuredArrow ⋙ StructuredArrow.toUnder c.pt F).obj j).hom

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ (((const J).obj (Under.mk (𝟙 (limit F)))).obj j).hom ≫ π F j =
    ((toStructuredArrow F ⋙ StructuredArrow.toUnder (limit F) F).obj j).hom

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ ∀ {Y Z : J} (g : Y ⟶ Z), F.map ((𝟭 J).map g) ≫ c.ι.app Z = c.ι.app Y

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
j : J
⊢ c.ι.app j ≫ (((const J).obj (Over.mk (𝟙 c.pt))).obj j).hom =
    ((c.toCostructuredArrow ⋙ CostructuredArrow.toOver F c.pt).obj j).hom

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ ι F j ≫ (((const J).obj (Over.mk (𝟙 (colimit F)))).obj j).hom =
    ((toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj j).hom

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∈ S
x✝ : M
⊢ 0 • x✝ = 0

Tactic:
by simp

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

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (ConcreteCategory.hom ((cospan f g).map (𝟙 (some WalkingPair.left))))
      ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.left))) x) =
    (ConcreteCategory.hom ((cospan f g).map (𝟙 left))) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommAlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommAlgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommAlgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommAlgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Algebra R X
inst✝³ : CommRing Y
inst✝² : Algebra R Y
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Algebra R X
inst✝³ : CommRing Y
inst✝² : Algebra R Y
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
by simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, op (X i) = Z) → ∃ i, X i = unop Z

Tactic:
rintro ⟨i, hi⟩
    exact ⟨i, by rw [← hi]⟩

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

Goal state before:
pp: case singleton
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
x : R
h' : R ∙ x ≤ J.radical
⊢ ∃ n, (R ∙ x) ^ n ≤ J

Tactic:
simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'

Goal state after:
case singleton
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
x : R
h' : x ∈ J.radical
⊢ ∃ n, (R ∙ x) ^ n ≤ J
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j : J
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((const J).obj ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj).map f ≫
        (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ ((const J).obj (F.obj j)).map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ ∀ (X : C), ⊤ ((𝟭 C).obj X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
i : ι
⊢ ofObj X (X i)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
F : C ⥤ D
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure.map F ≤ (Q.strictMap F).isoClosure

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
p : F.Elements
⊢ (ConcreteCategory.hom (F.map (𝟙 p.fst))) p.snd = p.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : ⊤ ≤ P.isoClosure
y : F.Elements
x✝ : ⊤ y
⊢ ⊤ y.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ (F.map (𝟙 X)).toFunctor.obj d = d

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ (Grothendieck.ι F X).obj d = (Grothendieck.ι F X).obj ((F.map (𝟙 X)).toFunctor.obj d)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ (F.map (f ≫ g)).toFunctor.obj d = (F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)

Tactic:
by simp

Goal state after: