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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
this : eval x (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0
⊢ eval x (U ℝ ↑n) = 0

Tactic:
refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
this : eval x (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0
⊢ (↑k + 1) * π / (↑n + 1) < π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
← cos_zero

Goal state after:
case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < cos 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
← cos_zero

Goal state after:
case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < cos 0
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
arithGeom_eq ha n

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (b - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)

Tactic:
arithGeom_eq ha n

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (0 - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ n) / (1 - a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ 2 * n / (2 * n).gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))

Tactic:
Nat.Coprime.gcd_mul_left_cancel n (by simp),

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ 2 * n / n.gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
rw [tsum_of_add_one_of_neg_add_one (by simpa using aux_summable_add hk z)
    (by simpa [sub_eq_add_neg] using aux_summable_sub hk z),
    tsum_mul_left, Summable.tsum_add (aux_summable_add hk z) (aux_summable_sub hk z)]

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) +
      (-1) ^ k * ↑k ! * (∑' (b : ℕ), (z + (↑b + 1)) ^ (-1 - ↑k) + ∑' (b : ℕ), (z - (↑b + 1)) ^ (-1 - ↑k)) =
    (-1) ^ k * ↑k ! *
      (∑' (n : ℕ), (z + ↑(↑n + 1)) ^ (-1 - ↑k) + (z + ↑0) ^ (-1 - ↑k) + ∑' (n : ℕ), (z + ↑(-(↑n + 1))) ^ (-1 - ↑k))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)

Tactic:
sub_eq_add_neg

Goal state after:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot + -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -((-1) ^ k * ↑k ! * z ^ (-1 + -↑k))
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: 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 := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
⊢ φ.Faithful

Tactic:
rwa [← isSeparator_iff_faithful_preadditiveCoyonedaObj]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ |∑ i ∈ Finset.range N, f ↑i + ∑' (i : ℕ), f ↑(i + N) - ∑ n ∈ Finset.range N, f ↑n| ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x

Tactic:
add_sub_cancel_left,

Goal state after:
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ |∑' (i : ℕ), f ↑(i + N)| ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case e'_3.e_f
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
x✝ : ℕ
⊢ f ↑(x✝ + N) = f ↑(x✝ + (N - 1) + 1)

Tactic:
congr 2

Goal state after:
case e'_3.e_f
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
x✝ : ℕ
⊢ x✝ + N = x✝ + (N - 1) + 1
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
⊢ ∀ (b : (filteredClosure f).FullSubcategory), ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = b.obj

Tactic:
rintro ⟨j, h⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
h : filteredClosure f j
⊢ ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := j, property := h }.obj
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
⊢ ∀ (b : (cofilteredClosure f).FullSubcategory),
    ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = b.obj

Tactic:
rintro ⟨j, h⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
h : cofilteredClosure f j
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := j, property := h }.obj
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
⊢ X.left ⟶ ((Comma.map α β).obj { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom }).left

Tactic:
exact Y.left.hom

Goal state after:
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
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ ((colimitHomIsoLimitYoneda' F A).inv ≫ ↾fun g ↦ colimit.ι F (op i) ≫ g) = limit.π (F.rightOp ⋙ yoneda.obj A) i

Tactic:
by
  rw [← dsimp% colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
  refine ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms =>
    ?_, ?_⟩
  · exact
      Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)
  · intro
    exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ R.cochainComplex.IsStrictlyGE 0

Tactic:
dsimp [cochainComplex]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ R.cochainComplex.IsStrictlyLE 0

Tactic:
dsimp [cochainComplex]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
⊢ Epi f

Tactic:
have : (⟦(p.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(𝟙 Q)⟧ := by
    rw [← hp] at hpbar
    exact hpbar

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
⊢ Epi f
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f + (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯
          (-↑m) ⋯ ⋯))

Tactic:
Cocycle.toSingleMk_add _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ +
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y) ≫
      (DerivedCategory.singleFunctor C 0).map g =
    DerivedCategory.Q.map φ.hom' ≫
      inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'

Tactic:
rw [Category.assoc, ← NatTrans.naturality, ← Category.assoc, ← Category.assoc]

Goal state after:
case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (inv (DerivedCategory.Q.map R.ι') ≫ (singleFunctor C 0 ⋙ DerivedCategory.Q).map g) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y' =
    (DerivedCategory.Q.map φ.hom' ≫ inv (DerivedCategory.Q.map R'.ι')) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'
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
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.ι.f 0) ≫ F.map (P.cocomplex.d 0 1) = 0

Tactic:
← F.map_comp,

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
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.ι.f 0 ≫ P.cocomplex.d 0 1) = 0
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ (r • α.app Y) = (r • α.app X) ≫ G.map f

Tactic:
by
            intros
            rw [comp_smul, smul_comp, α.naturality]

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map (X✝.ρ g) ≫ F.map f.hom = F.map f.hom ≫ F.map (Y✝.ρ g)

Tactic:
← F.map_comp,

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map (X✝.ρ g ≫ f.hom) = F.map f.hom ≫ F.map (Y✝.ρ g)
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ h⁻¹ᘁ

Tactic:
rw [← SingleObj.inv_as_inv]; rfl

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ h⁻¹

Tactic:
rw [← SingleObj.inv_as_inv]; rfl

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

Goal state before:
pp: case refine_1
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)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z

Tactic:
← F.map_comp,

Goal state after:
case refine_1
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)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ { g // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g } ≃
    { z // F.map (U.map (adj₁.counit.app X)) ≫ z = adj₁.counit.app ((U ⋙ F).obj X) ≫ z }

Tactic:
by
      apply (adj₁.homEquiv _ _).symm.subtypeEquiv
      intro g
      rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit,
        adj₁.homEquiv_counit, adj₁.homEquiv_counit, F.map_comp, assoc, U.map_comp, F.map_comp,
        assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
      apply eq_comm

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

Goal state before:
pp: case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (η.vcomp θ) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp only [mk_vcomp, whiskerLeft_comp]

Goal state after:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ ((preinclusion B).map { as := p } ◁ η.mk ≫ (preinclusion B).map { as := p } ◁ θ.mk) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f g : a ⟶ b
h i : b ⟶ c
η✝ : f ⟶ g
η : Hom₂ f g
θ✝ : h ⟶ i
θ : Hom₂ h i
⊢ Quot.map (Hom₂.whisker_left f) ⋯ (Quot.mk Rel θ) ≫ Quot.map (Hom₂.whisker_right i) ⋯ (Quot.mk Rel η) =
    Quot.map (Hom₂.whisker_right h) ⋯ (Quot.mk Rel η) ≫ Quot.map (Hom₂.whisker_left g) ⋯ (Quot.mk Rel θ)

Tactic:
exact Quot.sound (Rel.whisker_exchange η θ)

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 H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ θ.naturality (f ≫ g) ⊗≫
        (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c)

Tactic:
by
      rw [η.naturality_comp]
      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
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]

Goal state after:
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'
⊢ (F.mapComp f g ▷ η.app c ≫
          (α_ (F.map f) (F.map g) (η.app c)).hom ≫
            F.map f ◁ η.naturality g ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ≫
                η.naturality f ▷ G.map g ≫ (α_ (η.app a) (G.map f) (G.map g)).hom) ▷
        h ≫
      (α_ (η.app a) (G.map f ≫ G.map g) h).hom =
    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
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))

Tactic:
by
      rw [η.naturality_comp]
      bicategory

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ PFun.toSubtype (fun x ↦ x ≠ Z.point) (f ≫ g).toFun ∘ Subtype.val =
    PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val ≫
      PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val

Tactic:
by
    refine PFun.ext fun ⟨a, ha⟩ ⟨c, hc⟩ =>
      (PFun.mem_toSubtype_iff.trans ?_).trans Part.mem_bind_iff.symm
    suffices c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a) from
      ⟨by aesop, by simp; grind⟩
    rintro rfl
    refine ⟨fun h => hc.symm <| g.map_point ▸ congr_arg g.toFun h, hc.symm⟩

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ b ∈ f.fix a

Tactic:
by
  rw [PFun.mem_fix_iff]
  exact Or.inl hb

Goal state after: