mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ (x2 - ↑x) ^ (-2)) l - 0

Tactic:
rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = ↑(-2) * (l - ↑x) ^ (-2 - 1) - 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card = b.card + 1
⊢ 1 ≤ (regularizedHGFunSeries a b).radius

Tactic:
by
  by_cases! h' : ∀ j ∈ a, ∀ k : ℕ, j ≠ -k
  · grind
  · obtain ⟨j, hj, k, h'⟩ := h'
    rw [radius_regularizedHGFunSeries_eq_top_of_finite hj h']
    simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = (log (2 * π) + log ↑n) / 2 + log ((↑n / rexp 1) ^ n)

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

pp: n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0

Tactic:
log_pow,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = (log (2 * π) + log ↑n) / 2 + ↑n * log (↑n / rexp 1)

case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ},
    i ∈ Finset.Iic n →
      (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≠ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)

Tactic:
have := ne_of_lt (hcpos i (Finset.mem_Iic.mp hi))

Goal state after:
case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ},
    i ∈ Finset.Iic n →
      (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
this : 0 ≠ (-1) ^ i * c i
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≠ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
⊢ HasProdUniformlyOn (fun n z ↦ 1 + sineTerm z n) (fun x ↦ Complex.sin (↑π * x) / (↑π * x)) Z

Tactic:
apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right
  exact fun x hx => euler_sineTerm_tprod (by aesop)

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

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ (↑n ^ (1 + k))⁻¹

Tactic:
exact summable_nat_pow_inv.mpr <| by lia

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < ↑i * Real.log c

Tactic:
← Real.log_pow

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)
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₂
this : (R ⋙ H).Final
⊢ IsConnected (StructuredArrow { left := i₂, right := j₂, hom := u₂ } (map iL.hom iR.inv))

Tactic:
isConnected_iff_of_equivalence (StructuredArrow.commaMapEquivalence iL.hom iR.inv _)

Goal state after:
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₂
this : (R ⋙ H).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom (inv iR.inv)))
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Full

Tactic:
rw [functor]
  have : (F C).Full := by rw [F]; infer_instance
  have : (G C).Full := by rw [G]; infer_instance
  have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ Mono (I.ι.f n)

Tactic:
by
  cases n
  · exact mono_of_isLimit_fork I.isLimitKernelFork
  · rw [ι_f_succ]; infer_instance

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 : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q)
      ((CohomologyClass.mk x).toSmallShiftedHom.comp (SmallShiftedHom.mk₀Inv 0 ⋯ R.ι' ⋯) ⋯) =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
simp only [SmallShiftedHom.equiv_comp, CohomologyClass.equiv_toSmallShiftedHom_mk,
    SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv,
    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Iso.refl_inv,
    ShiftedHom.mk₀_id_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) n

Tactic:
cases n
    · rw [CochainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros]
      · refine (ShortComplex.exact_and_mono_f_iff_of_iso ?_).2
          ⟨exact_f_d (Injective.ι Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
          (by simp [ofCocomplex])
      all_goals rfl
    · rw [quasiIsoAt_iff_exactAt]
      · apply ofCocomplex_exactAt_succ
      · apply CochainComplex.exactAt_succ_single_obj

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₁ :
  F.map (𝟙 X) ≫ I.toRightDerivedZero' F =
    (injectiveResolution X).toRightDerivedZero' F ≫
      HomologicalComplex.cyclesMap
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) =
    I.toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv

Tactic:
simp only [Functor.map_id, id_comp] at h₁

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₁ :
  I.toRightDerivedZero' F =
    (injectiveResolution X).toRightDerivedZero' F ≫
      HomologicalComplex.cyclesMap
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) =
    I.toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
⊢ P f

Tactic:
refine cast ?_ (hyp b.back f.val)
  rcases a with ⟨⟨⟩, a : X⟩
  rcases b with ⟨⟨⟩, b : X⟩
  rcases f with ⟨g : G, h : g • a = b⟩
  cases inv_smul_eq_iff.mpr h.symm
  rfl

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 : C
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
suffices ∀ (W : D) (z : L.obj Y ⟶ W) (hz : L.map f ≫ z = 0),
      ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = z from
    preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
      ((CokernelCofork.isColimitMapCoconeEquiv _ L).2
        (Cofork.IsColimit.ofExistsUnique
          (fun s ↦ existsUnique_of_exists_of_unique
            (this _ _ (CokernelCofork.condition s))
            (fun _ _ h₁ h₂ ↦ by simpa [cancel_epi] using h₁.trans h₂.symm))))

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 : C
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
⊢ ∀ (W : D) (z : L.obj Y ⟶ W), L.map f ≫ z = 0 → ∃ l, L.map (cokernel.π f) ≫ l = z
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
J : Type u_3
inst✝ : Category.{v_2, u_3} J
F : J ⥤ Action V G
c✝ : Cocone F
h : IsColimit ((forget V G).mapCocone c✝)
⊢ IsColimit c✝

Tactic:
apply isColimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
    exact evaluationJointlyReflectsColimits _ (fun _ => h)

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

Goal state before:
pp: case refine_3
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)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ m = ↑((h X).lift' s.ι ⋯)

Tactic:
← cancel_mono (adj₁.unit.app X)

Goal state after:
case refine_3
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)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ m ≫ adj₁.unit.app X = ↑((h X).lift' s.ι ⋯) ≫ adj₁.unit.app X
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)
X : B
Y : A
⊢ ∀ (Y' : A) (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g

Tactic:
Y'

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)
X : B
Y Y' : A
⊢ ∀ (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g
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
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
⊢ ∀ (Y_1 : B) (f : X ⟶ Y) (g : L.obj Y ⟶ Y_1),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y_1).symm (L.map f ≫ g) =
      f ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h Y Y_1).symm g

Tactic:
Y'

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
⊢ ∀ (f : X ⟶ Y) (g : L.obj Y ⟶ Y'),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y').symm (L.map f ≫ g) =
      f ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h Y Y').symm g
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)
this✝ : L'.IsLeftAdjoint
this : (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv).IsLeftAdjoint := inferInstance
⊢ L.IsLeftAdjoint

Tactic:
refine ((Adjunction.ofIsLeftAdjoint
      (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv)).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)
this✝ : L'.IsLeftAdjoint
this : (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv).IsLeftAdjoint := inferInstance
⊢ L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv ≅ L
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
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫
      (α_ (θ.app a) (ι.app a) (H.map f)).hom ≫
        θ.app a ◁ ι.naturality f ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).inv ≫ θ.naturality f ▷ ι.app b ≫ (α_ (F.map f) (θ.app b) (ι.app b)).hom =
    ((α_ (η.app a) (ι.app a) (H.map f)).hom ≫
        η.app a ◁ ι.naturality f ≫
          (α_ (η.app a) (G.map f) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (F.map f) (η.app b) (ι.app b)).hom) ≫
      F.map f ◁ Γ.as.app b ▷ ι.app b

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

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'
  rw [fixInduction_spec]
  -- Porting note: the explicit motive required because `simp` does not apply `Part.get_eq_of_mem`
  refine Eq.rec (motive := fun x e ↦
      Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ ∀ (j j' : J) (f_1 : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f_1))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
      eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
intro j j' h

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ (hom
        ((homDiagram
              ((hom
                  (limit.lift (F ⋙ objects)
                    { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                X✝)
              ((hom
                  (limit.lift (F ⋙ objects)
                    { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                Y✝)).map
          h))
      (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.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
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := ⋯
sB : B ≌ AsSmall B := ⋯
sT : T ≌ AsSmall T := ⋯
L' : AsSmall A ⥤ AsSmall T := ⋯
R' : AsSmall B ⥤ AsSmall T := ⋯
b : AsSmall B
x : AsSmall T := ⋯
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x := ⋯
⊢ F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)

Tactic:
have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl

Goal state after:
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✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
hsT : ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 ((𝟭 (AsSmall T)).obj X)
⊢ F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ (mapPullbackAdj (f ≫ g)).unit ≫ (map (f ≫ g)).whiskerLeft (pullbackComp f g).hom = (mapPullbackAdj (f ≫ g)).unit

Tactic:
by
  rw [pullbackComp, Adjunction.unit_rightAdjointUniq_hom]

Goal state after: