mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
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)
⊢ (comonadToFunctor C).mapIso (ComonadIso.mk f f_ε f_δ) = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: case e_a
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
⊢ (↑b * ↑b') • g a = ↑b • b' • g a

Tactic:
rw [mul_smul, Submonoid.smul_def]

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
⊢ ∃ b, r * b = 1

Tactic:
have map_inv {j k : J} (f : j ⟶ k) : F.map f (inv j) = inv k := by
    have h := congr(F.map f $(h_inv j))
    have : F.map f (c.π.app j r) = c.π.app k r :=
      DFunLike.congr_fun (congr(Hom.hom $(c.w f))) r
    rw [map_mul, map_one, this] at h
    rw [← mul_one (F.map f (inv j)), ← h_inv k, ← mul_assoc]
    nth_rw 2 [mul_comm]; rw [h, one_mul]

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
⊢ ∃ b, r * b = 1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case h
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) (r * (ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    (ConcreteCategory.hom (c.π.app j)) 1

Tactic:
rw [RingHom.map_mul, RingHom.map_one]

Goal state after:
case h
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
⊢ ↑((ConcreteCategory.hom m) x) = ((Hom.hom s.fst) x, (Hom.hom s.snd) x)

Tactic:
have eq1 := (congr_arg (fun f : s.pt →+* A => f x) (congrArg Hom.hom e₁) :)

Goal state after:
case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
⊢ ↑((ConcreteCategory.hom m) x) = ((Hom.hom s.fst) x, (Hom.hom s.snd) x)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom)

pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h)

pp: case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f ≫ F.map g) (F.map h)

Tactic:
G.map₂_comp

Goal state after:
case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)

case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h)

case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f ≫ F.map g) (F.map h)
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✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (asIso (F.mapComp f g)).hom ≫ F.map f ◁ F.map₂ η ≫ (asIso (F.mapComp f h)).inv

Tactic:
by
    dsimp
    rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]

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

Goal state before:
pp: case e_a.w_base
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)
⊢ { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }.base =
    (({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
        { base := eqToHom ⋯, fiber := eqToHom ⋯ }).base

Tactic:
simp only [eqToHom_refl, Category.assoc, Grothendieck.comp_base,
        Category.comp_id]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ → G.map k₁ ≫ c.ι.app X₁ = G.map f ≫ c.ι.app Y → G.map k₂ ≫ c.ι.app X₂ = G.map f ≫ c.ι.app Y

Tactic:
intro _ _ _ _ _ h₁ h₂
    simp [← h₁, ← Functor.comp_map, c.ι.naturality, h₂]

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
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
a : C
x✝ : of a ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.left.app x
      | star => φ.right) =
    (match of a with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x✝

Tactic:
simp; simpa [-CommaMorphism.w] using (congrArg (fun f ↦ f.app a) φ.w).symm

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
x : WithTerminal C ⥤ D
⊢ mkCommaMorphism
      (NatIso.ofComponents
          (fun X ↦
            match X with
            | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
            | star => Iso.refl (x.obj star))
          ⋯).hom =
    𝟙 (mkCommaObject x)

Tactic:
ext <;> rfl

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

Goal state before:
pp: case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ h.hom.app Y

Tactic:
← Iso.eq_inv_comp,

Goal state after:
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ (lift F M hM).map PUnit.unit = hG.inv ≫ G.map PUnit.unit ≫ h.hom.app Y
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
x : WithInitial C ⥤ D
⊢ mkCommaMorphism
      (NatIso.ofComponents
          (fun X ↦
            match X with
            | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
            | star => Iso.refl (x.obj star))
          ⋯).hom =
    𝟙 (mkCommaObject x)

Tactic:
ext <;> rfl

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

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

Tactic:
← Iso.eq_inv_comp,

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : 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₂
⊢ ((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)) ≫
        i₁) ≫
      snd f 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)) ≫
        i₂) ≫
      snd f i

Tactic:
· simp only [Category.assoc, condition]

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
n : ℕ
⊢ (fun x ↦ r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
use n

Goal state after:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := ⋯
e₂ : Localization.Away (f r) ≃+* S' := ⋯
n : ℕ
⊢ (fun x ↦ f r ^ x) n = f ((fun x ↦ r ^ x) n)
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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } })

Tactic:
exact ⟨_, _, _, _, h₁', _, _, hf⟩

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape J ≤ (P.strictLimitsOfShape J).isoClosure

Tactic:
intro X ⟨h⟩

Goal state after:
case refine_2
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.LimitOfShape J X
⊢ (P.strictLimitsOfShape J).isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
Q : ObjectProperty C
hPQ : P ≤ Q
⊢ P.limitsOfShape J ≤ Q.limitsOfShape J

Tactic:
intro X ⟨h⟩

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
Q : ObjectProperty C
hPQ : P ≤ Q
X : C
h : P.LimitOfShape J X
⊢ Q.limitsOfShape J X
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.isoClosure.limitsOfShape J ≤ P.limitsOfShape J

Tactic:
intro X ⟨h⟩

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
X : C
h : P.isoClosure.LimitOfShape J X
⊢ P.limitsOfShape J X
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P.retractClosure ≤ P

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P ≤ P.retractClosure

Tactic:
· intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_retract P e hY

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P ≤ P.retractClosure
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
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)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m =
    c₂.inr ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }))

Tactic:
rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.2]

Goal state after:
case h₂
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)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape J ≤ (P.strictColimitsOfShape J).isoClosure

Tactic:
intro X ⟨h⟩

Goal state after:
case refine_2
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.ColimitOfShape J X
⊢ (P.strictColimitsOfShape J).isoClosure 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
Q : ObjectProperty C
hPQ : P ≤ Q
⊢ P.colimitsOfShape J ≤ Q.colimitsOfShape J

Tactic:
intro X ⟨h⟩

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
Q : ObjectProperty C
hPQ : P ≤ Q
X : C
h : P.ColimitOfShape J X
⊢ Q.colimitsOfShape J 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
⊢ P.isoClosure.colimitsOfShape J ≤ P.colimitsOfShape J

Tactic:
intro X ⟨h⟩

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
X : C
h : P.isoClosure.ColimitOfShape J X
⊢ P.colimitsOfShape J X
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z X Y : C
f : X ⟶ Y
inst✝¹ : HasPushout f f
inst✝ : Epi f
⊢ IsIso (codiagonal f)

Tactic:
rw [(IsIso.inv_eq_of_hom_inv_id (inl_codiagonal f)).symm]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
⊢ (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
      (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)) =
    (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
⊢ (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
      (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)) =
    (Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ ((↑(assoc R R R ↑T ↑U ↑S)).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
      ↑(assoc R R R ↑S ↑T ↑U) =
    ((Algebra.TensorProduct.map (AlgHom.id R ↑T) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
          ↑(assoc R R R ↑T ↑S ↑U)).comp
      (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom) (AlgHom.id R ↑U))

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ ((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
      ↑(assoc R R R ↑S ↑T ↑U).symm =
    ((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
          ↑(assoc R R R ↑S ↑U ↑T).symm).comp
      (Algebra.TensorProduct.map (AlgHom.id R ↑S) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ (antipode R) (a * b) = (antipode R) b * (antipode R) a

Tactic:
by
  exact congr($antipode_comp_mul_comp_comm (b ⊗ₜ a))

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

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
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝³ : F.Monoidal
inst✝² : F'.Monoidal
inst✝¹ : G.Monoidal
hF : F.FullyFaithful
X : C
inst✝ : GrpObj (F.obj X)
⊢ F.map (lift (hF.preimage ι) (𝟙 X) ≫ μ) = F.map (toUnit X ≫ η)

Tactic:
by
    simp [OplaxMonoidal.η_of_cartesianMonoidalCategory]

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

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
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝³ : F.Monoidal
inst✝² : F'.Monoidal
inst✝¹ : G.Monoidal
hF : F.FullyFaithful
X : C
inst✝ : GrpObj (F.obj X)
⊢ F.map (lift (𝟙 X) (hF.preimage ι) ≫ μ) = F.map (toUnit X ≫ η)

Tactic:
by
    simp [OplaxMonoidal.η_of_cartesianMonoidalCategory]

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ ?m.139 ^ 0 ≤ m ^ lift.{u, v} #(β a)

pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := ⋯
a : α
⊢ Cardinal.{max u v}

Tactic:
exact
                    power_le_power_left
                      (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) zero_le

Goal state after: