mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
ε : ℝ
hε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
npos : 0 < n
⊢ u n / ↑n ≤ (↑n * l + ε * (1 + ε + l) * ↑n) / ↑n

Tactic:
by gcongr; linarith only [hn]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ PreservesFiniteColimits (embedding F)

Tactic:
apply preservesFiniteColimits_preadditiveCoyonedaObj_of_projective

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:

Tactic:
_ = ∫ x in N..M+N, f x := by
        refine intervalIntegral.integral_congr_uIoo fun x ↦ ?_
        grind [Real.norm_of_nonneg, uIoo_of_le]
      _ ≤ ∑ n ∈ Finset.range M, f (n + N : ℕ) := by
        convert! AntitoneOn.integral_le_sum (anti.mono _) using 2 <;> grind
      _ ≤ _ := by grind [summable.sum_le_tsum, Nat.cast_pos]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

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
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'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
⊢ IsConnected (StructuredArrow { left := i₂, right := j₂, hom := u₂ } (map iL.hom iR.inv))

Tactic:
have := final_of_natIso iR
  rw [isConnected_iff_of_equivalence (StructuredArrow.commaMapEquivalence iL.hom iR.inv _)]
  have : StructuredArrow.map₂ u₂ iR.hom ≅ StructuredArrow.post j₂ G R' ⋙
      StructuredArrow.map₂ (G := 𝟭 _) (F := 𝟭 _) (R' := R ⋙ H) u₂ iR.hom ⋙
      StructuredArrow.pre _ R H :=
    eqToIso (by
      congr
      · simp
      · ext; simp) ≪≫
    (StructuredArrow.map₂CompMap₂Iso _ _ _ _).symm ≪≫
    isoWhiskerLeft _ ((StructuredArrow.map₂CompMap₂Iso _ _ _ _).symm ≪≫
      isoWhiskerLeft _ (StructuredArrow.preIsoMap₂ _ _ _).symm) ≪≫
    isoWhiskerRight (StructuredArrow.postIsoMap₂ j₂ G R').symm _
  have := final_of_natIso this.symm
  rw [IsIso.Iso.inv_inv]
  infer_instance

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

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
⊢ IsIso (colimitPointwiseProductToProductColimit F)

Tactic:
refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩

Goal state after:
case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
⊢ y = y'

case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
⊢ ∃ a, (hom (colimitPointwiseProductToProductColimit F)) a = x
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) = 0

Tactic:
rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)) =
    𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)

Tactic:
by
    rw [← (HomotopyCategory.quotient _ _).map_id]
    apply HomotopyCategory.eq_of_homotopy
    apply InjectiveResolution.descIdHomotopy

Goal state after:
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
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ ((Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯).hom = (R.extMk (g ≫ f) m hm ⋯).hom

Tactic:
simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom, Category.assoc]

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
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (g ≫ f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (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 : D
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩

Goal state after:
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 : D
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Epi f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (r • α.app Y✝) = (r • α.app X✝) ≫ G.map f✝

Tactic:
rw [comp_smul, smul_comp, α.naturality]

Goal state after:
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✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this : PreservesColimit (parallelPair NormalEpi.g 0) L
⊢ Nonempty (NormalEpi f)

Tactic:
refine ⟨NormalEpi.ofArrowIso ?_ e⟩

Goal state after:
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✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this : PreservesColimit (parallelPair NormalEpi.g 0) L
⊢ NormalEpi (L.map f')
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing X (G.obj (F.obj X)ᘁ)

Tactic:
letI := exactPairingCongrRight (X := F.obj X) (Y := F.obj (G.obj (F.obj X)ᘁ))
      (Y' := (F.obj X)ᘁ) (adj.toEquivalence.counitIso.app (F.obj 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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasRightDual (F.obj X)
this : ExactPairing (F.obj X) (F.obj (G.obj (F.obj X)ᘁ)) :=
  exactPairingCongrRight (adj.toEquivalence.counitIso.app (F.obj X)ᘁ)
⊢ ExactPairing X (G.obj (F.obj X)ᘁ)
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)

Tactic:
refine Prod.ext rfl (funext fun x => ?_)

Goal state after:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 x =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 x
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 x =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 x

Tactic:
induction x using Fin.cases

Goal state after:
case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 0 =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 0

case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
i✝ : Fin n
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 i✝.succ =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 i✝.succ
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: 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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ otherMap R F' adj₁ adj₂ X = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))

Tactic:
by
      dsimp [otherMap]
      rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc,
        adj₁.right_triangle_components, comp_id, adj₂.left_triangle_components]

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
x : B
h : x ⟶ c
X✝ Y✝ : LeftLift f g
η : X✝ ⟶ Y✝
⊢ (X✝.whisker h).unit ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = (Y✝.whisker h).unit

Tactic:
dsimp only [whisker_lift, whisker_unit]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X✝ Y✝ : LeftLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ X✝.unit ≫ (α_ h X✝.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = h ◁ Y✝.unit ≫ (α_ h Y✝.lift f).inv
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
⊢ ∀ (s : LeftLift u (h ≫ 𝟙 a)) (τ : (LeftLift.mk f adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯

Tactic:
by
      intro s τ₀
      ext
      /- We need to specify the type of `τ` to use the notation `⊗≫`. -/
      let τ : h ≫ f ⟶ s.lift := τ₀.right
      have hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit := by simpa [bicategoricalComp] using LeftLift.w τ₀
      calc τ
        _ = 𝟙 _ ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 _ := by
          rw [adj.left_triangle]; bicategory
        _ = 𝟙 _ ⊗≫ h ◁ adj.unit ▷ f ⊗≫ (_ ◁ adj.counit ≫ τ ▷ _) ⊗≫ 𝟙 _ := by
          rw [leftZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = _ := by
          rw [hτ]; dsimp only [StructuredArrow.homMk_right]

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ (b ∈ (f a).bind fun x ↦ Part.some ⟨some x, ⋯⟩) ↔
    b ∈
      (Part.some ⟨some a, ⋯⟩).bind
        (PFun.toSubtype (fun x ↦ ¬x = (partialFunToPointed.obj Y✝).point) (partialFunToPointed.map f).toFun ∘
          Subtype.val)

Tactic:
Part.bind_some

Goal state after:
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ (b ∈ (f a).bind fun x ↦ Part.some ⟨some x, ⋯⟩) ↔
    b ∈
      (PFun.toSubtype (fun x ↦ ¬x = (partialFunToPointed.obj Y✝).point) (partialFunToPointed.map f).toFun ∘ Subtype.val)
        ⟨some a, ⋯⟩
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
⊢ unopFunctor.IsEquivalence

Tactic:
by
  change opEquivalence.inverse.IsEquivalence
  infer_instance

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

Goal state after:
Module: Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : P.IsStableUnderBraiding
c : WideSubcategory P
inst✝² : ComonObj c.obj
inst✝¹ : IsCommComonObj c.obj
inst✝ : P.IsStableUnderComonoid c.obj
⊢ Δ ≫ (β_ c c).hom = Δ

Tactic:
ext
    exact IsCommComonObj.comul_comm _

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Cartesian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsCartesianDistributive C
A B Z : C
f g : Z ⟶ (pair A B).obj { as := WalkingPair.left }
he : f ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = g ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl
⊢ f = g

Tactic:
by
      let ι := coprod.inl (X := A) (Y := B)
      have : Mono (Z ◁ ι) := SplitMono.mono
        { retraction := (∂L Z A B).inv ≫ coprod.desc (𝟙 _) (fst Z B ≫ lift (𝟙 Z) f) }
      have : lift (𝟙 Z) f = lift (𝟙 Z) g := by rw [← cancel_mono (Z ◁ ι)]; aesop
      simpa only [lift_snd] using this =≫ snd _ _

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

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ (homCartesianLift f g φ' ≫ cartesianLift a f).base = φ'.base

Tactic:
by simpa using IsHomLift.fac (forget F) (g ≫ f) φ'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
this : IsIso (limit.post K colim)
⊢ PreservesLimit K colim

Tactic:
apply preservesLimit_of_isIso_post

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F

Tactic:
by
  have : HasLeftDerivedFunctor F W ↔ HasRightKanExtension W.Q F :=
    ⟨fun h => h.hasRightKanExtension', fun h => ⟨h⟩⟩
  rw [this, hasRightExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]

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

Goal state before:
pp: case pos
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
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

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
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
· exact has_decomp_connected_components_aux_conn X

Goal state after:
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
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
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 : C
x : (F.obj X).obj
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
⊢ ∃ Y i y, (ConcreteCategory.hom (F.map i)) y = x ∧ IsConnected Y ∧ Mono i

Tactic:
let s' : IsColimit s := isColimitOfPreserves F hl

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
⊢ ∃ Y i y, (ConcreteCategory.hom (F.map i)) y = x ∧ IsConnected Y ∧ Mono i
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
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
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map fi2.inv)) ((ConcreteCategory.hom (F.map fi1.hom)) x) = y

Tactic:
hfi1,

Goal state after:
case h
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
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map fi2.inv)) a = y
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✝ : IsGalois X
x y : (F.obj X).obj
φ : Aut X
h : φ • x = y
a : AutGalois F
ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ
⊢ ∃ g, g • x = y

Tactic:
use (autMulEquivAutGalois F).symm ⟨a⟩

Goal state after:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).obj
φ : Aut X
h : φ • x = y
a : AutGalois F
ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ
⊢ (autMulEquivAutGalois F).symm { unop' := a } • x = y