mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (Cocycle.fromSingleMk (-f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))

Tactic:
rw [Cocycle.fromSingleMk_neg _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (NatTrans.rightDerivedToHomotopyCategory α).app X =
    (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
← cancel_mono (P.isoRightDerivedToHomotopyCategoryObj G).hom,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (NatTrans.rightDerivedToHomotopyCategory α).app X ≫ (P.isoRightDerivedToHomotopyCategoryObj G).hom =
    ((P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
          (P.isoRightDerivedToHomotopyCategoryObj G).inv) ≫
      (P.isoRightDerivedToHomotopyCategoryObj G).hom
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ ((Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯).hom = (R'.extMk (φ.hom.f n ≫ f) m hm ⋯).hom

Tactic:
have : (R'.cochainComplexXIso (-n) n (by lia)).hom ≫ φ.hom.f n =
      φ.hom'.f (-n) ≫ (R.cochainComplexXIso (-n) n (by lia)).hom := by
    simp [φ.hom'_f _ _ rfl]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ ((Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯).hom = (R'.extMk (φ.hom.f n ≫ f) m hm ⋯).hom
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
X✝ Y✝ Z✝ : SingleObj M
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : X
⊢ (ConcreteCategory.hom (↾fun x ↦ f ≫ g • x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x)).toFun x

Tactic:
exact (smul_smul g f x).symm

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ ε F = ε F ≫ F.map (𝟙 (𝟙_ V))

Tactic:
F.map_id,

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ ε F = ε F ≫ 𝟙 (F.obj (𝟙_ V))
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
⊢ Function.RightInverse (fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) fun f ↦
    { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ }

Tactic:
by
            intro f
            ext x
            dsimp
            ext g
            simp only [NatTrans.naturality_assoc,
              evaluationRightAdjoint_obj_obj, evaluationRightAdjoint_obj_map, limit.lift_π,
              Fan.mk_pt, Fan.mk_π_app, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X)) (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.leftToRight.app (G.obj X)

Tactic:
homEquiv_apply,

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) = t.leftToRight.app (G.obj X)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ≫ θ.naturality (f ≫ g)) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
by
      rw [naturality_comp θ]
      bicategory

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    (F.map f ≫
        match Y with
        | ⟨j, X⟩ => (h j).app X) =
      (match X with
        | ⟨j, X⟩ => (h j).app X) ≫
        G.map f

Tactic:
rintro ⟨j, X⟩ ⟨_, _⟩ ⟨f⟩

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
j : I
X Y✝ : C j
f : X ⟶ Y✝
⊢ (F.map (SigmaHom.mk f) ≫
      match ⟨j, Y✝⟩ with
      | ⟨j, X⟩ => (h j).app X) =
    (match ⟨j, X⟩ with
      | ⟨j, X⟩ => (h j).app X) ≫
      G.map (SigmaHom.mk f)
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

Tactic:
injection Part.mem_unique ⟨h₁, h₂⟩ h'

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
⊢ b ∈ f.fix a'

Tactic:
obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h <;> cases Part.mem_unique ha' h'

Goal state after:
case mp.inr.refl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'
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₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
dsimp [Pentagon]

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₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ▷ X ≫ (∂R X Y Z).inv = coprod.inl

Tactic:
by
  apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp
  rw [assoc, Iso.inv_hom_id, comp_id, coprod_inl_rightDistrib_hom]

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

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : A ⊕ B
f : x ⟶ y
⊢ F.map f ≫
      (match y with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match x with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map f

Tactic:
by
      cases f
      · simpa using! e₁.hom.naturality _
      · simpa using! e₂.hom.naturality _

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

Goal state before:
pp: case refine_1
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₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    ((α_ Y₁ Y₂ Y₃).hom ≫ (e₁.inv ≫ e₁.hom ⊗ₘ (e₂.inv ⊗ₘ e₃.inv) ≫ (e₂.hom ⊗ₘ e₃.hom)) ⊗ₘ 𝟙 Y₄) ≫
      (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)

Tactic:
e₁.inv_hom_id,

Goal state after:
case refine_1
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₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    ((α_ Y₁ Y₂ Y₃).hom ≫ (𝟙 Y₁ ⊗ₘ (e₂.inv ⊗ₘ e₃.inv) ≫ (e₂.hom ⊗ₘ e₃.hom)) ⊗ₘ 𝟙 Y₄) ≫
      (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_2
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₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫
      (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom ≫ (e₁.inv ≫ e₁.hom ⊗ₘ (e₂.inv ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫ (e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom

Tactic:
e₁.inv_hom_id,

Goal state after:
case refine_2
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₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫
      (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom ≫ (𝟙 Y₁ ⊗ₘ (e₂.inv ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫ (e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom
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 (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)

Tactic:
dsimp [Pentagon]

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₄
⊢ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁ comp (Opposite.unop x✝¹) (Opposite.unop x✝²) (Opposite.unop x✝³) ≫
            comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)

Tactic:
← EnrichedCategory.assoc

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (α_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
                (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³)).inv ≫
            (comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ▷
                Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ≫
              comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : 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.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ = τ

Tactic:
use map p (f ≫ g) (φ ≫ ψ) (f' := h ≫ f ≫ g) rfl (τ ≫ ψ)

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.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)) ∧
    ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : 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.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
⊢ ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
by
    intro a' h τ hτ
    have h₁ : IsHomLift p (h ≫ f ≫ g) (τ ≫ ψ) := by simpa using IsHomLift.comp p (h ≫ f) _ τ ψ
    /- We get a morphism `π : a' ⟶ a` such that `π ≫ φ ≫ ψ = τ ≫ ψ` from the universal property
    of `φ ≫ ψ`. This will be the morphism induced by `φ`. -/
    use map p (f ≫ g) (φ ≫ ψ) (f' := h ≫ f ≫ g) rfl (τ ≫ ψ)
    refine ⟨⟨inferInstance, ?_⟩, ?_⟩
    /- The fact that `π ≫ φ = τ` follows from `π ≫ φ ≫ ψ = τ ≫ ψ` and the universal property of
    `ψ`. -/
    · apply IsStronglyCartesian.ext p g ψ (h ≫ f) (by simp)
    -- Finally, the uniqueness of `π` comes from the universal property of `φ ≫ ψ`.
    · intro π' ⟨hπ'₁, hπ'₂⟩
      apply map_uniq
      simp [hπ'₂.symm]

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 A : C
inst✝¹ : Nonempty (F.obj X).obj
inst✝ : IsConnected A
f : X ⟶ A
⊢ Function.Surjective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
have : Epi f := epi_of_nonempty_of_isConnected F f
  exact surjective_on_fiber_of_epi F f

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := ⋯
a : (F.obj A).obj
τ : Aut B
hτ : f ≫ τ.hom = σ.hom ≫ f
⊢ (fun f_1 ↦ (ConcreteCategory.hom (F.map f_1.hom)) ((ConcreteCategory.hom (F.map f)) a)) τ =
    (fun f_1 ↦ (ConcreteCategory.hom (F.map f_1.hom)) ((ConcreteCategory.hom (F.map f)) a))
      ((evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
        ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a))

Tactic:
simpa using ConcreteCategory.congr_hom (F.congr_map hτ) a

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
m : s.pt ⟶ (mk bc.pt (c₁.combPairHoms c₂ bc)).pt
hm : ∀ (j : ι₁ ⊕ ι₂), m ≫ (mk bc.pt (c₁.combPairHoms c₂ bc)).proj j = s.proj j
w : WalkingPair
⊢ m ≫ proj bc w =
    (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      proj bc w

Tactic:
by
      cases w
      · refine Fan.IsLimit.hom_ext h₁ _ _ (fun a ↦ by aesop)
      · refine Fan.IsLimit.hom_ext h₂ _ _ (fun a ↦ by aesop)

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

Goal state before:
pp: case neg
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ¬∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
· simp only [not_forall, not_false_eq_true] at nhi
    obtain ⟨hi⟩ := nhi
    exact has_decomp_connected_components_aux_initial X hi

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

Goal state before:
pp: case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
refine ⟨evaluation_injective_of_isConnected F A X a, ?_⟩

Goal state after:
case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Surjective fun f ↦ (ConcreteCategory.hom (F.map f)) a