mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
n : ℕ
g : J.cocomplex.X n ⟶ I.cocomplex.X n
g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1)
w : J.cocomplex.d n (n + 1) ≫ g' = g ≫ I.cocomplex.d n (n + 1)
⊢ { X₁ := J.cocomplex.X n, X₂ := J.cocomplex.X (n + 1), X₃ := J.cocomplex.X (n + 2), f := J.cocomplex.d n (n + 1),
          g := J.cocomplex.d (n + 1) (n + 2), zero := ⋯ }.f ≫
      g' ≫ I.cocomplex.d (n + 1) (n + 2) =
    0

Tactic:
simp [reassoc_of% w]

Goal state after:
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
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso (F.toRightDerivedZero.app X)

Tactic:
(InjectiveResolution.self X).toRightDerivedZero_eq F

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
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso
    ((InjectiveResolution.self X).toRightDerivedZero' F ≫
      (CochainComplex.isoHomologyπ₀
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex)).hom ≫
        ((InjectiveResolution.self X).isoRightDerivedObj F 0).inv)
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:
inv_mul_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.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (x y : R) (b : X ⟶ Y), (x * y) • b = x • y • b

Tactic:
intros; ext; exact mul_smul _ _ _

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

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (r s : R) (x : X ⟶ Y), (r + s) • x = r • x + s • x

Tactic:
intros; ext; exact add_smul _ _ _

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
x✝ : PreservesColimitsOfShape J (F ⋙ H)
K : J ⥤ D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
⊢ PreservesColimit K H

Tactic:
refine preservesColimit_of_preserves_colimit_cocone
    ((IsColimit.precomposeInvEquiv iso _).symm
      (isColimitOfPreserves F (colimit.isColimit (K ⋙ G)))) ?_

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
x✝ : PreservesColimitsOfShape J (F ⋙ H)
K : J ⥤ D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
⊢ IsColimit (H.mapCocone ((Cocone.precompose iso.inv).obj (F.mapCocone (colimit.cocone (K ⋙ 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)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ (adj₁.homEquiv ((𝟭 B).obj (L.obj Y)) (F.obj (U.obj (F.obj X)))) (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      (adj₁.homEquiv ((𝟭 B).obj (L.obj Y)) (F.obj (U.obj (F.obj X)))) (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
adj₁.homEquiv_unit,

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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      (adj₁.homEquiv ((𝟭 B).obj (L.obj Y)) (F.obj (U.obj (F.obj X)))) (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))
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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      (adj₁.homEquiv ((𝟭 B).obj (L.obj Y)) (F.obj (U.obj (F.obj X)))) (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
adj₁.homEquiv_unit,

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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))
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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
adj₁.homEquiv_unit,

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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ η'.mk ▷ h ≫
      (α_ ((preinclusion B).map { as := p }) g✝ h).inv ≫
        (normalizeIso p g✝).hom ▷ h ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      eqToHom ⋯

Tactic:
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]

Goal state after:
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
⊢ (η ≫ θ) ≫ ι ≅ η ≫ θ ≫ ι

Tactic:
by
  exact isoMk (fun a ↦ α_ (η.app a) (θ.app a) (ι.app a)) <| by
    intro a b f
    dsimp only [comp_app, comp_naturality]
    bicategory

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

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
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
⊢ ∀ (τ : t.ofCompId ⟶ s), τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
τ

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s✝ t✝ : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
τ : t.ofCompId ⟶ s
⊢ τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
⊢ ∀ (τ : t.ofIdComp ⟶ s), τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
τ

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
τ : t.ofIdComp ⟶ s
⊢ τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
⊢ ∀ (s : LeftLift f g) (τ : t.ofIdComp ⟶ s), τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
by
    intro s τ
    ext
    apply P.hom_ext
    simp [← LeftLift.w τ]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
s : RightLift f g
⊢ ∀ (τ : s ⟶ t.ofIdComp), τ = t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))

Tactic:
τ

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
s : RightLift f g
τ : s ⟶ t.ofIdComp
⊢ τ = t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))
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 =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift

Tactic:
by
          rw [leftZigzag]; bicategory

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

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

Tactic:
by
          rw [leftZigzag]; bicategory

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

Goal state before:
pp: X✝ Y✝ Z✝ : PartialFun
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
o : { X := Option X✝, point := none }.X
a : X✝
⊢ { toFun := Option.elim' none fun a ↦ ((f ≫ g) a).toOption, map_point := ⋯ }.toFun (some a) =
    ({ toFun := Option.elim' none fun a ↦ (f a).toOption, map_point := ⋯ } ≫
          { toFun := Option.elim' none fun a ↦ (g a).toOption, map_point := ⋯ }).toFun
      (some a)

Tactic:
by
        dsimp [CategoryStruct.comp]
        rw [Part.bind_toOption g (f a), Option.elim'_eq_elim]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
⊢ b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯

Tactic:
obtain ⟨h₁, h₂⟩ := h
        grind [WellFounded.fixF_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ▷ Y₁ ≫ X₂ ◁ g)

Tactic:
exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y : C
⊢ ((tensorBifunctor L W ε).map ε.inv).app (L'.obj Y) ≫
      (Lifting.iso L' W (tensorLeft (𝟙_ C) ⋙ L') ((tensorBifunctor L W ε).obj (L'.obj (𝟙_ C)))).hom.app Y ≫
        L'.map (λ_ Y).hom ≫ 𝟙 (L.obj Y) ≫ 𝟙 (L'.obj Y) =
    ((tensorBifunctor L W ε).map (ε' L W ε).inv).app (L'.obj Y) ≫ (μ L W ε (𝟙_ C) Y).hom ≫ L'.map (λ_ Y).hom

Tactic:
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y : C
⊢ ((tensorBifunctor L W ε).map ε.inv).app (L'.obj Y) ≫
      (μ L W ε (𝟙_ C) Y).hom ≫ L'.map (λ_ Y).hom ≫ 𝟙 (L'.obj Y) ≫ 𝟙 (L'.obj Y) =
    ((tensorBifunctor L W ε).map (ε' L W ε).inv).app (L'.obj Y) ≫ (μ L W ε (𝟙_ C) Y).hom ≫ L'.map (λ_ Y).hom
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X : C
⊢ ((tensorBifunctor L W ε).obj (L'.obj X)).map ε.inv ≫
      (Lifting.iso L' W (tensorRight (𝟙_ C) ⋙ L') ((tensorBifunctor L W ε).flip.obj (L'.obj (𝟙_ C)))).hom.app X ≫
        L'.map (ρ_ X).hom ≫ 𝟙 (L.obj X) ≫ 𝟙 (L'.obj X) =
    ((tensorBifunctor L W ε).obj (L'.obj X)).map (ε' L W ε).inv ≫ (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom

Tactic:
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X : C
⊢ ((tensorBifunctor L W ε).obj (L'.obj X)).map ε.inv ≫
      (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom ≫ 𝟙 (L'.obj X) ≫ 𝟙 (L'.obj X) =
    ((tensorBifunctor L W ε).obj (L'.obj X)).map (ε' L W ε).inv ≫ (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ R = S

Tactic:
by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
⊢ ∀ (φ' : a' ⟶ c) [p.IsHomLift (h ≫ f ≫ g) φ'], ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = φ'

Tactic:
τ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
⊢ ∀ [p.IsHomLift (h ≫ f ≫ g) τ], ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
⊢ ∀ (φ' : a' ⟶ b) [p.IsHomLift (h ≫ f) φ'], ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ = φ'

Tactic:
τ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
⊢ ∀ [p.IsHomLift (h ≫ f) τ], ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ = τ
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
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        (eId V (F₁.obj j) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj j) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
rw [e_id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
⊢ ∀ (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ.hom = φ'

Tactic:
τ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
⊢ ∀ [p.IsHomLift (g ≫ f) τ], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ.hom = τ
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := ⋯
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
have inv_hom : φ' ≫ φ = 𝟙 b := fac p (p.map φ) φ _ (𝟙 b)

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ p.IsStronglyCartesian f φ

Tactic:
constructor
  intro c g φ' hφ'
  subst_hom_lift p f φ; clear a b R S
  -- Let `ψ` be a Cartesian arrow lying over `g`
  obtain ⟨a', ψ, hψ⟩ := h _ _ (p.map φ)
  -- Let `τ' : c ⟶ a'` be the map induced by the universal property of `ψ`
  let τ' := IsStronglyCartesian.map p (p.map φ) ψ (f' := g ≫ p.map φ) rfl φ'
  -- Let `Φ : a' ≅ a` be natural isomorphism induced between `φ` and `ψ`.
  let Φ := domainUniqueUpToIso p (p.map φ) φ ψ
  -- The map induced by `φ` will be `τ' ≫ Φ.hom`
  use τ' ≫ Φ.hom
  -- It is easily verified that `τ' ≫ Φ.hom` lifts `g` and `τ' ≫ Φ.hom ≫ φ = φ'`
  refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩
  · simp [τ', Φ]
  -- It remains to check that it is unique. This follows from the universal property of `ψ`.
  intro π ⟨hπ, hπ_comp⟩
  rw [← Iso.comp_inv_eq]
  apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'
  simp [hπ_comp, Φ]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
⊢ ∀ (φ' : a ⟶ c') [p.IsHomLift ((f ≫ g) ≫ h) φ'], ∃! χ, p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = φ'

Tactic:
τ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
⊢ ∀ [p.IsHomLift ((f ≫ g) ≫ h) τ], ∃! χ, p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
⊢ ∀ (φ' : b ⟶ c') [p.IsHomLift (g ≫ h) φ'], ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = φ'

Tactic:
τ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
⊢ ∀ [p.IsHomLift (g ≫ h) τ], ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = τ