mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
⊢ (mateEquiv adj₁ adj₃) (β.whiskerLeft α) = ((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)

Tactic:
by
  ext b
  have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β
  unfold vComp hComp at vcomp
  have vcompb := congr_app vcomp b
  simp only [comp_obj, id_obj, whiskerRight_comp, assoc, mateEquiv_apply, whiskerLeft_comp,
    whiskerLeft_twice, comp_app, Functor.whiskerLeft_app, Functor.whiskerRight_app,
    associator_hom_app, map_id, associator_inv_app, leftUnitor_hom_app, rightUnitor_inv_app,
    Functor.comp_map, Functor.id_map, id_comp, whiskerRight_twice, Iso.inv_hom_id_assoc,
    comp_id] at vcompb
  simpa [mateEquiv]

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

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
⊢ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr) = ⊤

Tactic:
refine top_unique fun x hx => ?_; clear hx
  rw [← x.inl_fst_add_inr_snd_eq]
  refine add_mem ?_ ?_
  · exact le_sup_left (α := Subalgebra S _) <| Set.mem_range_self x.fst
  · exact le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ δ ∘ₗ δ = LinearMap.rTensor M (LinearMap.rTensor M f) ∘ₗ LinearMap.rTensor M δ ∘ₗ δ

Tactic:
← coassoc_symm,

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ δ ∘ₗ δ = LinearMap.rTensor M (LinearMap.rTensor M f) ∘ₗ α⁻¹ ∘ₗ LinearMap.lTensor M δ ∘ₗ δ
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
⊢ Function.HasFiniteMulSupport fun s ↦ f s ^ multiplicity (g s) r

Tactic:
simp only [multiplicity_eq_count_normalizedFactors (hg _) hr, normalize_eq]
  fun_prop

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ span s ≤ I ↔ s ⊆ ↑I

Tactic:
TwoSidedIdeal.ringCon_le_iff,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ (span s).ringCon ≤ I.ringCon ↔ s ⊆ ↑I
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (hI'.from I ≫ f)
⊢ (inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A

Tactic:
by rw [assoc, IsIso.inv_hom_id]

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'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
⊢ IsLocalizedModule S (↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f)

Tactic:
rw [isLocalizedModule_iff_isBaseChange S (Localization S)]

Goal state after:
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'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
⊢ IsBaseChange (Localization S) (↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ -1 = ↑(-1)

Tactic:
Int.cast_neg,

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ -1 = -↑1
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ M.δ.app X = M.δ.app X ≫ M.map (𝟙 (M.obj X))

Tactic:
Functor.map_id

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ M.δ.app X = M.δ.app X ≫ 𝟙 (M.obj (M.obj 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 ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ (unop (op (unop (op K)))).map f ≫ (adj.homEquiv (K.obj j') Y) (t.app j') =
    (adj.homEquiv (K.obj j) Y) (t.app j) ≫ ((const J).obj (G.obj Y)).map f

Tactic:
← adj.homEquiv_naturality_left,

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 ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ (adj.homEquiv ((unop (op (unop (op K)))).obj j) Y) (F.map ((unop (op (unop (op K)))).map f) ≫ t.app j') =
    (adj.homEquiv (K.obj j) Y) (t.app j) ≫ ((const J).obj (G.obj Y)).map f
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
⊢ HasColimit F

Tactic:
have : HasColimit (F ⋙ Comma.fst _ _) := i₁

Goal state after:
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasColimit F
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
· exact ⟨zero, 𝟙 _, 𝟙 _, inferInstance, by simp⟩

Goal state after:
case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
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
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv

Tactic:
by
    rw [F'.mapCompIso_inv, F'.mapCompIso_inv, ← inv_comp_eq, ← IsIso.inv_comp_eq]
    simp

Goal state after:
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
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ (R ∙ x) ^ n ≤ I

Tactic:
rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
⊢ f.hom ≫
      { pt := Over.mk (t₂.π.app star),
            π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.pt.hom =
    { pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.pt.hom

Tactic:
simp [dsimp% f.w star]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
exact ⟨Q.op, inferInstance, by rwa [← op_isoClosure, op_monotone_iff]⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ n I x, I.FG) → FinitePresentation R A

Tactic:
rintro ⟨n, I, e, hfg⟩

Goal state after:
case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
⊢ FinitePresentation R A
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
          ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom) ≫
      colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor =
    𝟙 (colimit (Grothendieck.ι F X ⋙ G))

Tactic:
by
    ext d
    simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]
    conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)]
    rw [← eqToHom_map G (by simp), Grothendieck.eqToHom_eq]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
            ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
        colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
      (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom) ≫
          colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor) ≫
        colimMap
            (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
          colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor

Tactic:
simp only [Functor.comp_obj, Grothendieck.ιNatTrans, ι_colimMap_assoc, NatTrans.comp_app,
      whiskerRight_app, Functor.associator_hom_app, Category.comp_id, colimit.ι_pre, Category.assoc,
      colimit.ι_pre_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    ((G.map ((Grothendieck.ιNatTrans f).app X.fiber) ≫ (Grothendieck.ι F Y.base ⋙ G).map g) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫
      c.ι.app Y.base

Tactic:
Functor.comp_map,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    ((G.map ((Grothendieck.ιNatTrans f).app X.fiber) ≫ G.map ((Grothendieck.ι F Y.base).map g)) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫
      c.ι.app Y.base
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)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.fst =
    s.π.app j ≫ prod.fst

Tactic:
erw [assoc, limMap_π, comp_id, limit.lift_π]
              exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm

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 : Y ⟶ X
inst✝ : EffectiveEpi f
Z✝ : C
m₁ m₂ : X ⟶ Z✝
h : f ≫ m₁ = f ≫ m₂
⊢ m₁ = desc f (f ≫ m₂) ⋯

Tactic:
exact uniq _ _ _ _ h

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 : C ⥤ D
inst✝² : F.Initial
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasLimit G
⊢ IsIso (limit.pre G F)

Tactic:
rw [limit.pre_eq (limitConeComp F (getLimitCone G)) (getLimitCone G)]

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
inst✝ : HasLimit G
⊢ IsIso
    ((limit.isoLimitCone (getLimitCone G)).hom ≫
      (limitConeComp F (getLimitCone G)).isLimit.lift (Cone.whisker F (getLimitCone G).cone) ≫
        (limit.isoLimitCone (limitConeComp F (getLimitCone G))).inv)
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.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : V.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : V.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ U.hom ≫ F.map (StructuredArrow.Hom.right h ≫ q₁) = f ≫ Final.homToLift F Y ≫ F.map q₂

Tactic:
by simp only [F.map_comp, StructuredArrow.w_assoc, hq]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
⊢ isomorphisms C ≤ P.pushouts

Tactic:
intro X Y f (_ : IsIso f)
  obtain ⟨A, B, p, hp, g, _⟩ := h X
  exact ⟨A, B, p, p ≫ g, g ≫ f, hp, (IsPushout.of_id_snd (f := p ≫ g)).of_iso
    (Iso.refl _) (Iso.refl _) (asIso p) (asIso f) (by simp) (by simp) (by simp) (by 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
⊢ P.pushouts ≤ P

Tactic:
by
  rwa [← isStableUnderCobaseChange_iff_pushouts_le]

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
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) ⋯ ⋯)
⊢ pullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅ pullback f g

Tactic:
refine ?_ ≪≫
    pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv (pullback.fst _ _)) (g ≫ inv (pullback.fst _ _)) ≪≫ ?_
  · refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_
    · rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]
    · rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]
    · rw [Category.comp_id, Category.id_comp]
    · ext <;> simp
    · infer_instance
  · refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_
    · rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
    · rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
    · infer_instance

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : CommRingCat} (e : X ≅ Y) (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

pp: case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
· intro X Y Z e f hf
    exact h.right f.hom e.commRingCatIsoToRingEquiv hf

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)