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

Goal state before:
pp: n l : ℕ
⊢ DifferentiableOn ℂ (fun z ↦ (-1) ^ l * ↑l ! * ((z + (↑n + 1)) ^ (-1 - ↑l) + (z - (↑n + 1)) ^ (-1 - ↑l))) ℍₒ

Tactic:
apply DifferentiableOn.const_mul

Goal state after:
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y + (↑n + 1)) ^ (-1 - ↑l) + (y - (↑n + 1)) ^ (-1 - ↑l)) ℍₒ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + (↑n + 1) ≠ 0

pp: case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0

Tactic:
· simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_intCast (.mk x hx) (-(n + 1))).symm

Goal state after:
case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z = (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum hk hz,

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z = (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hf
k M : ℕ
c : ℝ
hc : 0 < c
⊢ MonotoneOn (fun x ↦ x ^ k) (Icc ↑0 ↑M)

Tactic:
intro x hx y hy hxy
      apply pow_le_pow_left₀ (by simpa using hx.1) hxy

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

Goal state before:
pp: case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f (Max.max n m).succ).snd
      (⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)) =
    max ((FilteredClosureSmall.bundledAbstractFilteredClosure f n).snd x)
      ((FilteredClosureSmall.bundledAbstractFilteredClosure f m).snd y)

Tactic:
FilteredClosureSmall.bundledAbstractFilteredClosure

Goal state after:
case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ ⟨FilteredClosureSmall.InductiveStep (Max.max n m + 1) fun m_1 x ↦
            FilteredClosureSmall.bundledAbstractFilteredClosure f m_1,
          FilteredClosureSmall.inductiveStepRealization (Max.max n m + 1) fun m_1 x ↦
            FilteredClosureSmall.bundledAbstractFilteredClosure f m_1⟩.snd
      (⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)) =
    max ((FilteredClosureSmall.bundledAbstractFilteredClosure f n).snd x)
      ((FilteredClosureSmall.bundledAbstractFilteredClosure f m).snd y)
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case coeq.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f (Max.max n m).succ).fst

Tactic:
simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
      refine FilteredClosureSmall.InductiveStep.coeq ?_ ?_ x y g g'
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]

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

Goal state before:
pp: case coeq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f (Max.max n m).succ).snd
      (⋯.mpr (FilteredClosureSmall.InductiveStep.coeq ⋯ ⋯ x y g g')) =
    coeq g g'

Tactic:
FilteredClosureSmall.bundledAbstractFilteredClosure

Goal state after:
case coeq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ ⟨FilteredClosureSmall.InductiveStep (Max.max n m + 1) fun m_1 x ↦
            FilteredClosureSmall.bundledAbstractFilteredClosure f m_1,
          FilteredClosureSmall.inductiveStepRealization (Max.max n m + 1) fun m_1 x ↦
            FilteredClosureSmall.bundledAbstractFilteredClosure f m_1⟩.snd
      (⋯.mpr (FilteredClosureSmall.InductiveStep.coeq ⋯ ⋯ x y g g')) =
    coeq g g'
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
⊢ Small.{max v w, u} (filteredClosure f).FullSubcategory

Tactic:
by
  refine small_of_injective_of_exists (FilteredClosureSmall.abstractFilteredClosureRealization f)
    (fun _ _ => ObjectProperty.FullSubcategory.ext) ?_
  rintro ⟨j, h⟩
  induction h with
  | base x =>
      refine ⟨⟨0, ?_⟩, ?_⟩
      · simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
        exact ULift.up x
      · simp only [FilteredClosureSmall.abstractFilteredClosureRealization,
          FilteredClosureSmall.bundledAbstractFilteredClosure]
        rfl
  | max hj₁ hj₂ ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
      refine FilteredClosureSmall.InductiveStep.max ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
      rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
      rfl
  | coeq hj₁ hj₂ g g' ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
      refine FilteredClosureSmall.InductiveStep.coeq ?_ ?_ x y g g'
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
      rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
      rfl

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:
by
  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.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
n : ℤ
⊢ Injective (R.cochainComplex.X n)

Tactic:
by_cases hn : 0 ≤ n
  · obtain ⟨k, rfl⟩ := Int.eq_ofNat_of_zero_le hn
    exact Injective.of_iso (R.cochainComplexXIso _ _ rfl).symm inferInstance
  · exact IsZero.injective (CochainComplex.isZero_of_isStrictlyGE _ 0 _ (by lia))

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)
⊢ kernel.ι (d g) ≫ d f = 0

Tactic:
refine (isColimitFiniteSubproductsCocone (fun (_ : M) => G)).pullback_zero_ext (fun F => ?_)

Goal state after:
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)
⊢ pullback.snd ((finiteSubcoproductsCocone fun x ↦ G).ι.app F) (kernel.ι (d g)) ≫ kernel.ι (d g) ≫ d f = 0
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✝ n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ (-f) ≫ R.cocomplex.d n m = 0

Tactic:
simp [hf]

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✝ 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
⊢ (g ≫ f) ≫ R.cocomplex.d n m = 0

Tactic:
simp [hf]

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 R : C
f : Q ⟶ R
a : P ⟶ Q
h : a ≫ f = 0
⊢ pseudoApply f (Quot.mk (PseudoEqual Q) (Over.mk a)) = 0

Tactic:
by simp [over_coe_def, pseudoApply_mk', h]

Goal state after:
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✝ n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ R.complex.d m n ≫ (-f) = 0

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯))

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯)).pt

Tactic:
· exact (IsColimit.precomposeHomEquiv _ _).symm (cokernelIsCokernel f.hom)

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯)).pt
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a b c : N ⋊[φ] G
⊢ (a * b * c).left = (a * (b * c)).left

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a b c : N ⋊[φ] G
⊢ (a * b * c).right = (a * (b * c)).right

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ F.map (inv (f ≫ g))ᘁ = F.map (inv f)ᘁ ≫ F.map (inv g)ᘁ

Tactic:
by simp [comp_rightAdjointMate]

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfShape J H ↔ PreservesColimitsOfShape J (F ⋙ H)

Tactic:
refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {K} ↦ ?_⟩⟩

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
x✝ : PreservesColimitsOfShape J (F ⋙ H)
K : J ⥤ D
⊢ PreservesColimit K H
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
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f

Tactic:
← adj₁.counit_naturality

Goal state after:
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
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ F.map (U.map (R.map f)) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : L.Full
inst✝² : L.Faithful
inst✝¹ : G.Full
inst✝ : G.Faithful
h : (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔ ∀ (X : Cᵒᵖ), Mono (q.op.rightTriple.leftToRight.app X)
⊢ (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)

Tactic:
rw [← (Opposite.equivToOpposite (α := C)).forall_congr_right] at h

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : L.Full
inst✝² : L.Faithful
inst✝¹ : G.Full
inst✝ : G.Faithful
h :
  (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔
    ∀ (a : C), Mono (q.op.rightTriple.leftToRight.app (Opposite.equivToOpposite a))
⊢ (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint

Tactic:
refine ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft ?_).isLeftAdjoint

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ L ⋙ F ≅ L' ⋙ (comonadicAdjunction F).toComonad.forget
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ (map (α ≫ β)).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (map α ⋙ map β).map f

Tactic:
by
    dsimp
    simp only [comp_id, id_comp]
    ext <;> simp

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ (map (α ≫ β)).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (map α ⋙ map β).map f

Tactic:
by
    dsimp
    simp only [comp_id, id_comp]
    ext <;> simp

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
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ fixInduction h H = H a h fun x h' ↦ fixInduction ⋯ H

Tactic:
by
  unfold fixInduction
  generalize_proofs
  induction ‹Acc _ _›
  rfl

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
use τ ≫ ψ

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := ⋯
τ : a'✝ ⟶ pullbackObj ⋯ g := ⋯
⊢ (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ ≫ ψ) ∧ ∀ (y : a'✝ ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ
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:
simpa using IsHomLift.fac (forget F) (g ≫ f) φ'

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

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf : (fiberInclusion.map f).base = 𝟙 S
⊢ (F.map (fiberInclusion.map f).base.op.toLoc).toFunctor.obj
      (fiberInclusion.obj ((Fiber.inducedFunctor ⋯).obj Y)).fiber =
    (F.map (𝟙 { as := op S })).toFunctor.obj Y

Tactic:
simp [hf]

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

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

Tactic:
by_cases h : IsConnected X

Goal state after:
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 ι

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.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : X.HasTensor Y
inst✝² : Y.HasTensor X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ whiskerLeft X f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ whiskerRight f X

Tactic:
dsimp [braiding]
  cat_disch

Goal state after: