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

Goal state before:
pp: case hf
n : ℕ
⊢ Set.InjOn (fun k ↦ (↑k + 1) * π / (↑n + 1)) ↑(Finset.range n)

Tactic:
intro x hx y hy hxy
    field_simp at hxy
    aesop

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

Goal state before:
pp: L : PeriodPair
z : ℂ
hz : z ∉ L.lattice
⊢ ℘'[L] z ^ 2 = 4 * ℘[L] z ^ 3 - L.g₂ * ℘[L] z - L.g₃

Tactic:
by
  simpa [sub_eq_zero, relation, hz, sub_add] using congr($L.relation_eq_zero z)

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

Goal state before:
pp: x✝ : ℤ
⊢ fib (↑1 + x✝) = fib (↑1 - 1) * fib x✝ + fib ↑1 * fib (x✝ + 1)

Tactic:
by simp [add_comm]

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

Goal state before:
pp: ⊢ ψ * φ = -1

Tactic:
rw [mul_comm]

Goal state after:
⊢ φ * ψ = -1
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (n * k + r) / ↑(n * k + r) < L

Tactic:
rw [mul_comm]

Goal state after:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) < L
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))

pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
· intro x hx y hy hxy
      apply exp_monotone
      simp only [neg_le_neg_iff]
      gcongr

Goal state after:
case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (generator F)

Tactic:
generator

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (∐ fun X ↦ ∐ fun x ↦ projectiveSeparator C)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ n⌋₊ / c k ^ n) atTop (𝓝 1)

Tactic:
· refine tendsto_nat_floor_div_atTop.comp ?_
      exact tendsto_pow_atTop_atTop_of_one_lt (cone k)

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ULift.{v, w} α

Tactic:
exact ULift.up x

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ULift.{v, w} α

Tactic:
exact ULift.up x

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ g = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Tactic:
by
  refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
  rw [IsColimit.ι_map]
  simpa using! i.hom.2.w.symm

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

Goal state before:
pp: case h₀
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 α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
hb₁ : b ≠ v
⊢ Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

Tactic:
rw [Pi.ι_π_of_ne _ hb₁, comp_zero]

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
n : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) n

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

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a.hom = 0

Tactic:
rw [← pseudoZero_aux P a]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
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
⊢ (R.extMk f m hm hf).comp (Ext.mk₀ g) ⋯ = R'.extMk (f ≫ φ.hom.f n) m hm ⋯

Tactic:
by
  have := HasDerivedCategory.standard C
  ext
  have : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso n n (by lia)).inv =
      (f ≫ (R.cochainComplexXIso n n (by lia)).inv) ≫ φ.hom'.f n := by
    simp [φ.hom'_f n n rfl]
  simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, this]
  rw [Cocycle.fromSingleMk_postcomp _ (zero_add _) _ (by lia)
      (by simp [R.cochainComplex_d _ _ _ _ rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_postcomp,
    ← ShiftedHom.comp_mk₀ _ 0 rfl, ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]
  congr 3
  rw [Category.assoc, ← NatTrans.naturality, ← Category.assoc, ← Category.assoc]
  congr 1
  simpa only [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq,
    Functor.map_comp] using! DerivedCategory.Q.congr_map φ.ι'_comp_hom'.symm

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✝¹ : HasKernels C
inst✝ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this✝ : CreatesLimit (parallelPair f 0) P.ι
this : HasLimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
exact preservesLimit_of_createsLimit_and_hasLimit _ _

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ z = 0

Tactic:
← cancel_mono (L.objObjPreimageIso W).inv,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ z ≫ (L.objObjPreimageIso W).inv = 0 ≫ (L.objObjPreimageIso W).inv
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:
comp_smul,

Goal state after:
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✝
⊢ r • F.map f✝ ≫ α.app Y✝ = (r • α.app X✝) ≫ G.map f✝
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
⊢ ∀ (a : R), a • 0 = 0

Tactic:
intros
        ext
        apply smul_zero

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Group G
A : Action V G
g : G
⊢ A.ρ (g * g⁻¹) = 𝟙 A.V

Tactic:
mul_inv_cancel,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Group G
A : Action V G
g : G
⊢ A.ρ 1 = 𝟙 A.V
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g

Tactic:
by have w := comm g =≫ f.inv; simp at w; simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f

Tactic:
← hm

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ ((beckAlgebraCofork X).π ≫ m).f
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.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' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
X : (monadicAdjunction U).toMonad.Algebra
⊢ RegularEpi { f := X.a, h := ⋯ }

Tactic:
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ Epi q.leftTriple.rightToLeft ↔ Mono q.rightTriple.leftToRight

Tactic:
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ (∀ (k : C), Epi (q.leftTriple.rightToLeft.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.leftToRight.app k)
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝⁵ : L.Full
inst✝⁴ : L.Faithful
inst✝³ : G.Full
inst✝² : G.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft

Tactic:
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝⁵ : L.Full
inst✝⁴ : L.Faithful
inst✝³ : G.Full
inst✝² : G.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ (∀ (k : C), Epi (q.leftTriple.leftToRight.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.rightToLeft.app k)
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
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ t.leftToRight.app X =
    (F.leftUnitor.inv ≫
          inv (whiskerRight t.adj₂.counit F) ≫
            (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom).app
      X

Tactic:
dsimp [leftToRight]

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
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ 𝟙 (F.obj X) ≫
      t.adj₂.unit.app (F.obj X) ≫ 𝟙 (H.obj (G.obj (F.obj X))) ≫ (inv (whiskerRight t.adj₁.unit H)).app X ≫ 𝟙 (H.obj X) =
    𝟙 (F.obj X) ≫
      (inv (whiskerRight t.adj₂.counit F)).app X ≫
        𝟙 (F.obj (G.obj (H.obj X))) ≫ t.adj₁.counit.app (H.obj X) ≫ 𝟙 (H.obj X)
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h

Tactic:
by simp [-LeftExtension.w]

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

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.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 s.extension

Tactic:
by
        rw [rightZigzag]; bicategory

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

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

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

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Tactic:
refine
    le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj ((Subobject.pullback π(π₁, F.F)).obj X.rel)

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj
      ((Subobject.pullback (prod.map F.f (𝟙 Y.tgt))).obj Y.rel) ≤
    (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback π(π₁, G.F)).obj Y.rel)

case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback (prod.map G.f (𝟙 Z.tgt))).obj Z.rel) ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inl.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✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inl_ C C').map f✝¹ = (Sum.inl_ C C').map f✝

pp: case inr.inr
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✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝

Tactic:
· case inl x y f g => rw [((by assumption : IsDiscrete C).subsingleton x y).allEq f g]

Goal state after:
case inr.inr
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✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by
  ext <;> simp; ext <;> simp <;> (rw [← Category.assoc]; congr 1; simp)

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a

Tactic:
exact left_inv h

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
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i) ≫ ((diagram V F₁ F₂).obj (Opposite.op i)).map f = (eHomEquiv V) (τ.app i ≫ F₂.map f)

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
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i ≫ F₂.map f) = (eHomEquiv V) (τ.app j) ≫ ((diagram V F₁ F₂).map f.op).app j

Tactic:
· dsimp
      simp only [eHomEquiv_comp, tensorHom_def_assoc, MonoidalCategory.whiskerRight_id,
        ← unitors_equal, assoc, Iso.inv_hom_id_assoc, eHomWhiskerLeft]

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
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i ≫ F₂.map f) = (eHomEquiv V) (τ.app j) ≫ ((diagram V F₁ F₂).map f.op).app j
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
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫
    eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
      (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)

Tactic:
tensorHom_def_assoc

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
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
        (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
          (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)