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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • 1 = mk ((algebraMap R A) a) s
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'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)) = mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂))

Tactic:
mul_assoc,

Goal state after:
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'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)) = mk (t₂ • s • m₁ + t₁ • s • m₂) (s * (t₁ * (s * t₂)))
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 : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M
h : e (f x₁✝) = e (f x₂✝)
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
EmbeddingLike.apply_eq_iff_eq

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''
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 : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M
h : f x₁✝ = f x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝
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'
⊢ ↑⋯.unit⁻¹ (g m) = ↑⋯.unit⁻¹ (g m')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, eq_comm,
      Module.End.algebraMap_isUnit_inv_apply_eq_iff]

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''
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'
⊢ ↑(m, s).2 • g m' = ↑(m', s').2 • g m
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (f (b' • a + b • a')) = ↑⋯.unit⁻¹ (f a) + ↑⋯.unit⁻¹ (f a')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul, ← map_smul,
        ← map_smul, map_add]

Goal state after:
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b' • a) + f (b • a') = ↑⋯.unit⁻¹ (f (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • f a')
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
⊢ ↑(iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M

Tactic:
ext m
  rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe, iso_symm_apply']
  exact one_smul _ _

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

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) ≫ h.isoPushout.inv)) x =
      (ConcreteCategory.hom (ofHom (algebraMap R' S'))) x
⊢ Algebra.IsPushout R R' S S'

Tactic:
dsimp only [hom_comp, RingHom.coe_comp, Function.comp_apply, hom_ofHom] at h3

Goal state after:
R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
⊢ Algebra.IsPushout R R' S S'
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X

Tactic:
· ext x
    have e : (0 : X) = 1 := by
      rw [← f.hom.map_one, ← f.hom.map_zero]
    replace e : 0 * x = 1 * x := congr_arg (· * x) e
    rw [one_mul, zero_mul, ← f.hom.map_zero] at e
    exact e

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
h : ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) r)
⊢ IsUnit r

Tactic:
simp only [isUnit_iff_exists_inv] at h ⊢

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
h : ∀ (j : J), ∃ b, (ConcreteCategory.hom (c.π.app j)) r * b = 1
⊢ ∃ b, r * b = 1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
⊢ IsLocalHom (Hom.hom (c.π.app j))

Tactic:
refine ⟨fun (x : c.pt) hx ↦ (?_ : IsUnit x)⟩
  rw [isUnit_iff_forall_isUnit F hc]; intro i
  obtain ⟨k, f, g, lh, eq⟩ := hj x hx i
  exact lh.map_nonunit _ (eq ▸ hx.map _)

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) =
    (α_ (F.map f) (F.map g) (F.map h)).inv ≫ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom

Tactic:
by
  simp only [map₂_associator, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)} → j₂✝ ∈ {j | Nonempty (Z j)}

Tactic:
by rintro ⟨y⟩; exact ⟨h₁ f y⟩

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 Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
by
  obtain ⟨P', _, hP'⟩ := EssentiallySmall.exists_small_le' P
  obtain ⟨Q', _, hQ'⟩ := EssentiallySmall.exists_small_le' Q
  refine ⟨P' ⊔ Q', inferInstance, ?_⟩
  simp only [sup_le_iff]
  constructor
  · exact hP'.trans (monotone_isoClosure le_sup_left)
  · exact hQ'.trans (monotone_isoClosure le_sup_right)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : EffectiveEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ ≫ u = x✝ ≫ u

Tactic:
by
      simpa [← sq.w, cancel_mono_assoc_iff] using h =≫ v

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ ∀ (a : α), π a ≫ (asIso (Sigma.desc π)).inv ≫ Sigma.desc e = e a

Tactic:
by
    intro a
    have : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom := by simp only [asIso_hom,
      colimit.ι_desc, Cofan.mk_ι_app]
    rw [this, assoc]
    simp only [asIso_hom, asIso_inv, IsIso.hom_inv_id_assoc, colimit.ι_desc,
      Cofan.mk_ι_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ ∀ {X_1 Y_1 : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1),
    (parallelPair f.op g.op).map f_1 ≫
        (match Y_1 with
          | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
          | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
      (match X_1 with
          | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
          | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
        (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map f_1

Tactic:
by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inl f f =
    ((pushoutIsoOpPullback f f).inv.unop ≫ pullback.fst f.unop f.unop).op

Tactic:
pushoutIsoOpPullback_inv_fst,

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inl f f = (pushout.inl f f).unop.op
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ s.ι.app WalkingParallelPair.one = g₂ ≫ s.ι.app WalkingParallelPair.one

Tactic:
by
      simp only [Cofork.app_one_eq_π]
      rw [← PullbackCone.IsLimit.lift_snd hc g₁ g₂ hg,
        Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
      simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ m ≫ (IsPullback.cone small_k).snd = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).snd

Tactic:
· exact (hm WalkingCospan.right).trans (by simp)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ =
    pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄

Tactic:
by rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_fst]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
Iso.comp_inv_eq,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
Iso.comp_inv_eq,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
⊢ ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) (x : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ

Tactic:
intro X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
j : J
⊢ (Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }

Tactic:
have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
j : J
this :
  (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } =
    { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι }.ι.app j
⊢ (Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
e : J ≌ J'
⊢ P.IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J'

Tactic:
simp only [isClosedUnderLimitsOfShape_iff, P.limitsOfShape_congr e]

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
⊢ ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ

Tactic:
intro X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W₁ f
⊢ coproducts.{w, v, u} W₂ f

Tactic:
rw [coproducts_iff] at hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J, W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f
Module: Mathlib.CategoryTheory.Limits.FullSubcategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : Category.{w', w} J
inst✝² : HasLimitsOfShape J P.FullSubcategory
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : PreservesLimitsOfShape J P.ι
⊢ P.limitsOfShape J ≤ P

Tactic:
rintro X ⟨p⟩
    exact P.prop_of_iso (IsLimit.conePointUniqueUpToIso
      (isLimitOfPreserves P.ι (limit.isLimit (P.lift p.diag p.prop_diag_obj)))
        p.isLimit) (limit (P.lift p.diag p.prop_diag_obj)).property

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W f
⊢ W f

Tactic:
rw [coproducts_iff] at hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : ∃ J, W.colimitsOfShape (Discrete J) f
⊢ W f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift (toUnit X) f ≫ snd (𝟙_ C) M = f

Tactic:
exact lift_snd _ _

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (M.X ⊗ M.X)))) (𝟙 (M.X ⊗ M.X) ≫ μ) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
← lift_fst_snd

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (M.X ⊗ M.X)))) (lift (fst M.X M.X) (snd M.X M.X) ≫ μ) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
⊢ (F ⋙ forget MonCat).IsRepresentable → yonedaMon.essImage F

Tactic:
rintro ⟨X, ⟨e⟩⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
X : C
e : (F ⋙ forget MonCat).RepresentableBy X
⊢ yonedaMon.essImage F
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ η = toUnit (𝟙_ C) ≫ η

Tactic:
rw [toUnit_unique (toUnit _) (𝟙 _), Category.id_comp]

Goal state after: