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

Goal state before:
pp: case e'_2.e'_7.e'_4
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ₘ ε.symm.hom) ⊗ₘ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ₘ ε.symm.inv ⊗ₘ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
e_1✝¹ : ((X ⊗ 𝟙_ (LocalizedMonoidal L W ε)) ⊗ Y ⟶ X ⊗ Y) = ((X ⊗ unit) ⊗ Y ⟶ X ⊗ Y)
e_1✝ : L'.obj X' ⊗ L.obj (𝟙_ C) ⊗ L'.obj Y' = L'.obj X' ⊗ L'.obj (𝟙_ C) ⊗ L'.obj Y'
⊢ e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ (λ_ Y).hom =
    L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

Tactic:
exact triangle_aux₂ _ _ _ e₁ e₂

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)

pp: case ha
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.obj a = R

pp: case hb
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.obj c = T

Tactic:
on_goal 1 => rw [p.map_comp]

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map φ ≫ p.map ψ) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)

case ha
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.obj a = R

case hb
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.obj c = T
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)

Tactic:
have : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom := (Iso.app_hom α a) ▸ isHomLift' a

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
this : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ (𝟭 D₂).map (α.app X₁)
eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁

Tactic:
have eq₃ := α.naturality (adj.unit.app X₁)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ (𝟭 D₂).map (α.app X₁)
eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
eq₃ : (L₁ ⋙ G').map (adj.unit.app X₁) ≫ α.app ((G ⋙ F).obj X₁) = α.app ((𝟭 C₁).obj X₁) ≫ (G ⋙ L₂).map (adj.unit.app X₁)
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).obj ≃ (F.obj X).obj ⊕ (F.obj Y).obj :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card (F.obj X).obj + Nat.card (F.obj Y).obj

Tactic:
rw [← Nat.card_sum]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).obj ≃ (F.obj X).obj ⊕ (F.obj Y).obj :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card ((F.obj X).obj ⊕ (F.obj Y).obj)
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
h : (ConcreteCategory.hom i.hom) y = (ConcreteCategory.hom (F.map f)) z
⊢ (fun f ↦ (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f)) y) i =
    (fun f ↦ (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f)) y)
      (u.hom ≫ (functorToAction F).map f)

Tactic:
by simpa [hu]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom
        (F.map
          ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop ((autMulEquivAutGalois F) f))).hom))
      a =
    (ConcreteCategory.hom (f.hom.app A)) a

Tactic:
dsimp [autMulEquivAutGalois, endMulEquivAutGalois]
  rw [endEquivAutGalois_π]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).obj
this : ((toAut F G) g).hom.app X = 𝟙 (F.obj X)
⊢ (ConcreteCategory.hom (𝟙 (F.obj X))) x = x

Tactic:
FintypeCat.id_apply

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).obj
this : ((toAut F G) g).hom.app X = 𝟙 (F.obj X)
⊢ x = x
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
⊢ IsConnected ((TwoSquare.overPost F X).StructuredArrowRightwards g)

Tactic:
by
    let P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
      TwoSquare.StructuredArrowRightwards.mk _ _ (Over.mk (Y := X ⨯ Z) prod.fst)
        (Over.homMk (prod.lift (show W.left ⟶ F.obj X from W.hom) g ≫ inv (prodComparison F X Z))
            (by simp [inv_prodComparison_map_fst])) prod.snd
            (by simp [inv_prodComparison_map_snd])
    have := Nonempty.intro P
    let φ (Q) : Q ⟶ P := StructuredArrow.homMk (CostructuredArrow.homMk
      (Over.homMk (prod.lift Q.right.left.hom Q.right.hom))) (by
        ext
        dsimp
        rw [← cancel_mono (prodComparison F X _)]
        ext
        · simpa [← Functor.map_comp, P] using Over.w Q.hom.left
        · simpa [← Functor.map_comp, P] using CostructuredArrow.w Q.hom)
    exact zigzag_isConnected (fun Q₁ Q₂ ↦ (Zigzag.of_hom (φ Q₁)).trans (Zigzag.of_inv (φ Q₂)))

Goal state after:
Module: Mathlib.CategoryTheory.Join.Sum

Goal state before:
pp: case inl.inl
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
heq : (fromSum C D).map ((Sum.inl_ C D).map f✝¹) = (fromSum C D).map ((Sum.inl_ C D).map f✝)
⊢ (Sum.inl_ C D).map f✝¹ = (Sum.inl_ C D).map f✝

pp: case inr.inr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : D
f✝¹ f✝ : x✝ ⟶ y✝
heq : (fromSum C D).map ((Sum.inr_ C D).map f✝¹) = (fromSum C D).map ((Sum.inr_ C D).map f✝)
⊢ (Sum.inr_ C D).map f✝¹ = (Sum.inr_ C D).map f✝

Tactic:
all_goals
      simp only [fromSum_map_inl, fromSum_map_inr] at heq
      simp [Functor.map_injective _ heq]

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

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).hom ≫
      prod.map (map fun i ↦ f ↑i) (map fun i ↦ f ↑i) ≫
        ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).inv

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv]
  dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]
  cat_disch

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

Goal state before:
pp: case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 + 1 then M i else N i) (m + 1) ≫ eqToHom ⋯ ≫ f (m + 1)

Tactic:
| succ m =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
inst✝ : Small.{w, u'} J
⊢ ObjectProperty.preservesLimit F = (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal

Tactic:
by
  ext
  by_cases hF : HasLimit F
  · rw [preservesLimit_eq_isLocal_single (limit.isLimit F) (colimit.isColimit _)]
    convert Iff.rfl
    ext
    exact ⟨fun ⟨_⟩ ↦ ⟨⟨⟩⟩, fun ⟨_⟩ ↦ ⟨⟨hF⟩⟩⟩
  · exact ⟨fun _ _ _ _ ⟨h⟩ ↦ (hF h.down).elim,
      fun _ ↦ ⟨fun hc ↦ (hF ⟨_, hc⟩).elim⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = 𝟙 (F.obj ((𝟭 C).obj A.A))

Tactic:
← F.map_id

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 ((𝟭 C).obj A.A))
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalCategory C
⊢ ∀ {c c' d d' : C} (f : c ⟶ c') (g : d ⟶ d'), f ⊗ₘ g = f ▷ d ≫ c' ◁ g

Tactic:
by simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalLeftAction C D
x : C
y z : D
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (x ⊙ₗ z)

Tactic:
by
  rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalCategory C
⊢ ∀ {c c' d d' : C} (f : d ⟶ d') (g : c ⟶ c'), f ⊗ₘ g = f ▷ c ≫ d' ◁ g

Tactic:
by simp [tensorHom_def]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalRightAction C D
x : D
y z : C
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (x ⊙ᵣ z)

Tactic:
by
  rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ P.X ◁ Q.actLeft ≫ (α_ R.X P.X Q.X).inv

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ Q.X

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom

Tactic:
rw [associator_inv_naturality_right]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X P.X (S.X ⊗ Q.X)).inv ≫ (R.X ⊗ P.X) ◁ Q.actLeft

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ Q.X

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
G H : C
inst✝⁴ : GrpObj G
inst✝³ : GrpObj H
φ : H ⟶ G
inst✝² : IsMonHom φ
P : C
p : G ⟶ P
inst✝¹ : GrpObj P
inst✝ : IsMonHom p
h : IsPullback φ (toUnit H) p η
⊢ ∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
by
    refine ⟨h.lift (G ◁ φ ≫ conj G) (toUnit _) ?_, ?_⟩
    · simp [conj, comp_mul, inv_comp, mul_comp, h.w, comp_inv, ← Hom.one_def]
    · simp

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| X.X ◁ M.X ◁ f.hom ≫ (α_ X.X M.X N₂.X).inv

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| M.actLeft ▷ N₂.X

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)

Tactic:
rw [associator_inv_naturality_right]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| (α_ X.X M.X N₁.X).inv ≫ (X.X ⊗ M.X) ◁ f.hom

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| M.actLeft ▷ N₂.X

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫
        prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

Tactic:
prodComparison_fst,

Goal state after:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ i.map (fst ((reflector i).obj A) ((reflector i).obj B))
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.comp
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ (fun n ↦ X✝.normalizeObj n) = Z✝.normalizeObj

Tactic:
apply Eq.trans <;> assumption

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * z =
    (Hom.hom (↟(mul' R ↑A)))
      (LinearMap.id ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 ⊗ₜ[R]
        (Hom.hom (↟(mul' R ↑A))) ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).2)

Tactic:
mul'_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * z =
    LinearMap.id ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 *
      (Hom.hom (↟(mul' R ↑A))) ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).2
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : (j : J) → Category.{?u.14, u_2} (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
k l m : Total P
f : k.Hom l
g : l.Hom m
⊢ (P k.fst).ι.app k.snd ≫ D.map f.base ≫ D.map g.base = f.hom ≫ g.hom ≫ (P m.fst).ι.app m.snd

Tactic:
f.w_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : (j : J) → Category.{?u.14, u_2} (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
k l m : Total P
f : k.Hom l
g : l.Hom m
⊢ f.hom ≫ (P l.fst).ι.app l.snd ≫ D.map g.base = f.hom ≫ g.hom ≫ (P m.fst).ι.app m.snd