mathlib-initiative/mathlib-tactics huggingface dataset:
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''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
e : M →ₗ[R] M'
f : M' →ₗ[R] M''
he : Function.Bijective ⇑e
⊢ IsLocalizedModule S (f ∘ₗ e) ↔ IsLocalizedModule S f

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ .of_linearEquiv_right _ _ (.ofBijective _ he)⟩

Goal state after:
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''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
e : M →ₗ[R] M'
f : M' →ₗ[R] M''
he : Function.Bijective ⇑e
h : IsLocalizedModule S (f ∘ₗ e)
⊢ IsLocalizedModule S f
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''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
e : M →ₗ[R] M'
f : M' →ₗ[R] M''
he : Function.Bijective ⇑e
h : IsLocalizedModule S (f ∘ₗ e)
x✝ : M'
⊢ ((f ∘ₗ e) ∘ₗ ↑(LinearEquiv.ofBijective e he).symm) x✝ = f x✝

Tactic:
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
h : A.A ≅ B.A
w : T.map h.hom ≫ B.a = A.a ≫ h.hom
⊢ T.map (h.inv ≫ h.hom) ≫ B.a = B.a

Tactic:
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 : T.free.obj X ⟶ Y
⊢ ((fun f ↦ { f := T.map f ≫ Y.a, h := ⋯ }) ((fun f ↦ T.η.app X ≫ f.f) f)).f = f.f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
⊢ i.inv.app X ≫ 𝟙 (T.obj X) ≫ i.hom.app ((𝟭 C).obj X) = 𝟙 (F.obj X)

Tactic:
simp

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:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
h : A.A ≅ B.A
w : A.a ≫ G.map h.hom = h.hom ≫ B.a
⊢ A.a ≫ G.map (h.hom ≫ h.inv) = A.a

Tactic:
simp

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

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

Tactic:
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:
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:
simp

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

Goal state before:
pp: R S : CommRingCat
A B : Under R
f : A ⟶ B
a : ↑R
⊢ (ConcreteCategory.hom (A.hom ≫ Under.Hom.right f)) a = (ConcreteCategory.hom B.hom) a

Tactic:
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✝ : HasPullbacksAlong f
x : Over X
y : Over Y
u : (map f).obj x ⟶ y
⊢ Hom.left u ≫ y.hom = x.hom ≫ f

Tactic:
simp

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

Goal state before:
pp: case h₀
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
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.fst y.hom f = Hom.left v ≫ pullback.fst y.hom f

Tactic:
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:
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:
simp

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

Goal state before:
pp: R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝ : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) x✝ =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) x✝

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case h₀
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
u : (pushout f).obj x ⟶ y
⊢ pushout.inl x.hom f ≫ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = pushout.inl x.hom f ≫ Hom.right u

Tactic:
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''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
x : M
⊢ (l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M) x = (l ∘ₗ f) x

Tactic:
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
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
Z : Under X
⊢ Mono ((mapPushoutAdj f).unit.app Z)

Tactic:
simp

Goal state after:
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
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
Z : Under X
⊢ Mono (homMk (pushout.inl Z.hom f) ⋯)
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''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
g : M' →ₗ[R] M''
inst✝ : IsLocalizedModule S (g ∘ₗ f)
x✝ : M
⊢ (↑(linearEquiv S f (g ∘ₗ f)) ∘ₗ f) x✝ = (g ∘ₗ f) x✝

Tactic:
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:
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), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ G.map f ≫ g =
    (rightAdjointOfCostructuredArrowTerminalsAux G B₁ A).symm
      (f ≫ (rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g)

Tactic:
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
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ * m₂) = f m₁ * f m₂

Tactic:
hf

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

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.left })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.left })) a

Tactic:
simp

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

Goal state before:
pp: case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.right })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.right })) a

Tactic:
simp

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

Goal state before:
pp: case right
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.2

Tactic:
ext b

Goal state after:
case right
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
b : ↑B
⊢ ((AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight) b =
    (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.2
      b
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:
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:
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
x : M
s : ↥S
⊢ ((map S f g) h) (mk' f x s) = mk' g (h x) s

Tactic:
simp only [map, lift, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_apply]
  rw [iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s), LocalizedModule.lift_mk]
  rfl

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
x : M
s : ↥S
⊢ ((map S f f) LinearMap.id) (Function.uncurry (mk' f) (x, s)) = LinearMap.id (Function.uncurry (mk' f) (x, s))

Tactic:
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:
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:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) ≫ F.map₂ η = 𝟙 (F.map g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f : x ⟶ y
⊢ F.map₂ (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f : x ⟶ y
⊢ F.map₂Iso (eqToIso ⋯) = eqToIso ⋯

Tactic:
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
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀
s : ↥S
⊢ ((map S f₀ f₂) (h ∘ₗ g)) (Function.uncurry (mk' f₀) (x, s)) =
    ((map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g) (Function.uncurry (mk' f₀) (x, s))

Tactic:
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 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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case e'_3.e'_7
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
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  ({ pt := X✝.left, π := X✝.hom }.pt ⟶ F.obj j) = (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)
e_6✝ : F = (fromPUnit F).obj Y✝.right
⊢ { pt := X✝.left, π := X✝.hom }.π = X✝.hom ≫ (fromPUnit F).map f.right

Tactic:
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:
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:
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:
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:
simp

Goal state after: