mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
Finset.range_eq_Ico

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Icc 0 ↑N)
integrable : IntegrableOn f (Ioi 0) volume
nonneg : ∀ t ∈ Ioi 0, 0 ≤ f t
⊢ ∑ n ∈ Finset.Ico 0 N, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi 0, f x
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: 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

Tactic:
induction h with

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

Goal state before:
pp: 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

Tactic:
induction h with

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
x✝ : IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A)
h₁ : IsFiltered (CostructuredArrow yoneda A)
h₂ : FinallySmall (CostructuredArrow yoneda A)
⊢ PreservesFiniteLimits A

case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall (CostructuredArrow yoneda A)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : R.Final
⊢ (snd L R).Final

Tactic:
have := R.final_iff_isFiltered_structuredArrow.mp inferInstance
  exact final_snd_of_isFiltered_structuredArrow L R

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteLimits (functor C)

Tactic:
rw [functor]
  have : PreservesFiniteLimits (F C) := by rw [F]; infer_instance
  have : PreservesFiniteLimits (G C) := by rw [G]; apply preservesFiniteLimits_rightOp
  have : PreservesFiniteLimits (H C) :=
    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding _
  infer_instance

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Tactic:
· intro
    exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)

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 : Over P
hf : f.hom = 0
⊢ biprod.fst ≫ 0 = biprod.snd ≫ (Over.mk 0).hom

Tactic:
Over.coe_hom,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ biprod.fst ≫ 0 = biprod.snd ≫ 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ P.isoModSerre (Abelian.factorThruImage f)

Tactic:
by
  rw [isoModSerre_iff_of_epi]
  exact P.prop_of_iso
    (asIso (kernel.map _ f (𝟙 _) (Abelian.image.ι f) (by simp))).symm hf

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 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
⊢ ∀ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0

Tactic:
z

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 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
⊢ L.map z ≫ L.map f = 0 → L.map z = 0
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 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
⊢ ∀ (g : W ⟶ L.obj X), g ≫ L.map f = 0 → g = 0

Tactic:
z

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 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
⊢ z ≫ L.map f = 0 → z = 0
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
hf : P.epiModSerre f
Z : C
⊢ ∀ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0

Tactic:
z

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
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
⊢ L.map f ≫ L.map z = 0 → L.map z = 0
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : X
f : ⟨PUnit.unit, a⟩ ⟶ ⟨PUnit.unit, b⟩
⊢ P (homOfPair (ActionCategory.back ⟨PUnit.unit, b⟩) ↑f) = P f

Tactic:
rcases f with ⟨g : G, h : g • a = b⟩

Goal state after:
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : X
g : G
h : g • a = b
⊢ P (homOfPair (ActionCategory.back ⟨PUnit.unit, b⟩) ↑⟨g, h⟩) = P ⟨g, h⟩
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
⊢ ∀ (g : L.obj Y ⟶ W), L.map f ≫ g = 0 → g = 0

Tactic:
z

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
⊢ L.map f ≫ z = 0 → z = 0
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
g : G
⊢ ∀ (y : G),
    ⟨fun b ↦ F.map (homOfPair b (g * y)), g * y⟩ =
      ⟨fun b ↦ F.map (homOfPair b g), g⟩ * ⟨fun b ↦ F.map (homOfPair b y), y⟩

Tactic:
h

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
g h : G
⊢ ⟨fun b ↦ F.map (homOfPair b (g * h)), g * h⟩ = ⟨fun b ↦ F.map (homOfPair b g), g⟩ * ⟨fun b ↦ F.map (homOfPair b h), h⟩
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✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ ((res V f).map g₁).hom = ((res V f).map g₂).hom

Tactic:
h

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ ((res V f).map g₂).hom = ((res V f).map g₂).hom
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
this : Abelian D := abelian L P
⊢ PreservesFiniteLimits L

Tactic:
((Functor.preservesFiniteLimits_tfae L).out 3 2 :)

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
this : Abelian D := abelian L P
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
⊢ (whiskeringLeft L P E).essImage F → P.isoModSerre.IsInvertedBy F.obj

Tactic:
rintro ⟨G, ⟨e⟩⟩

Goal state after:
case refine_1
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
G : D ⥤ₑ E
e : (whiskeringLeft L P E).obj G ≅ F
⊢ P.isoModSerre.IsInvertedBy F.obj
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_2
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
⊢ (beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ } = s.π

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},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }

Tactic:
· ext
      simpa [← T.η.naturality_assoc, T.left_unit_assoc] using! T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁

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},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫
        adj₂.unit.app (U'.1 (F.obj X)) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X)))) ((adj₂.homEquiv Y (F.obj X)).symm f ≫ F.map (adj₁.unit.app X))

Tactic:
← adj₂.homEquiv_naturality_right_symm,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫
        adj₂.unit.app (U'.1 (F.obj X)) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))
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)
X : B
Y Y' : A
g : Y ⟶ Y'
⊢ ∀ (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g

Tactic:
h

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
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)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (constructLeftAdjointEquiv R F' adj₁ adj₂ h✝ Y' X) (h ≫ g) =
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h✝ Y X) h ≫ R.map g
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
⊢ ∀ (g_1 : L.obj Y ⟶ Y'),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y').symm (L.map g ≫ g_1) =
      g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h Y Y').symm g_1

Tactic:
h

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ X Y').symm (L.map g ≫ h) =
    g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ Y Y').symm h
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f ≫ g = f' ≫ g

Tactic:
h

Goal state after:
B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g = f' ≫ g
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g' = f ≫ g'

Tactic:
h

Goal state after:
B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g' = f' ≫ g'
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f ≫ g = f ≫ g'

Tactic:
h

Goal state after:
B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f ≫ g' = f ≫ g'
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f' ≫ g' = f' ≫ g

Tactic:
h

Goal state after:
B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f' ≫ g' = f' ≫ g'
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
⊢ ∀ {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
h

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
⊢ ∀ (η : f ⟶ g) (θ : g ⟶ h), Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 : b ⟶ c
⊢ ∀ {h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
h

Goal state after:
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),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

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

Tactic:
h

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
    (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

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

Tactic:
simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]

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)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit

Tactic:
adj.left_triangle

Goal state after:
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)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit
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 : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift

Tactic:
adj.left_triangle

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ⊗≫ τ ⊗≫ 𝟙 s.lift
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ (Functor.sigma F).map (SigmaHom.mk f) ≫ SigmaHom.mk ((α ⟨i, Y✝⟩.fst).app ⟨i, Y✝⟩.snd) =
    SigmaHom.mk ((α ⟨i, X⟩.fst).app ⟨i, X⟩.snd) ≫ (Functor.sigma G).map (SigmaHom.mk f)

Tactic:
change SigmaHom.mk _ = SigmaHom.mk _

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ SigmaHom.mk ((F ⟨i, X⟩.fst).map f ≫ (α ⟨i, Y✝⟩.fst).app ⟨i, Y✝⟩.snd) =
    SigmaHom.mk ((α ⟨i, X⟩.fst).app ⟨i, X⟩.snd ≫ (G ⟨i, X⟩.fst).map f)
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: ⊢ PartialFun ⥤ Pointed

Tactic:
exact
    { obj := fun X => ⟨(Option X), none⟩
      map := fun f => ⟨Option.elim' none fun a => (f a).toOption, rfl⟩
      map_id := fun X => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => (by
        dsimp [CategoryStruct.id]
        convert! Part.some_toOption a)
      map_comp := fun f g => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => by
        dsimp [CategoryStruct.comp]
        rw [Part.bind_toOption g (f a), Option.elim'_eq_elim] }

Goal state after: