mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ ∀ (b : ℕ), ((↑1 * x + ↑(-↑(b + 1))) ^ (↑k + 1))⁻¹ = (x - (↑b + 1)) ^ (-1 - ↑k)

Tactic:
simp [← zpow_neg, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| fun n ↦ iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z

Tactic:
n

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n ↦ ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n ↦ ⌊c k ^ n⌋₊) n)

Tactic:
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c k ^ n⌋₊ := by
    intro n
    refine zero_lt_one.trans_le ?_
    simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ (cone k).le]

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n ↦ ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n ↦ ⌊c k ^ n⌋₊) n)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasColimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (Sigma.ι f s).app d ≫ (sigmaObjIso f d).hom = Sigma.ι (fun s ↦ (f s).obj d) s

Tactic:
by
  simp [sigmaObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasColimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ Sigma.ι (fun s ↦ (f s).obj d) s ≫ (sigmaObjIso f d).inv = (Sigma.ι f s).app d

Tactic:
by
  simp [sigmaObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach,
      h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x ≫ Sigma.ι (fun x ↦ G) (↑x).as ≫ d g =
    0

Tactic:
simp [← Preadditive.comp_sum, ← Preadditive.sum_comp', pullback.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : f = 0
a : Pseudoelement P
⊢ pseudoApply f a = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
⊢ pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧ → ⟦a⟧ = ⟦a'⟧

Tactic:
| _ a a'
   => 

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
⊢ pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧ → ⟦a⟧ = ⟦a'⟧
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'

Tactic:
induction abar, abar' using Quotient.inductionOn₂ with | _ a a'

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
⊢ pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧ → ⟦a⟧ = ⟦a'⟧
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
obtain ⟨a', ha⟩ := hS _ this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
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
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯
            ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
      ((((ShiftedHom.mk₀ 0 ⋯ φ.hom').map DerivedCategory.Q).comp
            (ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q)
            ⋯).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯

Tactic:
← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),

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
⊢ ((ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
          (ShiftedHom.mk₀ 0 ⋯
            ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π')))
          ⋯).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
      ((((ShiftedHom.mk₀ 0 ⋯ φ.hom').map DerivedCategory.Q).comp
            (ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q)
            ⋯).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯
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
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ (((ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
              (ShiftedHom.mk₀ 0 ⋯
                ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π')))
              ⋯).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯ =
    ((ShiftedHom.mk₀ 0 ⋯
              ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
          (((ShiftedHom.mk₀ 0 ⋯ φ.hom').map DerivedCategory.Q).comp
            (ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q)
            ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯

Tactic:
← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),

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
⊢ (((ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
              (ShiftedHom.mk₀ 0 ⋯
                ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π')))
              ⋯).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯ =
    (((ShiftedHom.mk₀ 0 ⋯
                  ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
              ((ShiftedHom.mk₀ 0 ⋯ φ.hom').map DerivedCategory.Q) ⋯).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
hf : L.map (cokernel.π f) = 0
⊢ P.epiModSerre f

Tactic:
simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π f) (𝟙 _)

Goal state after:
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✝
⊢ (↾fun x ↦ f ≫ g • x) = (↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x

Tactic:
by ext x; exact (smul_smul g f x).symm

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
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
J : Type u_4
inst✝ : Category.{v_3, u_4} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
⊢ PreservesColimitsOfShape J F

Tactic:
by
  constructor
  intro K
  apply Action.preservesColimit_of_preserves
  exact PreservesColimitsOfShape.preservesColimit

Goal state after:
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
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)

Tactic:
constructor
  · intro h c
    exact (inferInstance : Epi (((evaluation _ _).obj c).map η))
  · intros
    apply NatTrans.epi_of_epi_app

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
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.leftToRight.app X)

Tactic:
rw [mono_leftToRight_app_iff_mono_adj₂_unit_app]

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
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.adj₂.unit.app (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (whiskerHom i.inv h ≫ whiskerHom i.hom h) = StructuredArrow.Hom.right (i.inv ≫ i.hom) ▷ h

Tactic:
simp [-Iso.inv_hom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ StructuredArrow.Hom.right (whiskerHom i.inv h ≫ whiskerHom i.hom h) = h ◁ StructuredArrow.Hom.right (i.inv ≫ i.hom)

Tactic:
simp [-Iso.inv_hom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ (whiskerHom i.inv h ≫ whiskerHom i.hom h).left = h ◁ (i.inv ≫ i.hom).left

Tactic:
simp [-Iso.inv_hom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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:
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.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:
rw [eq, ← Subobject.pullback_comp]; apply le_of_eq; congr; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X : C
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
T : Over X
⊢ Hom.left ((pullbackIsoOverPullback g).hom.app T) ≫ pullback.fst T.hom g = fst T.hom g

Tactic:
simpa using! (Over.forget _).congr_map
    ((ChosenPullbacksAlong.mapPullbackAdj g).rightAdjointUniq_hom_app_counit
      (Over.mapPullbackAdj g) T)

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
⊢ (fun x ↦ (Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₁ ≫ Sigma.desc e) =
    (fun x ↦ (Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₂ ≫ Sigma.desc e)

Tactic:
ext a

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ Sigma.ι (fun a ↦ pullback g₁ (Sigma.ι X a)) a ≫
      (fun x ↦ (Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₁ ≫ Sigma.desc e) =
    Sigma.ι (fun a ↦ pullback g₁ (Sigma.ι X a)) a ≫
      (fun x ↦ (Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₂ ≫ Sigma.desc e)
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : PreGaloisCategory C
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ HasColimitsOfShape (SingleObj G) C

Tactic:
obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.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 Y : C
f g : X ⟶ Y
h : F.map f = F.map g
⊢ f = g

Tactic:
have : IsIso (equalizer.ι (F.map f) (F.map g)) := equalizer.ι_of_eq h

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (equalizer.ι (F.map f) (F.map g))
⊢ f = g
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
  by_contra h
  have ⟨hin⟩ : Nonempty (IsInitial X) := (initial_iff_fiber_empty F X).mpr (not_nonempty_iff.mp h)
  exact IsConnected.notInitial hin

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ HasColimitsOfShape (SingleObj G) FintypeCat

Tactic:
obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

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

Goal state before:
pp: 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 ≫ τ.hom = σ.hom ≫ f

Tactic:
let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  refine ⟨?_, ?_, ?_⟩
  · exact (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)
  · apply evaluation_injective_of_isConnected F A B a
    simp
  · intro τ hτ
    apply evaluation_aut_injective_of_isConnected F B (F.map f a)
    simpa using ConcreteCategory.congr_hom (F.congr_map hτ) a

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

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

pp: case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.right ≫ m =
    inj bc WalkingPair.right ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

Tactic:
· refine Cofan.IsColimit.hom_ext h₁ _ _ (fun a ↦ by aesop)

Goal state after:
case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.right ≫ m =
    inj bc WalkingPair.right ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯
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 : (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt),
    ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi

Tactic:
intro (x : F.obj X)

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
⊢ ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Set.range ⇑(autEmbedding F) = ⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom}

Tactic:
ext a

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ a ∈ Set.range ⇑(autEmbedding F) ↔ a ∈ ⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom}
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : C ≌ D
h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X
h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y
k : ∀ (X : C), e.unitIso.hom.app X = eqToHom ⋯
k' : ∀ (Y : D), e.counitIso.hom.app Y = eqToHom ⋯
⊢ ∀ (X : C), (𝟭 C).obj X = (e.functor ⋙ e.inverse).obj X

Tactic:
by simp [h]

Goal state after: