mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.π'))).comp
      (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯)
      ⋯

Tactic:
congr

Goal state after:
case e_g
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q =
    (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
      (ShiftedHom.mk₀ 0 ⋯ (𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ P.isoModSerre f ↔ P.epiModSerre f

Tactic:
have := P.monoModSerre_of_mono f
  rw [isoModSerre_iff]
  tauto

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

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt

Tactic:
· exact P.prop_kernel f.hom X.property Y.property

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

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (a : R) (x y : X ⟶ Y), a • (x + y) = a • x + a • y

Tactic:
intros; ext; exact smul_add _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: case refine_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ (h X).left = s.ι ≫ (h X).right

Tactic:
rw [← cancel_mono (adj₁.unit.app ((h X).Z)), assoc, ← adj₁.unit_naturality (h _).left]

Goal state after:
case refine_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: case mp
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
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₁.unit
idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
⊢ IsIso t.adj₂.counit

Tactic:
exact t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq 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₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))

Tactic:
congr

Goal state after:
case e_a
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
⊢ G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X) = inv (t.adj₁.unit.app (G.obj X))
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ F.map f ◁ η.app b ◁ Γ.as.app b

Tactic:
by
      dsimp only [comp_app, comp_naturality]
      calc
        _ = 𝟙 _ ⊗≫ η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫
                η.naturality f ▷ ι.app b ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality f ⊗≫ ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫
              η.naturality f ▷ ι.app b) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ ⟨fun a ↦ p a, asSubtype fun x ↦ { Dom := p x, get := fun h ↦ f ⟨x, h⟩ }⟩ = ⟨p, f⟩

Tactic:
congr

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hbase a fa

Tactic:
unfold fixInduction'

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih ↦
      Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e ↦
          have e := ⋯;
          hbase a' ⋯)
        (fun a'' e ↦
          have e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hbase a fa
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hind a a' h' fa (fixInduction' h' hbase hind)

Tactic:
unfold fixInduction'

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih ↦
      Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e ↦
          have e := ⋯;
          hbase a' ⋯)
        (fun a'' e ↦
          have e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hind a a' h' fa
      (fixInduction h' fun a' h ih ↦
        Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → (fun x ↦ C x) a') ((f a').get ⋯)
          (fun b' e ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun a'' e ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case ofRel.ofRel
X Y : RelCat
rel✝¹ rel✝ : SetRel X Y
h : { rel := rel✝¹ }.rel = { rel := rel✝ }.rel
⊢ { rel := rel✝¹ } = { rel := rel✝ }

Tactic:
congr

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr

Goal state after:
case e_self
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)

Tactic:
congr

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_a
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 :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom) ≫ (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv) ≫
      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv) =
    ((((((((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv) ≫
                    L'.obj (X₁ ⊗ X₂) ◁ (μ L W ε X₃ X₄).inv) ≫
                  (μ L W ε X₁ X₂).inv ▷ (L'.obj X₃ ⊗ L'.obj X₄)) ≫
                (L'.obj X₁ ⊗ L'.obj X₂) ◁ (μ L W ε X₃ X₄).hom) ≫
              (μ L W ε X₁ X₂).hom ▷ L'.obj (X₃ ⊗ X₄)) ≫
            (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).hom) ≫
          L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom) ≫
        (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv) ≫
      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv)

Tactic:
congr

Goal state after:
case e_a.e_a.e_a.e_a
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 :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom =
    (((((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv) ≫
              L'.obj (X₁ ⊗ X₂) ◁ (μ L W ε X₃ X₄).inv) ≫
            (μ L W ε X₁ X₂).inv ▷ (L'.obj X₃ ⊗ L'.obj X₄)) ≫
          (L'.obj X₁ ⊗ L'.obj X₂) ◁ (μ L W ε X₃ X₄).hom) ≫
        (μ L W ε X₁ X₂).hom ▷ L'.obj (X₃ ⊗ X₄)) ≫
      (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).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
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ⊗ₘ 𝟙 Y = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom ⊗ₘ 𝟙 Y

Tactic:
congr

Goal state after:
case e_f
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' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ F.map (A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f) = F.map (𝟙 A.V)

Tactic:
congr

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f = 𝟙 A.V
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
S T : 𝒮
f : S ⟶ T
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
by
  simpa using (inferInstance : p.IsHomLift (f ≫ 𝟙 T) (φ ≫ ψ))

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
k : Under j
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map k.hom).obj (Under.mk (𝟙 k.right))) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k

Tactic:
congr

Goal state after:
case e_a.e_12
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
k : Under j
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun b ↦
    (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
            ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b })).asEquivalence.trans
      (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b }))).asEquivalence.symm
this✝ :
  ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
this : IsFiltered (AsSmall A)
⊢ IsFiltered A

Tactic:
exact IsFiltered.of_equivalence sA.symm

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ IsFilteredOrEmpty (Grothendieck F)

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ (X Y : Grothendieck F), ∃ Z x x, True

case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : ↑(F.obj { as := op S })
⊢ Function.Injective (Fiber.inducedFunctor ⋯).map

Tactic:
intro f g heq
    replace heq := fiberInclusion.congr_map heq
    simpa [cancel_mono, ← Cat.Hom.toNatIso_hom,
      ← Cat.Hom.toNatIso_inv] using ((Hom.ext_iff _ _).mp heq).2

Goal state after:
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✝⁵ : HasZeroMorphisms C
inst✝⁴ : (i : I) → HasZeroMorphisms (D i)
inst✝³ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), (F i).PreservesHomology
inst✝ : HasZeroObject C
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).Exact
⊢ S.Exact

Tactic:
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢

Goal state after:
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✝⁵ : HasZeroMorphisms C
inst✝⁴ : (i : I) → HasZeroMorphisms (D i)
inst✝³ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), (F i).PreservesHomology
inst✝ : HasZeroObject C
S : ShortComplex C
hS : ∀ (i : I), IsZero (S.map (F i)).homology
⊢ IsZero S.homology
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
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ PreservesColimitsOfShape (SingleObj G) F

Tactic:
choose G' hg hf he using Finite.exists_type_univ_nonempty_mulEquiv G

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
G' : Type ?u.28
hg : Group G'
hf : Fintype G'
he : Nonempty (G ≃* G')
⊢ PreservesColimitsOfShape (SingleObj G) F
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
i : X ≅ Y
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj

Tactic:
have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)
  exact Nat.card_eq_of_bijective e (Equiv.bijective e)

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 Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom
        ((Types.binaryProductIso ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.left })
              ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.right })).inv ≫
          prod.snd))
      (x, y) =
    y

Tactic:
Types.binaryProductIso_inv_comp_snd

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (↾_root_.Prod.snd)) (x, y) = y
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g

Tactic:
Function.comp_apply,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ (autMap g (autMap f σ)).hom = σ.hom ≫ f ≫ g
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 : (ConcreteCategory.hom (F.map i)) y = x
left✝ : IsConnected Y
right✝ : Mono i
Z : C
f : Z ⟶ Y
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = y
⊢ ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi

Tactic:
refine ⟨⟨Z, z, hgal⟩, f ≫ i, ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 : (ConcreteCategory.hom (F.map i)) y = x
left✝ : IsConnected Y
right✝ : Mono i
Z : C
f : Z ⟶ Y
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = y
⊢ x =
    (ConcreteCategory.hom
        ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
          (Opposite.op { obj := Z, pt := z, isGalois := hgal })))
      (f ≫ i)
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
inst✝ : Mono u
b : (F.obj A).obj
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) b = a

Tactic:
apply connected_component_unique F b a u (selfProdPermIncl h b)
  exact selfProdTermIncl_fib_eq h b

Goal state after: