mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: n : ℕ
⊢ ‖![1, ↑n + 1]‖ = ↑n + 1

Tactic:
simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one]
  norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: n : ℕ
⊢ ‖![1, -(↑n + 1)]‖ = ↑n + 1

Tactic:
simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one]
  norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) * ↑z / ↑‖x‖ + ↑(x 1) / ↑‖x‖) * ↑‖x‖

Tactic:
← add_div,

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) * ↑z + ↑(x 1)) / ↑‖x‖ * ↑‖x‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
by
  refine (summand_bound z hk x).trans (mul_le_mul_of_nonneg_right ?_ (by positivity))
  exact Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz)
    (neg_nonpos.mpr hk)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case e'_3
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| = |eval x ((⇑derivative)^[k] (T ℝ (-n)))|

Tactic:
T_neg

Goal state after:
case e'_3
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| = |eval x ((⇑derivative)^[k] (T ℝ n))|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case e'_4
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ eval 1 ((⇑derivative)^[k] (T ℝ n)) = eval 1 ((⇑derivative)^[k] (T ℝ (-n)))

Tactic:
T_neg

Goal state after:
case e'_4
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ eval 1 ((⇑derivative)^[k] (T ℝ n)) = eval 1 ((⇑derivative)^[k] (T ℝ n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
    (𝓝 (logDeriv (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) x))

Tactic:
by
  refine logDeriv_tendsto isOpen_compl_range_intCast hx
      HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_
  · filter_upwards with n using by fun_prop
  · simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]
    exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
by
    calc _ = fib (m + n) + fib (m + n + 1) := by grind [fib_add_two]
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib ((m + 1 : ℕ) + n) := by
        rw [fib_natCast_add]; grind
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib m * fib n +
          fib (m + 1) * fib (n + 1) := by rw [fib_natCast_add]; grind
      _ = _ := by grind [fib_add_two]

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ↑π * (↑π * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))

Tactic:
have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))
  have h1 := cot_series_rep' hz
  simp only [one_div, Nat.cast_add, Nat.cast_one] at *
  rw [h0, ← h1]
  ring

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n % k = 0
⊢ False

Tactic:
← Nat.dvd_iff_mod_eq_zero,

Goal state after:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬k ∣ n
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + ↑n) ^ (k + 1) = (z + ↑n) ^ (-1 - ↑k)

Tactic:
rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; lia, zpow_neg_coe_of_pos _ (by lia),
    one_div]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case hg
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ IntegrableOn (fun x ↦ f x * g (x - 1)) (Ico ↑a ↑b) volume

Tactic:
· apply Integrable.mono_measure _ (volume.restrict_mono_set Ico_subset_Icc_self)
    apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left
    apply MonotoneOn.memLp_isCompact isCompact_Icc
    intro _ _ _ _ _
    apply hg <;> grind

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

Goal state before:
pp: case refine_2
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 < ε
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < d

Tactic:
filter_upwards [A ε εpos, Ioi_mem_atTop 0] with n hn (npos : 0 < n)

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
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 < d
Module: Mathlib.CategoryTheory.Limits.Indization.Products

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a ↦ ⋯.presentation.F ⋙ yoneda
⊢ IsIndObject (∏ᶜ f)

Tactic:
suffices (∏ᶜ f ≅ colimit (pointwiseProduct F)) from
    (isIndObject_colimit _ _ (fun i => h _)).map this.inv

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a ↦ ⋯.presentation.F ⋙ yoneda
⊢ ∏ᶜ f ≅ colimit (pointwiseProduct F)
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
⊢ PreservesFiniteLimits (tensorObj G)

Tactic:
by
  have := preservesInjectiveObjects G hG
  have : (tensorObj G).PreservesMonomorphisms :=
    (tensorObj G).preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects
      (tensorObjPreadditiveCoyonedaObjAdjunction G)
  have : PreservesBinaryBiproducts (tensorObj G) :=
    preservesBinaryBiproducts_of_preservesBinaryCoproducts _
  have : (tensorObj G).Additive := Functor.additive_of_preservesBinaryBiproducts _
  have : (tensorObj G).PreservesHomology :=
    (tensorObj G).preservesHomology_of_preservesMonos_and_cokernels
  exact (tensorObj G).preservesFiniteLimits_of_preservesHomology

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Abelian D
P : ObjectProperty C
inst✝² : P.IsSerreClass
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel

Tactic:
refine ⟨P.le_kernel_of_isoModSerre_isInvertedBy F, fun hF X Y f ⟨h₁, h₂⟩ ↦ ?_⟩
  have : Mono (F.map f) :=
    (((ShortComplex.mk _ _ (kernel.condition f)).exact_of_f_is_kernel
      (kernelIsKernel f)).map F).mono_g (((hF _ h₁).eq_of_src _ _))
  have : Epi (F.map f) :=
    (((ShortComplex.mk _ _ (cokernel.condition f)).exact_of_g_is_cokernel
      (cokernelIsCokernel f)).map F).epi_f (((hF _ h₂).eq_of_tgt _ _))
  exact isIso_of_mono_of_epi (F.map f)

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (η.app c)) → Mono η

Tactic:
· intro _
    apply NatTrans.mono_of_mono_app

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
h : H.FullyFaithful
this✝ : H.Full
this : H.Faithful
⊢ IsIso t.adj₁.unit

Tactic:
t.isIso_unit_iff_isIso_counit

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
h : H.FullyFaithful
this✝ : H.Full
this : H.Faithful
⊢ IsIso t.adj₂.counit
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝² : G.Full
inst✝¹ : G.Faithful
inst✝ : H.PreservesEpimorphisms
X : C
x✝ : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
⊢ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)

Tactic:
rw [← map_rightToLeft_app]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝² : G.Full
inst✝¹ : G.Faithful
inst✝ : H.PreservesEpimorphisms
X : C
x✝ : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
⊢ Epi (G.map (t.rightToLeft.app X))
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
← leftToRight_app_obj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.leftToRight.app (G.obj X))
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id X)) f = f

Tactic:
by
    rintro f g ⟨η⟩
    exact Quot.sound (Rel.id_comp η)

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

Goal state before:
pp: case f
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
a✝ : Hom₂ g h
⊢ Quot.lift (liftHom₂ F) ⋯ (f ◁ Quot.mk Rel a✝) =
    (Iso.refl (liftHom F (f ≫ g))).hom ≫
      liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝) ≫ (Iso.refl (liftHom F (f ≫ h))).inv

pp: case h
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯

Tactic:
· cat_disch

Goal state after:
case h
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫
      (α_ (η.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) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)

Tactic:
by
          bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ Γ.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) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
by
          bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫
      (α_ (η.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) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)

Tactic:
by
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : B ⥤ᵒᵖᴸ C
θ : OplaxTrans G H
a b c : B
a' : C
f : a' ⟶ G.obj a
g : a ⟶ b
h : b ⟶ c
⊢ f ◁ θ.naturality (g ≫ h) ≫ f ◁ θ.app a ◁ H.mapComp g h =
    f ◁ G.mapComp g h ▷ θ.app c ≫
      f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫
        f ◁ G.map g ◁ θ.naturality h ≫
          f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫
            f ◁ θ.naturality g ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom

Tactic:
by
  simp_rw [← whiskerLeft_comp, naturality_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ η.naturality (f ≫ g) ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
    F.mapComp f g ▷ η.app c ▷ h ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
        (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
          F.map f ◁ η.naturality g ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                η.naturality f ▷ G.map g ▷ h ≫
                  (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom

Tactic:
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_comp]; simp

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

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) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
by
          bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫
      (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
        η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)

Tactic:
by
          bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        θ.naturality f ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫ θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)

Tactic:
by
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ rightZigzag t.unit ε) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
by
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
by
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)

Tactic:
by
          bicategory

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

Goal state before:
pp: α β : PartialFun
e : α ≃ β
⊢ ↑(⇑e ∘ ⇑e.symm) = 𝟙 β

Tactic:
simp only [Equiv.self_comp_symm, PFun.coe_id]
    rfl

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:
rw [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.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩) ↔ some b = (partialFunToPointed.map f).toFun (some a)

Tactic:
classical
            refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
            rw [Subtype.ext_iff] at h
            dsimp at h
            rw [h]
            rw [← Part.mem_toOption, mem_def] at hw
            exact hw.symm

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ (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✝

Tactic:
by
      fapply Types.Limit.mk.{v, v}
      · intro j
        refine eqToHom ?_ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ?_ <;> simp
      · intro j j' h
        dsimp [Functor.comp_obj, homDiagram_obj]
        simp only [Functor.map_comp, eqToHom_map, ← Functor.comp_map, Category.assoc, eqToHom_trans,
          eqToHom_trans_assoc]
        have := congr($((s.π.naturality h).symm).toFunctor)
        dsimp at this
        rw [Functor.id_comp] at this
        rw [Functor.congr_hom this f]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
⊢ IsLimit c

Tactic:
suffices IsIso (limit.lift _ c) from
    IsLimit.ofIsoLimit (limit.isLimit _)
      (Cone.ext (asIso (limit.lift _ c) :)).symm

Goal state after:
C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
⊢ IsIso (limit.lift G c)
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ F.HasPointwiseLeftDerivedFunctorAt W X

Tactic:
hasPointwiseLeftDerivedFunctorAt_iff F W.Q W

Goal state after:
C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)