mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (μ L W ε X₁ Y).inv ≫ L'.map f ▷ L'.obj Y = L'.map (f ▷ Y) ≫ (μ L W ε X₂ Y).inv

Tactic:
by
  simp [Iso.eq_comp_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (μ L W ε X Y₁).inv ≫ L'.obj X ◁ L'.map g = L'.map (X ◁ g) ≫ (μ L W ε X Y₂).inv

Tactic:
by
  simp [Iso.eq_comp_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      (((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃
h₂ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂ ≫
          ((associator L W ε).hom.app Y₁).app Y₂).app
      X₃ =
    (((associator L W ε).hom.app Y₁).app X₂ ≫
          ((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂).app
      X₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
have h₃ := NatTrans.congr_app (NatTrans.congr_app ((associator L W ε).hom.naturality f₁) X₂) X₃

Goal state after:
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₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      (((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃
h₂ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂ ≫
          ((associator L W ε).hom.app Y₁).app Y₂).app
      X₃ =
    (((associator L W ε).hom.app Y₁).app X₂ ≫
          ((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂).app
      X₃
h₃ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).map f₁ ≫ (associator L W ε).hom.app Y₁).app
          X₂).app
      X₃ =
    (((associator L W ε).hom.app X₁ ≫ (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).map f₁).app
          X₂).app
      X₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
suffices Pentagon ((L').obj X₁) ((L').obj X₂) ((L').obj X₃) ((L').obj X₄) by
    dsimp [Pentagon]
    refine Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)
    · rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc,
        ← tensor_comp, ← associator_naturality, id_comp, ← comp_id e₁.hom,
        tensor_comp, ← associator_naturality_assoc, ← comp_id (𝟙 ((L').obj X₄)),
        ← tensor_comp_assoc, associator_naturality, comp_id, comp_id,
        ← tensor_comp_assoc, assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id,
        ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id, id_tensorHom_id, id_tensorHom_id, comp_id]
    · rw [assoc, associator_naturality_assoc, associator_naturality_assoc,
        ← tensor_comp, e₁.inv_hom_id, ← tensor_comp, e₂.inv_hom_id, ← tensor_comp,
        e₃.inv_hom_id, e₄.inv_hom_id, id_tensorHom_id, id_tensorHom_id, id_tensorHom_id, comp_id]

Goal state after:
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
⊢ Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
⊢ ShortComplex.QuasiIso f ↔ ∀ (i : I), ShortComplex.QuasiIso ((F i).mapShortComplex.map f)

Tactic:
refine ⟨fun hf i ↦ inferInstance, fun hf ↦ ?_⟩
  simp only [ShortComplex.quasiIso_iff] at hf ⊢
  rw [hP.isIso_iff]
  exact fun i ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (ShortComplex.homologyFunctorIso (F i))).app
      (Arrow.mk f))).1 (hf i)

Goal state after:
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 : C
inst✝ : IsConnected X
⊢ Nonempty (F.obj X).obj

Tactic:
by_contra h

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
h : ¬Nonempty (F.obj X).obj
⊢ False
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
x : X.obj := (ConcreteCategory.hom i.hom) y
σ : G
hσ : σ • x = x'
⊢ (ConcreteCategory.hom (Y.ρ σ ≫ i.hom)) y = x'

Tactic:
rw [i.comm, FintypeCat.comp_apply]

Goal state after:
case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
x : X.obj := (ConcreteCategory.hom i.hom) y
σ : G
hσ : σ • x = x'
⊢ (ConcreteCategory.hom ((Action.FintypeCat.ofMulAction G X).ρ σ)) ((ConcreteCategory.hom i.hom) y) = x'
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
⊢ IsTerminal (colimit (SingleObj.functor (Aut.toEnd X))) ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)

Tactic:
by
  let J : SingleObj (Aut X) ⥤ C := SingleObj.functor (Aut.toEnd X)
  let e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅ _ :=
    preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫
    (Equiv.toIso <| SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl))
  apply Equiv.trans
  · apply (IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
      (isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)
  exact Types.isTerminalEquivUnique _

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
⊢ σ t = σ s → t = s

Tactic:
(hs : F.map (selfProdProj u t) b = F.map (selfProdProj u s) b)

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
⊢ t = s
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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
h : IsIso (𝟙 ((functorToAction F).obj X))
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
simpa [i, u]

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
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := (e X).symm x
hx' : x' = (e X).symm x
y' : (F'.obj X).obj := (e X).symm y
hy' : y' = (e X).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
g : F ≅ F := NatIso.ofComponents gapp ⋯
⊢ (ConcreteCategory.hom (gapp X).hom) x = y

Tactic:
simp [gapp, ← hx', hg', hy', Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
V : Type u_1
inst✝¹ : Quiver V
inst✝ : Nonempty V
⊢ Nonempty (Quiver.FreeGroupoid V)

Tactic:
inhabit V; exact ⟨⟨@default V _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ of V ⋙q (lift φ).toPrefunctor = φ

Tactic:
by
  rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]
  dsimp [lift]
  rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ i₁ + i₃ + i₂ = k

Tactic:
by rw [add_assoc, add_comm i₃, ← add_assoc, h]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' b b' : C
f : b ⟶ b'
hb : φ.obj b = φ.obj c
hb' : φ.obj b' = φ.obj c'
⊢ Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb' ∈
    (map φ hφ S).arrows (φ.obj c') (φ.obj c')

Tactic:
cases hφ hb

Goal state after:
case refl.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' b' : C
hb' : φ.obj b' = φ.obj c'
f : c ⟶ b'
hb : φ.obj c = φ.obj c
⊢ Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb' ∈
    (map φ hφ S).arrows (φ.obj c') (φ.obj c')
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect ≤ S

Tactic:
rw [le_iff]

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ⊆ E
⊢ full D ≤ full E

Tactic:
rw [le_iff]

Goal state after:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ⊆ E
⊢ ∀ {c d : C}, (full D).arrows c d ⊆ (full E).arrows c d
Module: Mathlib.CategoryTheory.Join.Basic

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
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
Fₗ Gₗ : C ⥤ E
α : Fₗ ≅ Gₗ
H : D ⥤ E'
x : C ⋆ D
⊢ (mapIsoWhiskerRight α H).inv.app x = (mapWhiskerRight α.inv H).app x

Tactic:
cases x <;> simp [mapIsoWhiskerRight]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p

Tactic:
← w₃,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p₃ ≫ f₃
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = g₃

Tactic:
← w₃,

Goal state after:
case refine_3
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = φ₂₃ ≫ h₂₃.p₂
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case isTrue
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 < n
⊢ Pi.π M m ≫ eqToHom ⋯ = Pi.π M m ≫ (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫ eqToHom ⋯

pp: case isFalse
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 < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
· simp [dif_pos (by lia : m < n + 1)]

Goal state after:
case isFalse
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 < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯
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ᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom ((F ⋙ P).map g)) ((fun j ↦ shrinkYonedaEquiv (c'.ι.app (op j) ≫ f)) X) =
    (fun j ↦ shrinkYonedaEquiv (c'.ι.app (op j) ≫ f)) X'

Tactic:
by
        dsimp
        rw [← dsimp% c'.w g.op, Category.assoc]
        conv_rhs => rw [shrinkYonedaEquiv_comp]
        rw [shrinkYonedaEquiv_shrinkYoneda_map]
        apply map_shrinkYonedaEquiv

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
t t' : Cone F
l : IsLimit t
l' : IsWeakLimit t'
x✝ : J
⊢ (l'.lift t ≫ l.lift t') ≫ t.π.app x✝ = 𝟙 t.pt ≫ t.π.app x✝

Tactic:
rw [assoc, id_comp, l.fac t', l'.fac t]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case none
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
⊢ ((Pi.optionEquivalence C).symm.functor ⋙ Functor.pi L) ⋙ Pi.eval D none ≅
    (L₁ ⋙ (Pi.optionEquivalence D).symm.functor) ⋙ Pi.eval D none

Tactic:
apply Iso.refl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case some
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
i : J
⊢ ((Pi.optionEquivalence C).symm.functor ⋙ Functor.pi L) ⋙ Pi.eval D (some i) ≅
    (L₁ ⋙ (Pi.optionEquivalence D).symm.functor) ⋙ Pi.eval D (some i)

Tactic:
apply Iso.refl

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
⊢ x ⊴ₗ f.inv ≫ x ⊴ₗ f.hom = 𝟙 (x ⊙ₗ z)

Tactic:
by
  rw [← actionHomRight_comp, Iso.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
inst✝ : MonoidalRightAction C D
x : D
y z : C
f : y ≅ z
⊢ x ⊴ᵣ f.inv ≫ x ⊴ᵣ f.hom = 𝟙 (x ⊙ᵣ z)

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

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
B : Subterminals C
A Z : C
g h : Z ⟶ A ⟹ B.obj
⊢ g = h

Tactic:
exact uncurry_injective (B.2 (MonoidalClosed.uncurry g) (MonoidalClosed.uncurry h))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
⊢ (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).IsPointwiseLeftKanExtensionAt (d, e)

Tactic:
set cone := Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K) |>.coconeAt (d, e)

Goal state after:
V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
⊢ (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).IsPointwiseLeftKanExtensionAt (d, e)