mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ (PushoutCocone.mk f g ⋯).inr ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
    ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
      (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl →
        (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
use BinaryCofan.IsColimit.inr_desc H₂ _ _

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
⊢ l₁ ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd

Tactic:
by simp [reassoc_of% hl₁', hl₂']

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPushout f g h i

Tactic:
refine ⟨⟨e⟩, ⟨isColimitOfReflects F <| ?_⟩⟩
  refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit
  exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _),
    (Category.comp_id _).trans (Category.id_comp _)]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
⊢ PreservesLimitsOfShape WalkingCospan F

Tactic:
refine preservesLimitsOfShape_walkingCospan_of_forall_isPullback fun X Y Z f g hfg ↦ ?_
  use pullback f g, pullback.fst f g, pullback.snd f g, .of_hasPullback f g
  rw [isPullback_iff_isLimit_binaryFan_of_isThin]
  refine ⟨(BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).isLimitMapConeEquiv ?_⟩
  apply isLimitOfPreserves _ (Nonempty.some ?_)
  rw [← CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin (f := f) (g := g)]
  exact .of_hasPullback f g

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
this : ∃ n, X = ↑n
⊢ 1 = 0

Tactic:
rcases this with ⟨w, H⟩

Goal state after:
case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = ↑w
⊢ 1 = 0
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case add
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝

Tactic:
rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
⊢ (FreeCommRing.lift fun a ↦ MvPolynomial.X a).comp
      (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of) =
    RingHom.id (MvPolynomial α ℤ)

Tactic:
ext <;> simp

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

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ u, u • t • r • m = u • s • n) ↔ ∃ u, u • (⟨r, hr⟩ * t) • m = u • s • n

Tactic:
simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]

Goal state after:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gˣ
⊢ x ∈ H.units ↔ ↑x ∈ H

Tactic:
Submonoid.mem_units_iff,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gˣ
⊢ ↑x ∈ H.toSubmonoid ∧ ↑x⁻¹ ∈ H.toSubmonoid ↔ ↑x ∈ H
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
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r = (algebraMap R (A ⊗[R] B)) r

pp: R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
r : ↑(of R)
⊢ (algebraMap R (A ⊗[R] B)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Tactic:
· exact Algebra.TensorProduct.includeLeft.commutes (R := R) r

Goal state after:
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
r : ↑(of R)
⊢ (algebraMap R (A ⊗[R] B)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 * x = x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x

Tactic:
zero_mul,

Goal state after:
case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 = x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : (Hom.hom f) 0 = x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x

Tactic:
exact e

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ (F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv

Tactic:
eq_inv_comp,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (λ_ (F.map f)).hom ≫ (F.map₂Iso (λ_ f)).inv = (F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv

Tactic:
eq_inv_comp,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (ρ_ (F.map f)).hom ≫ (F.map₂Iso (ρ_ f)).inv = F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) =
    ((F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
      F.map f ◁ inv (F.mapComp g h)

Tactic:
← Bicategory.inv_whiskerLeft,

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) =
    ((F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
      inv (F.map f ◁ F.mapComp g h)
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ m ≤ n + m - i

Tactic:
lia

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
x✝ : (ιOfLE h).EssSurj
X : C
hX : Q X
⊢ P.isoClosure X

Tactic:
exact ⟨_, ((ιOfLE h).objPreimage ⟨X, hX⟩).2,
      ⟨Q.ι.mapIso ((ιOfLE h).objObjPreimageIso ⟨X, hX⟩).symm⟩⟩

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
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
by
    obtain ⟨Q, _, _, _⟩ := EssentiallySmall.exists_small_le.{w} P
    exact ⟨Q, inferInstance, by rwa [isoClosure_le_iff]⟩

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
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ a, P a ≤ Q.isoClosure

Tactic:
have h (a : α) := EssentiallySmall.exists_small_le' (P a)
    choose Q _ hQ using h
    refine ⟨⨆ a, Q a, inferInstance, ?_⟩
    simp only [iSup_le_iff]
    intro a
    exact (hQ a).trans (monotone_isoClosure (le_iSup Q a))

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ ∃ inv, homFromCommaOfIsIso i ≫ inv = 𝟙 X ∧ inv ≫ homFromCommaOfIsIso i = 𝟙 Y

Tactic:
use homFromCommaOfIsIso (inv i)

Goal state after:
case h
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i) = 𝟙 X ∧ homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i = 𝟙 Y
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
j : J
⊢ (m ≫ prod.snd) ≫ c.π.app j = (forgetCone s).π.app j

Tactic:
simp [← L j]

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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
⊢ H.map { base := f, fiber := eqToHom ⋯ } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)) } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))

Tactic:
have := Functor.congr_obj congr($(α.naturality f).toFunctor) d

Goal state after:
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
this : (F.map f ≫ α.app Y✝).toFunctor.obj d = (α.app X✝ ≫ G.map f).toFunctor.obj d
⊢ H.map { base := f, fiber := eqToHom ⋯ } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)) } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
          ⋯).fst =
    s.fst

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ fst i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_π_app]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ snd i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_π_app]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    fst i₁ i₂ ≫ i₁ ≫ fst f i

Tactic:
simp only [limit.lift_π, PullbackCone.mk_π_app]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))

Tactic:
ext <;> simp

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

Goal state before:
pp: case refine_1.refine_4
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i) =
    (congrHom ⋯ ⋯).hom ≫
      map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ diagonal (f ≫ g) =
    diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯)

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ diagonal g = diagonal (f ≫ g) ≫ map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯

Tactic:
ext <;> simp

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

Goal state before:
pp: case w₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ diagonal (fst f g) =
    (pullbackSymmetry f (Over.mk g).hom).hom ≫
      Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ autoParam (g ≫ diagonal f = lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) CommSq.w._autoParam

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) = 𝟙 (X ⊗ Y)

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ (h ⊗ₘ k) = lift (f ≫ h) (g ≫ k)

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') = g ⊗ₘ g'

Tactic:
ext <;> simp

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

Goal state before:
pp: case e_a.e_a
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₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom = lift f₁ (lift f₂ f₃)

Tactic:
ext <;> simp

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 X : C
inst✝¹ : MonObj M
F : C ⥤ D
inst✝ : F.Monoidal
⊢ F.map 1 = 1

Tactic:
simp [Hom.one_def]

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
f : M ⟶ N
inst✝ : IsMonHom f
X : C
⊢ 1 ≫ f = 1

Tactic:
simp [Hom.one_def]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ 1 ≫ f = 1

Tactic:
simp [Hom.one_def]

Goal state after:
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
inst✝ : BraidedCategory C
⊢ IsCommMonObj M ↔ ∀ (X : C), IsMulCommutative (X ⟶ M)

Tactic:
by
  exact ⟨fun h X ↦ ⟨⟨by simp [mul_comm]⟩⟩, fun h ↦ ⟨by simp [mul_eq_mul, comp_mul, mul_comm]⟩⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ prodComparisonIso (𝟭 C) A B = Iso.refl ((𝟭 C).obj (A ⊗ B))

Tactic:
ext <;> simp

Goal state after: