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

Goal state before:
pp: case star.star
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) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
f : star ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f

Goal state after:
case star.star.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) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
⊢ G.map PUnit.unit ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map PUnit.unit
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
y : J
f : widePullbackShapeEquivObj none ⟶ widePullbackShapeEquivObj (some y)
⊢ none ⟶ some y

Tactic:
cases f

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
y : J
f : widePullbackShapeEquivObj none ⟶ widePullbackShapeEquivObj (some y)
⊢ (fun x ↦
        match some y, none, x with
        | .(none), .(some j), Hom.term j => PUnit.unit
        | y, .(y), Hom.id .(y) => 𝟙 (widePullbackShapeEquivObj y))
      ((fun f ↦
          match none, some y, f with
          | some x, some y, f => cast ⋯ (Hom.id (some y))
          | none, some y, f => PEmpty.casesOn (fun t ↦ f = t → (none ⟶ some y)) f ⋯
          | some x, none, f => Hom.term x
          | none, none, f => Hom.id none)
        f) =
    f

Tactic:
cases f

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.Final
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasColimit G
⊢ IsIso (colimit.pre G F)

Tactic:
by
  simp only [colimit.pre_eq (colimitCoconeComp F (getColimitCocone G)) (getColimitCocone G),
    colimitCoconeComp_cocone, IsColimit.desc_self]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case zero.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero
⊢ (parallelPair f✝.op g.op).map f ≫
      (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f✝ g).op).map f

Tactic:
cases f

Goal state after:
case zero.zero.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case zero.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ (parallelPair f✝.op g.op).map f ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f✝ g).op).map f

Tactic:
cases f

Goal state after:
case zero.one.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map WalkingParallelPairHom.left ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map WalkingParallelPairHom.left

case zero.one.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map WalkingParallelPairHom.right ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map WalkingParallelPairHom.right
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case one.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ (parallelPair f✝.op g.op).map f ≫
      (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case one.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ (parallelPair f✝.op g.op).map f ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f✝.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f✝ g).op).map f

Tactic:
cases f

Goal state after:
case one.one.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.one)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of.star
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
X : C
f : of X ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match of X with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f

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

Goal state before:
pp: case star.of
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
f : star ⟶ of Y
⊢ G.map f ≫
      (match of Y with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f

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
⊢ G.map PUnit.unit ≫
      (match of Y with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map PUnit.unit
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star.star
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
f : star ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f

Goal state after:
case star.star.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
⊢ G.map PUnit.unit ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map PUnit.unit
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
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))
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₂
⊢ P U

Tactic:
exact ⟨Z, h.right ≫ q₁, q₂, by simp only [F.map_comp, StructuredArrow.w_assoc, hq]⟩

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f.right T)

Tactic:
exact Final.out f.right

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₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
by
  rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsLimit
    (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)))
          (fun i ↦
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)) ≫
              (limit.cone (Discrete.functor fun i ↦ f i.succ)).π.app { as := i })
          j))

Tactic:
let :=
      extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F _)
        (isLimitOfHasBinaryProductOfPreservesLimit F _ _)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i ↦ F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i ↦ f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i ↦ f i.succ))
⊢ IsLimit
    (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)))
          (fun i ↦
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)) ≫
              (limit.cone (Discrete.functor fun i ↦ f i.succ)).π.app { as := i })
          j))
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
let α := Σ (X : Subtype Q), { p : X.1 ⟶ X.1 // p ≫ p = p }

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
⊢ P g

Tactic:
have : g = gr ≫ pullback.snd _ _ := by simp [gr]

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P g
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
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ PreservesLimit (pair A B) F

Tactic:
apply preservesLimit_of_preserves_limit_cone (tensorProductIsBinaryProduct A B)

Goal state after:
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
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ IsLimit (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
⊢ LinearMap.mul' S (B ⊗[R] A) ∘ₗ
      LinearMap.rTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul =
    Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit

Tactic:
by
    ext x y
    convert! congr($(mul_antipode_rTensor_comul_apply (R := S) x) ⊗ₜ[R]
      $(mul_antipode_rTensor_comul_apply (R := R) y)) using 1
    · dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      simp
    · dsimp [Algebra.TensorProduct.one_def]
      simp [Algebra.algebraMap_eq_smul_one, smul_tmul']

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 A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
have := left_inv A =≫ f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : (lift ι (𝟙 A) ≫ μ) ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = curry ((ihom.ev A).app Y ≫ g)

Tactic:
curry_natural_right,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = curry ((ihom.ev A).app Y) ≫ (ihom A).map g
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = ⊗𝟙.hom

Tactic:
convert! evaluation_coevaluation X Y

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = η_ X Y ▷ X ≫ (α_ X Y X).hom ≫ X ◁ ε_ X Y

case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢  ⊗𝟙.hom = (λ_ X).hom ≫ (ρ_ X).inv
Module: Mathlib.SetTheory.Cardinal.Subfield

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

Tactic:
change ↑a ∈ map (closure s).subtype _

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

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ (b.toDual m) (b i) = (b.toDual ((Finsupp.linearCombination R ⇑b) (b.repr m))) (b i)

Tactic:
b.linearCombination_repr

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ (b.toDual m) (b i) = (b.toDual m) (b i)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
m : M
⊢ (b.toDual (b i)) m = (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) (b.repr m))

Tactic:
b.linearCombination_repr

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
m : M
⊢ (b.toDual (b i)) m = (b.toDual (b i)) m
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ ((b.dualBasis.toDual ∘ₗ b.toDual) (b i)) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ (b.dualBasis.toDual (b.toDual (b i))) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ Injective ⇑L

Tactic:
rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]

Goal state after: