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

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cos θ) (T ℂ n) = cos (↑n * θ)

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf

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

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : ∑ i ∈ range n, (f i - f (i + 1)) ≤ ∑ i ∈ range n, (g i - g (i + 1))
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹

Tactic:
rw [Finset.sum_range_sub', Finset.sum_range_sub'] at hf

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : f 0 - f n ≤ g 0 - g n
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant
  have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx
  refine ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), ?_⟩
  rw [← Filter.tendsto_add_atTop_iff_nat 1]
  exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩

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

Goal state before:
pp: case r_pos
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ 0 < ↑r

Tactic:
exact ENNReal.coe_pos.mpr hr0

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ ↑n

Tactic:
by
  refine ⟨fun hP => ?_, fun hP => by simp [hP]⟩
  apply (coeff_eq_iff_of_forall_abs_le_one hPdeg hPbnd).mp
  suffices hPdeg' : n ≤ P.degree by
    replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'
    rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP
  lift P.degree to ℕ with d hd
  · contrapose! hP
    rw [degree_eq_bot.mp hP, leadingCoeff_zero]
    positivity
  replace hP := ge_of_eq hP
  contrapose! hP
  have : d - 1 < n - 1 := by grind [Nat.cast_withBot, WithBot.coe_le_coe, WithBot.coe_lt_coe]
  calc P.leadingCoeff ≤ 2 ^ (d - 1) := leadingCoeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd
  _ < 2 ^ (n - 1) := by gcongr; norm_num

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

Goal state before:
pp: L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z : ℂ
⊢ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝[≠] z] L.relation

Tactic:
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds
    (L.compl_lattice_sdiff_singleton_mem_nhds _)] with w hw hw'

Goal state after:
L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
hw' : w ∈ (↑L.lattice \ {z})ᶜ
⊢ ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ AnalyticAt ℂ L.relation 0

Tactic:
refine .of_meromorphicOrderAt_pos (one_pos.trans_le ?_) (by simp [relation])
  suffices 7 ≤ meromorphicOrderAt (L.relation * id ^ 6) 0 by
    rw [meromorphicOrderAt_mul (by fun_prop) (by fun_prop),
      meromorphicOrderAt_pow (by fun_prop)] at this
    rw [← WithTop.add_le_add_iff_right (z := 6) (by simp)]
    simpa [-add_le_add_iff_left_of_ne_top] using! this
  rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop)]
  refine ENat.monotone_map_iff.mpr Nat.mono_cast
    ((natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (by fun_prop)).mpr fun i hi₁ ↦ ?_)
  by_cases hi₂ : Odd i
  · simpa [← CharZero.eq_neg_self_iff, hi₂, (show Even 6 by decide).neg_pow] using!
      (iteratedDeriv_comp_neg i (L.relation * id ^ 6) 0 :)
  by_cases hi₃ : i = 0
  · simp [hi₃]
  by_cases hi₄ : i = 6
  · exact hi₄ ▸ L.iteratedDeriv_six_relation_mul_id_pow_six
  rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]
  simp_rw [pow_succ (_ + _), pow_succ (_ - _), pow_zero, one_mul]
  simp (discharger := fun_prop) only [iteratedDeriv_fun_add, iteratedDeriv_fun_sub,
    iteratedDeriv_fun_mul, iteratedDeriv_const, iteratedDeriv_fun_pow_zero,
    iteratedDeriv_derivWeierstrassPExcept_self, iteratedDeriv_weierstrassPExcept_self]
  obtain rfl | rfl : i = 2 ∨ i = 4 := by grind
  · simp [Finset.sum_range_succ]
  · simp [Finset.sum_range_succ, show Nat.choose 4 2 = 6 by rfl, g₂]; ring

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

Goal state before:

Tactic:
_ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp

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

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

Tactic:
exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-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)

Tactic:
← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)),

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-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 ! * z ^ (-1 - ↑k) =
    (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
Module: Mathlib.CategoryTheory.Generator.Indization

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (ObjectProperty.ofObj Ind.yoneda.obj).IsSeparating

Tactic:
refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_
  exact colimit.hom_ext (fun i => by simp [← Category.assoc, h])

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
f : (preadditiveCoyonedaObj G).obj A ⟶ (preadditiveCoyonedaObj G).obj B
this : Epi (Sigma.desc fun f ↦ f)
h : (kernel.ι (Sigma.desc fun m ↦ m) ≫ Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) = 0
⊢ (preadditiveCoyonedaObj G).map (epiDesc (Sigma.desc fun m ↦ m) (Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) h) = f

Tactic:
ext q

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
f : (preadditiveCoyonedaObj G).obj A ⟶ (preadditiveCoyonedaObj G).obj B
this : Epi (Sigma.desc fun f ↦ f)
h : (kernel.ι (Sigma.desc fun m ↦ m) ≫ Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) = 0
q : ↑((preadditiveCoyonedaObj G).obj A)
⊢ (ModuleCat.Hom.hom
        ((preadditiveCoyonedaObj G).map
          (epiDesc (Sigma.desc fun m ↦ m) (Sigma.desc fun m ↦ (ConcreteCategory.hom f) m) h)))
      q =
    (ModuleCat.Hom.hom f) q
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
⊢ IsTrans (Over P) (PseudoEqual P)

Tactic:
refine ⟨fun f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩ ↦ ?_⟩
  refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
    epi_comp _ _, epi_comp _ _, ?_⟩
  rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
a : Over S.X₁
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
rw [← ha'] at ha

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
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⟧
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⟧

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom) (by
      simp only [Category.assoc]
      exact comm)

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
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

Goal state before:
pp: case right
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.epiModSerre f

Tactic:
· exact CokernelCofork.IsColimit.isZero_of_epi
      (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ CreatesLimit (parallelPair f 0) P.ι

Tactic:
fapply createsLimitFullSubcategoryInclusion'

Goal state after:
case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ Cone (parallelPair f 0 ⋙ P.ι)

case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit ?c

case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P (Cone.pt ?c)
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
⊢ (toEndHom N) n = 𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))

Tactic:
apply Action.hom_ext
  ext (x : G ⧸ N)
  induction x using Quotient.inductionOn
  exact Quotient.sound ((QuotientGroup.leftRel_apply).mpr <| by simpa)

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
⊢ Mono f ↔ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
by
  have := preservesMonomorphisms L P
  have := Localization.essSurj_mapArrow L P.isoModSerre
  refine ⟨fun _ ↦ ?_, ?_⟩
  · suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Mono (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩
    intro X Y f hf
    rw [mono_map_iff L P] at hf
    refine ⟨_, _, Abelian.image.ι f, inferInstance, ⟨Iso.symm ?_⟩⟩
    have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_factorThruImage
    exact Arrow.isoMk (asIso (L.map (Abelian.factorThruImage f))) (Iso.refl _)
      (by simp [← L.map_comp])
  · rintro ⟨X', Y', f', _, ⟨e⟩⟩
    exact ((MorphismProperty.monomorphisms D).arrow_mk_iso_iff e).1
      (by simpa using inferInstanceAs (Mono (L.map f')))

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g ≫ η F = η F ≫ (𝟙_ (Action W G)).ρ g

Tactic:
by
        dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
        rw [map_id, Category.id_comp, Category.comp_id]

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), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Epi (η.app c)) → Epi η

Tactic:
· intros
    apply NatTrans.epi_of_epi_app

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    Quot.map (Hom₂.whisker_left (𝟙 a)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.left_unitor f), inv := Quot.mk Rel (Hom₂.left_unitor_inv f), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        η ≫
          { hom := Quot.mk Rel (Hom₂.left_unitor g), inv := Quot.mk Rel (Hom₂.left_unitor_inv g), hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.inv

Tactic:
rintro a b f g ⟨η⟩

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ Quot.map (Hom₂.whisker_left (𝟙 a)) ⋯ (Quot.mk Rel η) =
    { hom := Quot.mk Rel (Hom₂.left_unitor f), inv := Quot.mk Rel (Hom₂.left_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      Quot.mk Rel η ≫
        { hom := Quot.mk Rel (Hom₂.left_unitor g), inv := Quot.mk Rel (Hom₂.left_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    Quot.map (Hom₂.whisker_right (𝟙 b)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.right_unitor f), inv := Quot.mk Rel (Hom₂.right_unitor_inv f), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        η ≫
          { hom := Quot.mk Rel (Hom₂.right_unitor g), inv := Quot.mk Rel (Hom₂.right_unitor_inv g), hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.inv

Tactic:
rintro a b f g ⟨η⟩

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ Quot.map (Hom₂.whisker_right (𝟙 b)) ⋯ (Quot.mk Rel η) =
    { hom := Quot.mk Rel (Hom₂.right_unitor f), inv := Quot.mk Rel (Hom₂.right_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      Quot.mk Rel η ≫
        { hom := Quot.mk Rel (Hom₂.right_unitor g), inv := Quot.mk Rel (Hom₂.right_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.inv
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 : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ η.naturality f ▷ h ≫ (η.app a ◁ G.map₂ β) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
whisker_assoc

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
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 : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
by
  rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]

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
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
        F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
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).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u

Tactic:
rw [IsKan.fac_assoc]

Goal state after:
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).hom ≫ sτ.unit ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ C a'

Tactic:
apply hbase

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ Sum.inl b ∈ f a'
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X

pp: case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y

Tactic:
· ext x
      apply (h1 _ _).mp
      use f x, (hg _).2, (hf _).2

Goal state after:
case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C
f : x ⟶ y
⊢ (Sum.inl_ C C').obj x = (Sum.inl_ C C').obj y

Tactic:
(by assumption : IsDiscrete C).eq_of_hom f

Goal state after:
case inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C
f : x ⟶ y
⊢ (Sum.inl_ C C').obj y = (Sum.inl_ C C').obj y