mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

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 : IsIso g
this : HasPushout f g
⊢ IsIso inl

Tactic:
rw [← h.inl_isoPushout_inv]

Goal state after:
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 : IsIso g
this : HasPushout f g
⊢ IsIso (pushout.inl f g ≫ h.isoPushout.inv)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1

Tactic:
have hu1' := congr_arg ((u2 * s3) • ·) hu1.symm

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (u2 * s3) • u1 • (m1, s1).2 • (m2, s2).1 = (u2 * s3) • u1 • (m2, s2).2 • (m1, s1).1
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
x : S
a : A
⊢ (tensorProductEquivOfMapIncludeRight R S M B C) (x ⊗ₜ[R] (algebraMap A B) a) = (algebraMap (S ⊗[R] A) C) (x ⊗ₜ[R] a)

Tactic:
let : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
    (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toAlgebra
  have heq : x ⊗ₜ[R] (algebraMap A B) a = algebraMap _ _ (x ⊗ₜ[R] a) := rfl
  simp [heq, IsLocalization.tensorProductEquivOfMapIncludeRight]

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
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
h✝ : HasColimit (span f g)
P : C
fst : X ⟶ P
snd : Y ⟶ P
h : IsPushout f g fst snd
h' : IsPushout (F.map f) (F.map g) (F.map fst) (F.map snd)
⊢ PreservesColimit (span f g) F

Tactic:
rwa [h.preservesColimit_span_iff]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
⊢ ↑x = (fun l ↦ ↑l) <$> x

Tactic:
dsimp [castFreeCommRing, toFreeCommRing, FreeRing.lift, FreeRing, FreeAbelianGroup.liftMonoid_coe,
    Functor.map]

Goal state after:
α : Type u
x : FreeRing α
⊢ (FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x =
    (FreeAbelianGroup.lift ((fun α_1 ↦ FreeAbelianGroup.of α_1) ∘ fun l ↦ ↑l)) x
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj X)).map f ≫ (adj.homEquiv (unop X) (K.obj j')) (t.app j') =
    (adj.homEquiv ((unop ((const J).op.obj X)).obj j) (K.obj j'))
      ((unop ((const J).op.obj (F.op.obj X))).map f ≫ t.app j')

Tactic:
Category.id_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (adj.homEquiv (unop X) (K.obj j')) (t.app j') =
    (adj.homEquiv ((unop ((const J).op.obj X)).obj j) (K.obj j'))
      ((unop ((const J).op.obj (F.op.obj X))).map f ≫ t.app j')
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj (F.op.obj X))).map f ≫ (adj.homEquiv (unop X) (K.obj j')).symm (t.app j') =
    (adj.homEquiv (unop X) (K.obj j')).symm ((unop ((const J).op.obj X)).map f ≫ t.app j')

Tactic:
Category.id_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ (adj.homEquiv (unop X) (K.obj j')).symm (t.app j') =
    (adj.homEquiv (unop X) (K.obj j')).symm ((unop ((const J).op.obj X)).map f ≫ t.app j')
Module: Mathlib.CategoryTheory.Monad.Products

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
X✝ Y✝ : (prodComonad X).Coalgebra
f : X✝ ⟶ Y✝
⊢ f.f ≫ (Over.mk (Y✝.a ≫ prod.fst)).hom = (Over.mk (X✝.a ≫ prod.fst)).hom

Tactic:
simp [← dsimp% f.h_assoc]

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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ lift' S g h (mk (b' • a + b • a') (b * b')) = lift' S g h (mk a b) + lift' S g h (mk a' b')

Tactic:
LocalizedModule.lift'_mk,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (b' • a + b • a')) = lift' S g h (mk a b) + lift' S g h (mk a' b')
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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (b' • a + b • a')) = lift' S g h (mk a b) + lift' S g h (mk a' b')

Tactic:
LocalizedModule.lift'_mk,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (b' • a + b • a')) = ↑⋯.unit⁻¹ (g a) + lift' S g h (mk a' b')
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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • lift' S g h (mk a b) = lift' S g h (r • mk a b)

Tactic:
LocalizedModule.lift'_mk,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (g a) = lift' S g h (r • mk a b)
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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (g a) = lift' S g h (mk (r • a) b)

Tactic:
LocalizedModule.lift'_mk,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (g a) = ↑⋯.unit⁻¹ (g (r • 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
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''
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
⊢ fromLocalizedModule' S f (r • x) = (RingHom.id R) r • fromLocalizedModule' S f x

Tactic:
rw [fromLocalizedModule'_smul, RingHom.id_apply]

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
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (h.unit.app A))).pt ⟶ s.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (StructuredArrow.mk (h.unit.app A))).ι.app j ≫ m = s.ι.app j
⊢ m = StructuredArrow.homMk ((h.homEquiv A s.pt.right).symm s.pt.hom) ⋯

Tactic:
apply StructuredArrow.ext
    simp [← StructuredArrow.w m]

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f = ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g

Tactic:
by
      ext ⟨x, e⟩
      simpa using e

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

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

Tactic:
by simp; rfl

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).hom =
    ((G.mapFunctor (F.obj a✝) (F.obj b✝)).map (F.mapComp f (𝟙 b✝)) ≫ G.mapComp (F.map f) (F.map (𝟙 b✝))) ≫
      (F.comp G.toPrelaxFunctor).map f ◁ ((G.mapFunctor (F.obj b✝) (F.obj b✝)).map (F.mapId b✝) ≫ G.mapId (F.obj b✝)) ≫
        (ρ_ ((F.comp G.toPrelaxFunctor).map f)).hom

Tactic:
dsimp
    simp only [map₂_rightUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_right_assoc,
      whiskerLeft_comp, assoc]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ⇑f
hfk : (RingHom.ker f.toRingHom).FG
ulift_var : MvPolynomial (ULift.{u_1, 0} (Fin n)) R ≃ₐ[R] MvPolynomial (Fin n) R :=
  MvPolynomial.renameEquiv R Equiv.ulift
⊢ (RingHom.ker ↑↑ulift_var).FG

Tactic:
simpa using! Submodule.fg_bot

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case right
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ (RingHom.ker ↑↑equiv.symm).FG

Tactic:
simpa using! Submodule.fg_bot

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case intro.refine_1
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (RingHom.ker ↑↑(MvPolynomial.sumAlgEquiv R ι ι')).FG

Tactic:
rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
    exact Submodule.fg_bot

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (F.map (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst).hom))
      ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).snd =
    (unop X).snd

Tactic:
by simp; rfl

Goal state after:
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
⊢ m ≫ prod.fst = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫ prod.fst

Tactic:
simp [← L]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ 𝟙 (F.obj star) ≫ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x)) ≫ F.map (incl.map f)

Tactic:
Category.id_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x)) ≫ F.map (incl.map f)
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 : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
⊢ H.mapCone (Cone.whisker F (liftLimit ((isLimitExtendConeEquiv F c).symm hc))) ≅ c

Tactic:
let i := liftedLimitMapsToOriginal ((isLimitExtendConeEquiv F (G := G ⋙ H) _).symm hc)

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
i : H.mapCone (liftLimit ((isLimitExtendConeEquiv F c).symm hc)) ≅ extendCone.obj c :=
  liftedLimitMapsToOriginal ((isLimitExtendConeEquiv F c).symm hc)
⊢ H.mapCone (Cone.whisker F (liftLimit ((isLimitExtendConeEquiv F c).symm hc))) ≅ c
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (Cofork.ofπ h ⋯)

Tactic:
apply Cofork.IsColimit.mk' _ _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (s : Cofork (gr.left ≫ f) (gr.right ≫ f)) →
    { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
⊢ { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.symm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
⊢ { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
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
⊢ ∀ (f g : Arrow C) (x : f ≅ g), W.limitsOfShape J f.hom → W.limitsOfShape J g.hom

Tactic:
rintro ⟨_, _, f⟩ ⟨Y₁, Y₂, g⟩ e ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩
    let e₁ := Arrow.leftFunc.mapIso e
    let e₂ := Arrow.rightFunc.mapIso e
    have fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift (Cone.mk _ (c₁.π ≫ f)) :=
      e.inv.w.symm
    let c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const _).map e₁.inv ≫ c₁.π }
    let c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const _).map e₂.inv ≫ c₂.π }
    have h₁' : IsLimit c₁' := IsLimit.ofIsoLimit h₁ (Cone.ext e₁)
    have h₂' : IsLimit c₂' := IsLimit.ofIsoLimit h₂ (Cone.ext e₂)
    obtain hg : h₂'.lift (Cone.mk _ (c₁'.π ≫ f)) = g :=
      h₂'.hom_ext (fun j ↦ by
        rw [h₂'.fac]
        simp [reassoc_of% fac, c₁', c₂'])
    rw [← hg]
    exact ⟨_, _, _, _, h₁', _, _, hf⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (extendCofan c₁ c₂).ι.app { as := i.castSucc } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.castSucc } →
      (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.succ }

Tactic:
· rintro i -
      dsimp only [extendCofan_ι_app]
      rw [Fin.cases_succ, assoc, (BinaryCofan.IsColimit.desc' t₂ _ _).2.2, t₁.fac]
      rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ 𝟙 (F.obj ⊥) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x✝

Tactic:
Category.id_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x✝
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
X : C
h : P.isoClosure.ColimitOfShape J X
obj : J → C
h₁ : ∀ (j : J), P (obj j)
h₂ : ∀ (j : J), Nonempty (h.diag.obj j ≅ obj j)
⊢ P.colimitsOfShape J X

Tactic:
exact
   ⟨{ toColimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv

Tactic:
Category.id_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ i₁ = (i₁ ≫ e.hom) ≫ e.inv
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app j = 𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app j

Tactic:
by rintro ⟨_ | _⟩ <;> simp [tensorHom]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ∀ (j : Discrete WalkingPair),
    (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j =
      tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j

Tactic:
by rintro ⟨_ | _⟩ <;> simp [tensorHom]

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 : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
    (α_ X X X).hom ≫
      X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫
        α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))

Tactic:
by
    apply α.homEquiv'.injective
    simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]
    simp only [← α.homEquiv'_comp]
    simp only [whiskerRight_fst, whiskerRight_snd, whiskerLeft_fst, associator_hom_fst,
      whiskerLeft_snd, α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul, _root_.mul_assoc]
    simp only [← α.homEquiv'_comp]
    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
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B : C
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
unfold prodComparison
  ext <;> simp [← G.map_comp]

Goal state after: