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
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'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), a * 0 = 0

Tactic:
with_unfolding_all
      rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩

Goal state after:
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'
x✝¹ : R
x✝ : M
⊢ mk (x✝¹ • x✝) 1 = (RingHom.id R) x✝¹ • mk x✝ 1

Tactic:
simp [mk, OreLocalization.smul_oreDiv]

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_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g

Tactic:
LocalizedModule.lift_comp S g h

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''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ g = g
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''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ j = k

Tactic:
by
  rw [← lift_unique S f (k.comp f) map_unit j h, lift_unique]
  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✝
⊢ G.map₂ (F.map₂ (λ_ f).hom) =
    (G.map₂ (F.mapComp (𝟙 a✝) f) ≫ G.mapComp (F.map (𝟙 a✝)) (F.map f)) ≫
      (G.map₂ (F.mapId a✝) ≫ G.mapId (F.obj a✝)) ▷ G.map (F.map f) ≫ (λ_ (G.map (F.map f))).hom

Tactic:
simp only [map₂_leftUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_left_assoc,
      comp_whiskerRight, assoc]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ∃ J x, Nonempty (P.FullSubcategory ≌ J)
J : Type w
w✝ : Category.{w', w} J
e : P.FullSubcategory ≌ J
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
exact ⟨.ofObj (e.inverse ⋙ P.ι).obj, inferInstance,
      fun X hX ↦ ⟨_, ⟨⟨(e.functor.obj ⟨X, hX⟩)⟩, ⟨P.ι.mapIso (e.unitIso.app ⟨X, hX⟩)⟩⟩⟩⟩

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✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ yoneda.map (↑f.unop).unop ≫ (CostructuredArrow.mk (yonedaEquiv.symm (unop Y✝).snd)).hom =
    (CostructuredArrow.mk (yonedaEquiv.symm (unop X✝).snd)).hom

Tactic:
ext Z y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
Z : Cᵒᵖ
y : (yoneda.obj (CostructuredArrow.mk (yonedaEquiv.symm (unop X✝).snd)).left).obj Z
⊢ (ConcreteCategory.hom
          ((yoneda.map (↑f.unop).unop ≫ (CostructuredArrow.mk (yonedaEquiv.symm (unop Y✝).snd)).hom).app Z)).toFun
      y =
    (ConcreteCategory.hom ((CostructuredArrow.mk (yonedaEquiv.symm (unop X✝).snd)).hom.app Z)).toFun y
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 G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : (coconeFiberwiseColimitOfCocone c).pt ⟶ s.pt
hm : ∀ (j : C), (coconeFiberwiseColimitOfCocone c).ι.app j ≫ m = s.ι.app j
X : Grothendieck F
this : colimit.desc (Grothendieck.ι F X.base ⋙ G) (Cocone.whisker (Grothendieck.ι F X.base) c) ≫ m = s.ι.app X.base
⊢ c.ι.app X ≫ m = colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ s.ι.app X.base

Tactic:
simp [← this]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)

Tactic:
have eq : x = y := PLift.down (ULift.down (down f))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
eq : x = y
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ y✝ : (WithTerminal C)ᵒᵖ
f✝ : unop y✝ ⟶ unop x✝¹
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x✝ : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithTerminal C)ᵒᵖ).map (op f) ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithInitial.of (op x)
                  | star => WithInitial.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (down f).op
                  | op star, op (of a), x, x_2 =>
                    WithInitial.starInitial.to
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
                | WithInitial.star, WithInitial.of (op unop), x =>
                  op
                    (starTerminal.from
                      (Opposite.unop
                        (match WithInitial.of (op unop) with
                        | WithInitial.of x => op (of (Opposite.unop x))
                        | WithInitial.star => op star)))
                | WithInitial.star, WithInitial.star, x =>
                  𝟙
                    (match WithInitial.star with
                    | WithInitial.of x => op (of (unop x))
                    | WithInitial.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        (op f)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝¹ y✝ : (WithTerminal C)ᵒᵖ
f✝ : unop y✝ ⟶ unop x✝¹
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x✝ : op (of x) ⟶ op (of y)
⊢ op f = WithInitial.down (down f).op
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ y✝ : (WithInitial C)ᵒᵖ
f✝ : x✝ ⟶ y✝
x y : C
f : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithInitial C)ᵒᵖ).map f ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                  | op (of a), op star, x, x_2 =>
                    WithTerminal.starTerminal.from
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                | WithTerminal.of (op unop), WithTerminal.star, x =>
                  op
                    (starInitial.to
                      (Opposite.unop
                        (match WithTerminal.of (op unop) with
                        | WithTerminal.of x => op (of (Opposite.unop x))
                        | WithTerminal.star => op star)))
                | WithTerminal.star, WithTerminal.star, x =>
                  𝟙
                    (match WithTerminal.star with
                    | WithTerminal.of x => op (of (unop x))
                    | WithTerminal.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝ y✝ : (WithInitial C)ᵒᵖ
f✝ : x✝ ⟶ y✝
x y : C
f : op (of x) ⟶ op (of y)
⊢ f =
    down
      (match f with
      | op f => (WithTerminal.down f).op)
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₂
Z : C
q₁ : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ IsFiltered.coeqHom q₁ q₂) =
    g ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂)

Tactic:
simp only [F.map_comp, ← reassoc_of% h, StructuredArrow.mk_hom_eq_self, Category.assoc]

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

Goal state before:
pp: case refine_1
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))
⊢ ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₁ → P j₂

pp: case refine_2
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))
⊢ ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₂ → P j₁

Tactic:
· rintro U V h ⟨Z, q₁, q₂, hq⟩
      obtain ⟨W, q₃, q₄, hq'⟩ := IsFiltered.span q₁ h.right
      refine ⟨W, q₄, q₂ ≫ q₃, ?_⟩
      rw [F.map_comp, ← reassoc_of% hq, ← F.map_comp, hq', F.map_comp, StructuredArrow.w_assoc]

Goal state after:
case refine_2
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))
⊢ ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₂ → P j₁
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
⊢ IsLimit (c.overPost j)

Tactic:
haveI : Nonempty (Over j) := ⟨Over.mk (𝟙 j)⟩

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
⊢ IsLimit (c.overPost j)
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
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
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
erw [← Category.assoc, ← eq_whisker comm]

Goal state after:
case h₁
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
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p
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 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).hom ≫ fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)

Tactic:
by
  delta pullbackDiagonalMapIdIso
  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 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).hom ≫ snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)

Tactic:
by
  delta pullbackDiagonalMapIdIso
  simp

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)

Tactic:
intro X Y Z e f hf

Goal state after:
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
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
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)

Tactic:
intro X Y Z e f 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
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
              (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
            lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯)
              ⋯) ≫
          snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
        fst (snd f' g') i₂) ≫
      fst f' g' =
    ((𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
        fst (snd f' g') i₂) ≫
      fst f' g'

Tactic:
simp only [Category.assoc, lift_snd_assoc, lift_fst_assoc, lift_fst, Category.id_comp]

Goal state after:
case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂ ≫ fst f' g'
Module: Mathlib.CategoryTheory.Limits.FullSubcategory

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : HasLimitsOfShape J C
inst✝² : PreservesLimitsOfShape J F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.essImage.strictLimitsOfShape J ≤ F.essImage

Tactic:
rintro _ ⟨G, hG⟩
    exact ⟨limit (Functor.essImage.liftFunctor G F hG),
      ⟨IsLimit.conePointsIsoOfNatIso
        (isLimitOfPreserves F (limit.isLimit _)) (limit.isLimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

Goal state after:
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
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictColimitsOfShape J ≤ P
⊢ P.colimitsOfShape J ≤ P.isoClosure

Tactic:
rw [← isoClosure_strictColimitsOfShape]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictColimitsOfShape J ≤ P
⊢ (P.strictColimitsOfShape J).isoClosure ≤ P.isoClosure
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₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom ℬ (tensorHom ℬ f₁ f₂) f₃ ≫ (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
    (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫ tensorHom ℬ f₁ (tensorHom ℬ f₂ f₃)

Tactic:
by
  dsimp [tensorHom]
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩ <;> simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift (f ≫ ι) g ≫ μ = h ↔ g = lift f h ≫ μ

Tactic:
by
  rw [eq_comm, eq_lift_inv_left, eq_comm]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ a ∈ rangeOfWType s

Tactic:
← SetLike.mem_coe,

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ a ∈ ↑(rangeOfWType s)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #↑(s ∪ sec '' t) = Module.rank R M

Tactic:
Cardinal.mk_union_of_disjoint hst,

Goal state after:
case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #↑s + #↑(sec '' t) = Module.rank R M