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

Goal state before:
pp: case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) •
      z ^ i =
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦
            if i = 0 then ℘[L - l₀] x
            else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)).coeff
        i *
      z ^ i

Tactic:
FormalMultilinearSeries.coeff_ofScalars,

Goal state after:
case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) •
      z ^ i =
    (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) *
      z ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ 1 < eval x (T ℝ n)

Tactic:
by
  have : arcosh x ≠ 0 := by grind [cosh_arcosh, cosh_zero]
  rw [← cosh_arcosh (le_of_lt hx), T_real_cosh, one_lt_cosh, mul_ne_zero_iff]
  exact ⟨by norm_cast, by assumption⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPSummand x b c * (z - x) ^ b)

Tactic:
simp_rw [← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]

Goal state after:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPExceptSummand (L.ω₁ / 2) x b c * (z - x) ^ b)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ Summable ((fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm)

Tactic:
summable_partition _ Int.existsUnique_mem_box

Goal state after:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i ↦ ((fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i) ∧
    Summable fun j ↦ ∑' (i : ↑↑(box j)), ((fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i

k : ℝ
hk : 2 < k
⊢ 0 ≤ (fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℤ
m : ℕ
⊢ fib (-↑m + n) = fib (-↑m - 1) * fib n + fib (-↑m) * fib (n + 1)

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
    · exact fib_add_natCast _ _
    · exact fib_neg_natCast_add_neg_natCast _ _

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case hv.a
⊢ (fun n ↦ (√5)⁻¹ * φ ^ n) ∈ fibRec.solSpace

Tactic:
exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenRatio_isSol_fibRec

Goal state after:
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)
⊢ Tendsto (fun n ↦ u n / ↑n) atTop (𝓝 l)

Tactic:
have lnonneg : 0 ≤ l := by
    rcases hlim 2 one_lt_two with ⟨c, _, ctop, clim⟩
    have : Tendsto (fun n => u 0 / c n) atTop (𝓝 0) :=
      tendsto_const_nhds.div_atTop (tendsto_natCast_atTop_iff.2 ctop)
    apply le_of_tendsto_of_tendsto' this clim fun n => ?_
    gcongr
    exact hmono zero_le

Goal state after:
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
⊢ Tendsto (fun n ↦ u n / ↑n) atTop (𝓝 l)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫ φ f g = f ≫ biprod.inl

Tactic:
simp [φ]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫ φ f g ≫ biprod.fst = -𝟙 Y

Tactic:
simp [φ]

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

Goal state before:
pp: case hR₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := ⋯
faithful : φ.Faithful
⊢ (cm.op.map (preadditiveYoneda.obj Y)).Exact

Tactic:
exact exact.op.map_of_mono_of_preservesKernel _ mono inferInstance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
⊢ IsIndObject A

Tactic:
let hc : IsColimit c := (Functor.Final.isColimitWhiskerEquiv _ _).symm
    (Presheaf.isColimitTautologicalCocone A)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
⊢ IsIndObject A
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).inv ≫ coyoneda.map (colimit.ι F i).op = limit.π (F.op ⋙ coyoneda) (op i)

Tactic:
← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).inv ≫
      (coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op ⋙ coyoneda) (op i) =
    limit.π (F.op ⋙ coyoneda) (op i)
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape WalkingParallelPair C
⊢ HasColimitsOfShape WalkingParallelPair (Ind C)

Tactic:
by
  refine ⟨fun F => ?_⟩
  obtain ⟨P⟩ := nonempty_indParallelPairPresentation (F.obj WalkingParallelPair.zero).2
    (F.obj WalkingParallelPair.one).2 (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.left)
    (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.right)
  exact hasColimit_of_iso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
x✝ : Cᵒᵖ ⥤ Type u
⊢ IsIndObject x✝ ↔ leftExactFunctor Cᵒᵖ (Type u) x✝

Tactic:
apply isIndObject_iff_preservesFiniteLimits

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
⊢ (finiteSubproductsCone f).π.app S = ∑ a ∈ (Opposite.unop S).attach, Pi.π f (↑a).as ≫ Pi.ι (fun a ↦ f (↑a).as) a

Tactic:
by
  dsimp only [finiteSubproductsCone_pt, Functor.const_obj_obj, liftToFinsetObj_obj,
    Discrete.functor_obj_eq_as, finiteSubproductsCone_π_app]
  ext v
  simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Preadditive.sum_comp, Category.assoc]
  rw [Finset.sum_eq_single v]
  · simp
  · intro b hb hb₁
    rw [Pi.ι_π_of_ne _ hb₁, comp_zero]
  · simp

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✝ : EnoughInjectives C
Z : C
⊢ (ofCocomplex Z).d 0 1 = d (Injective.ι Z)

Tactic:
simp [ofCocomplex]

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✝ : EnoughInjectives C
Z : C
⊢ (Iso.refl
          {
              X₁ :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                    ((CochainComplex.single₀ C).obj Z)).X₂,
              X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
              X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
              f :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                    (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
              g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
              zero := ⋯ }.X₂).hom ≫
      { X₁ := Z, X₂ := under Z, X₃ := syzygies (Injective.ι Z), f := Injective.ι Z, g := d (Injective.ι Z),
          zero := ⋯ }.g =
    {
          X₁ :=
            ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                ((CochainComplex.single₀ C).obj Z)).X₂,
          X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
          X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
          f :=
            ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
          g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
          zero := ⋯ }.g ≫
      (Iso.refl
          {
              X₁ :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                    ((CochainComplex.single₀ C).obj Z)).X₂,
              X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
              X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
              f :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                    (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
              g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
              zero := ⋯ }.X₃).hom

Tactic:
simp [ofCocomplex]

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫
      𝟙
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)

Tactic:
erw [id_comp, comp_id]

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
Module: Mathlib.CategoryTheory.Action.Limits

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

Tactic:
exact add_smul _ _ _

Goal state after:
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
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
⊢ { l //
    (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ l = s.π ∧
      ∀ {m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt}, (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = l }

Tactic:
have := fun Y ↦ h Y |>.epi
    refine ⟨((h X).desc' s.π ?_).1, ?_, ?_⟩
    · rw [← cancel_epi (adj₁.counit.app (h X).W)]
      rw [← adj₁.counit_naturality_assoc (h X).left]
      dsimp
      rw [← dsimp% s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp,
        F.map_comp_assoc, s.condition, ← adj₁.counit_naturality_assoc (h X).right]
    · apply ((h X).desc' s.π _).2
    · intro m hm
      rw [← cancel_epi (adj₁.counit.app X)]
      apply hm.trans ((h _).desc' s.π _).2.symm

Goal state after:
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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
⊢ R.IsRightAdjoint

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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := ⋯
⊢ R'.IsRightAdjoint

Tactic:
· let : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := by
      infer_instance
    refine ((Adjunction.ofIsRightAdjoint
      (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight ?_).isRightAdjoint
    exact Functor.isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm ≪≫ R.rightUnitor

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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := ⋯
⊢ R'.IsRightAdjoint
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h✝ : b✝ ⟶ c✝
η✝ : Hom₂ f✝ g✝
ih : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
⊢ (fun p ↦ normalizeAux p (Hom.comp f✝ h✝)) = fun p ↦ normalizeAux p (Hom.comp g✝ h✝)

Tactic:
| whisker_right _ _ ih =>

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

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ (Γ.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.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ ((F.mapComp' (𝟙 X₁) f f ⋯).symm ≪≫ F.mapComp' f (𝟙 X₂) f ⋯).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom

Tactic:
mapComp'_comp_id,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ ((F.mapComp' (𝟙 X₁) f f ⋯).symm ≪≫ (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ ((F.mapComp' f (𝟙 X₂) f ⋯).symm ≪≫ F.mapComp' (𝟙 X₁) f f ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom

Tactic:
mapComp'_comp_id,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId X₂).symm).symm ≪≫ F.mapComp' (𝟙 X₁) f f ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
⊢ ∀ (X : ↑s.pt), (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.obj X = (s.π.app j).toFunctor.obj X

Tactic:
intro; simp [← comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y Z : C
⊢ (μ L W ε X Y).hom ▷ (toMonoidalCategory L W ε).obj Z ≫
      (μ L W ε (X ⊗ Y) Z).hom ≫ (toMonoidalCategory L W ε).map (α_ X Y Z).hom =
    (α_ ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z)).hom ≫
      (toMonoidalCategory L W ε).obj X ◁ (μ L W ε Y Z).hom ≫ (μ L W ε X (Y ⊗ Z)).hom

Tactic:
simp [associator_hom_app L W ε X Y Z]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ 𝒴.p.map (F.map φ) ≫ eqToHom ⋯

Tactic:
rw [← Functor.comp_map, congr_hom F.w]

Goal state after:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯
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 : a'.base ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
inst✝ : (forget F).IsHomLift (g ≫ f) φ'
⊢ φ'.base = g ≫ f

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

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

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
⊢ lift s ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j

Tactic:
dsimp [coneFunctorEnrichedHom]

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
⊢ lift s ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) = s.π.app j
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
⊢ Function.Surjective (Fiber.inducedFunctor ⋯).obj

Tactic:
intro Y

Goal state after:
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ ∃ a, (Fiber.inducedFunctor ⋯).obj a = Y
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

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

Tactic:
obtain ⟨c⟩ : Nonempty C := IsFiltered.nonempty

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
c : C
⊢ Nonempty (Grothendieck F)
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
⊢ G.IsLeftDerivedFunctor β W ↔ IsIso (LF.leftDerivedLift α W G β)

Tactic:
rw [isLeftDerivedFunctor_iff_isRightKanExtension]

Goal state after:
C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
⊢ G.IsRightKanExtension β ↔ IsIso (LF.leftDerivedLift α W G β)
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
a : (F.obj X).obj
⊢ 1 • a = a

Tactic:
by
    change F.map (𝟙 X) a = a
    simp only [map_id, FintypeCat.id_apply]

Goal state after: