mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_4
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)
⊢ limit.lift F
        { pt := F.1 i,
          π :=
            { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
              naturality := ⋯ } } ≫
      limit.π F i =
    𝟙 (F.obj i)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
⊢ (α_ X₁ Y₁ Z₁).hom ≫ (f ⊗ₘ g ⊗ₘ h) = ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
⊢ (α_ X₁ Y₁ Z₁).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ (λ_ M).hom = (η ⊗ₘ 𝟙 M) ≫ μ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ (ρ_ M).hom = (𝟙 M ⊗ₘ η) ≫ μ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ M ◁ μ ≫ μ = (α_ M M M).inv ≫ μ ▷ M ≫ μ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (η ⊗ₘ η ⊗ₘ η) = (𝟙 (𝟙_ C) ⊗ₘ (λ_ (𝟙_ C)).inv) ≫ (η ⊗ₘ η ⊗ₘ η)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ ((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ₘ η)) ≫ (λ_ M).hom = η

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ ((M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N) ≫ (μ ⊗ₘ μ) =
    (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ)

Tactic:
simp

Goal state after:
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
x✝ : Mₛ
⊢ x✝ ∈ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) ↔ x✝ ∈ ⇑f '' Set.range ⇑b

Tactic:
simp

Goal state after:
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
⊢ f.hom = { hom := η, isMonHom_hom := ⋯ }.hom

Tactic:
← Category.id_comp f.hom

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
⊢ 𝟙 (trivial C).X ≫ f.hom = { hom := η, isMonHom_hom := ⋯ }.hom
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ y✝ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (x✝¹ + y✝)) x✝ =
    (extendScalarsOfIsLocalization S A x✝¹ + extendScalarsOfIsLocalization S A y✝) x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (m✝ • x✝¹)) x✝ = ((RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (↑R (extendScalarsOfIsLocalization S A x✝¹)) x✝ = x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ : M →ₗ[A] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (↑R x✝¹)) x✝ = x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
x✝ : N
⊢ (LinearMap.extendScalarsOfIsLocalization S A ↑f ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm) x✝ =
    LinearMap.id x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
x✝ : M
⊢ (LinearMap.extendScalarsOfIsLocalization S A ↑f.symm ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f) x✝ =
    LinearMap.id x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[R] N
x✝ : M
⊢ ((fun e ↦ restrictScalars R e) ((fun e ↦ extendScalarsOfIsLocalization S A e) e)) x✝ = e x✝

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[A] N
x✝ : M
⊢ ((fun e ↦ extendScalarsOfIsLocalization S A e) ((fun e ↦ restrictScalars R e) e)) x✝ = e x✝

Tactic:
simp

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

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.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
x✝ : N
⊢ (↑R ((mapExtendScalars S f g Rₛ) ↑e ∘ₗ (mapExtendScalars S g f Rₛ) ↑e.symm) ∘ₗ g) x✝ = (↑R LinearMap.id ∘ₗ g) x✝

Tactic:
simp

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

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.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
x✝ : M
⊢ (↑R ((mapExtendScalars S g f Rₛ) ↑e.symm ∘ₗ (mapExtendScalars S f g Rₛ) ↑e) ∘ₗ f) x✝ = (↑R LinearMap.id ∘ₗ f) x✝

Tactic:
simp

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

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
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
x✝ : M
⊢ ((↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l)) ∘ₗ mkLinearMap S M) x✝ =
    ((IsLocalizedModule.map S g₁ g₂) l ∘ₗ g₁) x✝

Tactic:
simp

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

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
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ⇑(↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)) =
    ⇑(IsLocalizedModule.iso S g₂).symm ∘ ⇑((IsLocalizedModule.map S g₁ g₂) l) ∘ ⇑(IsLocalizedModule.iso S g₁)

Tactic:
simp

Goal state after:
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
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ «μ» F X X ▷ F.obj X ≫ «μ» F (X ⊗ X) X ≫ F.map ((α_ X X X).hom ≫ X ◁ μ ≫ μ) =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ «μ» F X X ≫ «μ» F X (X ⊗ X) ≫ F.map (X ◁ μ) ≫ F.map μ

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
N : C
e : F.obj N ≅ M.X
this✝ : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
⊢ η ≫ e.hom = η

Tactic:
simp

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
N : C
e : F.obj N ≅ M.X
this✝ : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
⊢ μ ≫ e.hom = (e.hom ⊗ₘ e.hom) ≫ μ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ hP.lift h k w ≫ fst = h

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ hP.lift h k w ≫ snd = k

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ c.fst = (Iso.refl c.pt).hom ≫ (PullbackCone.mk c.fst c.snd ⋯).fst

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ c.snd = (Iso.refl c.pt).hom ≫ (PullbackCone.mk c.fst c.snd ⋯).snd

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit }).inv ≫ pullback.fst f g = fst

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit }).inv ≫ pullback.snd f g = snd

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
⊢ inl ≫ hP.desc h k w = h

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
⊢ inr ≫ hP.desc h k w = k

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
c : PushoutCocone f g
h : IsColimit c
⊢ c.inl ≫ (Iso.refl c.pt).hom = (PushoutCocone.mk c.inl c.inr ⋯).inl

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
c : PushoutCocone f g
h : IsColimit c
⊢ c.inr ≫ (Iso.refl c.pt).hom = (PushoutCocone.mk c.inl c.inr ⋯).inr

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inl

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inr

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.π.app { as := WalkingPair.left } =
    (Iso.refl c.pt).hom ≫
      (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app
        { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.π.app { as := WalkingPair.right } =
    (Iso.refl c.pt).hom ≫
      (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app
        { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : Mono g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g), (s.fst ≫ inv fst) ≫ fst = s.fst

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
⊢ prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : IsLocalization S A
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
M' : Type u_4
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : Module A M'
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun l ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
⊢ (fun g' ↦ ↑R g' ∘ₗ f = ℓ ∘ₗ f) (LinearMap.extendScalarsOfIsLocalization S A ℓ)

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
⊢ (prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd) ≫ prod.snd =
    s.snd ≫ prod.snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ l ≫ t₁.snd = s.snd

Tactic:
apply PullbackCone.IsLimit.hom_ext H
    · simp [← s.condition, ← hl, ← t₁.condition, ← hi₂]
    · simpa using hl'

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
⊢ ∀
    (s :
      PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
        (hT.from ((pair X Y).obj { as := WalkingPair.right }))),
    BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.fst = s.fst

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
⊢ ∀
    (s :
      PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
        (hT.from ((pair X Y).obj { as := WalkingPair.right }))),
    BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.snd = s.snd

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
s : ↥S
⊢ (equivTensorProduct S M).symm ((equivTensorProduct S M) (mk x s)) =
    (equivTensorProduct S M).symm (Localization.mk 1 s ⊗ₜ[R] x)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ pullback.map (pullback.snd f g) (h ≫ pullback.snd i g) f i (pullback.fst f g) (h ≫ pullback.fst i g) g ⋯ ⋯ ≫
      pullback.fst f i =
    pullback.fst (pullback.snd f g) (h ≫ pullback.snd i g) ≫ pullback.fst f g

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ pullback.map (pullback.snd f g) (h ≫ pullback.snd i g) f i (pullback.fst f g) (h ≫ pullback.fst i g) g ⋯ ⋯ ≫
      pullback.snd f i =
    pullback.snd (pullback.snd f g) (h ≫ pullback.snd i g) ≫ h ≫ pullback.fst i g

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ c.ι.app { as := WalkingPair.left } ≫ (Iso.refl c.pt).hom =
    (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app
      { as := WalkingPair.left }

Tactic:
simp

Goal state after: