mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.isoClosure.map F = P.map F

Tactic:
refine le_antisymm ?_ (map_monotone P.le_isoClosure F)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.isoClosure.map F ≤ P.map F
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
eq1 : X = X'
eq2 : Y = Y'
eq3 : Z = Z'
H1 : f ≍ f'
H2 : g ≍ g'
⊢ f ≫ g ≍ f' ≫ g'

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝) ≫ α.inv.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
rw [α.hom_inv_id_app]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj (unop x✝))).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → isomorphisms C = ⊤

Tactic:
eq_top_iff

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → ⊤ ≤ isomorphisms C
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤.map F = ⊤

Tactic:
eq_top_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤ ≤ ⊤.map F
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ (∃ i, Arrow.mk g = Arrow.mk (f i)) → ofHoms f g

Tactic:
rintro ⟨i, h⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
by
  rw [iff, iff]
  exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ Q.isoClosure ≤ Q

Tactic:
by rw [Q.isoClosure_eq_self]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure.map F = P.map F

Tactic:
apply le_antisymm

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure.map F ≤ P.map F

case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.map F ≤ P.isoClosure.map F
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ (P.map F).map G = P.map (F ⋙ G)

Tactic:
apply le_antisymm

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ (P.map F).map G ≤ P.map (F ⋙ G)

case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ P.map (F ⋙ G) ≤ (P.map F).map G
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor = P.map E.inverse

Tactic:
apply le_antisymm

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor ≤ P.map E.inverse

case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.map E.inverse ≤ P.inverseImage E.functor
Module: Mathlib.CategoryTheory.Comma.Basic

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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv

Tactic:
← L₁.mapIso_inv l,

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ (L₁.mapIso l).inv ≫ X.hom = Y.hom ≫ R₁.map r.inv
Module: Mathlib.CategoryTheory.Comma.Basic

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
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
X✝ Y✝ : Comma L.op R.op
f : X✝ ⟶ Y✝
⊢ (R.map f.right.unop ≫ (unop (op { left := unop X✝.right, right := unop X✝.left, hom := X✝.hom.unop })).hom).op =
    ((unop (op { left := unop Y✝.right, right := unop Y✝.left, hom := Y✝.hom.unop })).hom ≫ L.map f.left.unop).op

Tactic:
simpa using! f.w.symm

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
f : X ⟶ Y
x✝ : IsIso ((forget GrpCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget GrpCat).map f)
    let e : X ≃* Y := { i.toEquiv with map_mul' := by simp [Iso.toEquiv, i] }
    exact e.toGrpIso.isIso_hom

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

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
X Y : C
f : X ⟶ Y
Z : D
⊢ Function.Bijective ((⇑(adj.homEquiv X Z) ∘ fun g ↦ F.map f ≫ g) ∘ ⇑(adj.homEquiv Y Z).symm) ↔
    Function.Bijective fun g ↦ f ≫ g

Tactic:
congr!

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
X Y : C
f : X ⟶ Y
Z : D
x✝ : Y ⟶ G.obj Z
⊢ (⇑(adj.homEquiv X Z) ∘ fun g ↦ F.map f ≫ g) ∘ ⇑(adj.homEquiv Y Z).symm = CategoryStruct.comp f
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
X Y : D
g : X ⟶ Y
Z : C
⊢ (Function.Bijective fun f ↦ f ≫ G.map g) ↔
    Function.Bijective ((⇑(adj.homEquiv Z Y) ∘ fun f ↦ f ≫ g) ∘ ⇑(adj.homEquiv Z X).symm)

Tactic:
congr!

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
X Y : D
g : X ⟶ Y
Z : C
x✝ : Z ⟶ G.obj X
⊢ x✝ ≫ G.map g = ((⇑(adj.homEquiv Z Y) ∘ fun f ↦ f ≫ g) ∘ ⇑(adj.homEquiv Z X).symm) x✝
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ ∀ (a : ThinSkeleton C), Quotient.lift₂ (fun X Y ↦ Nonempty (X ⟶ Y)) ⋯ a a

Tactic:
by
    refine Quotient.ind fun a => ?_
    exact ⟨𝟙 _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ sq.HasLift

Tactic:
exact
        CommSq.HasLift.mk'
          ⟨(CommSq.mk h₀).lift, by
            simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift

Tactic:
intro f g sq

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift

Tactic:
intro f g sq

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k = l

Tactic:
apply hs.hom_ext
  rintro (_ | j)
  · exact hbase
  · exact hπ j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl

Tactic:
rwa [Category.assoc, Category.id_comp] at e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁹ : Category.{w, u₂} D
E : Type u₃
inst✝⁸ : Category.{w', u₃} E
F✝ : C ⥤ D
G : D ⥤ E
A✝ A' B B' : C
inst✝⁷ : HasBinaryProduct A✝ B
inst✝⁶ : HasBinaryProduct A' B'
inst✝⁵ : HasBinaryProduct (F✝.obj A✝) (F✝.obj B)
inst✝⁴ : HasBinaryProduct (F✝.obj A') (F✝.obj B')
inst✝³ : HasBinaryProduct (G.obj (F✝.obj A✝)) (G.obj (F✝.obj B))
inst✝² : HasBinaryProduct ((F✝ ⋙ G).obj A✝) ((F✝ ⋙ G).obj B)
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
F : C ⥤ D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (prod.functor.obj A ⋙ F).map f_1 ≫ prodComparison F A Y =
      prodComparison F A f ≫ (F ⋙ prod.functor.obj (F.obj A)).map f_1

Tactic:
simp [prodComparison_natural]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
inst✝¹ : T.Full
inst✝ : T.Faithful
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι.app j ≫ m = c.ι.app j
⊢ m = homMk (T.preimage c.pt.hom) ⋯

Tactic:
apply CommaMorphism.ext
    · simp
    · apply T.map_injective
      simpa only [homMk_right, T.map_preimage, ← w m] using! (Category.id_comp _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝⁶ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁵ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst✝⁴ : F.IsEquivalence
inst✝³ : G.Faithful
inst✝² : G.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).IsEquivalence

Tactic:
by
  apply Comma.isEquivalenceMap

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    ((span f g).map f_1 ≫ Option.casesOn Y_1 (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn X_1 (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) <;> intro f <;> cases f <;> dsimp <;> aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₁ ≫ inv i₃ = inv i₁ ≫ f₁

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₁ = (inv i₁ ≫ f₁) ≫ i₃
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₂ ≫ inv i₃ = inv i₂ ≫ f₂

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₂ = (inv i₂ ≫ f₂) ≫ i₃
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₁ ≫ inv i₁ = inv i₃ ≫ f₁

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₁ = (inv i₃ ≫ f₁) ≫ i₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₂ = (inv i₃ ≫ f₂) ≫ i₂
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f g : Over X
φ : f ⟶ g
F✝ : T ⥤ D
Y : D
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Over (G.obj Y)
⊢ Hom.left
      ((post F ⋙ map (a.counit.app Y)).map ({ app := fun A ↦ homMk (a.unit.app A.left) ⋯, naturality := ⋯ }.app A) ≫
        { app := fun A ↦ homMk (a.counit.app A.left) ⋯, naturality := ⋯ }.app ((post F ⋙ map (a.counit.app Y)).obj A)) =
    Hom.left (𝟙 ((post F ⋙ map (a.counit.app Y)).obj A))

Tactic:
simp [-Functor.id_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f g : Under X✝
φ : f ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Under ((𝟭 T).obj X)
⊢ Hom.right
      ((post F).map ({ app := fun A ↦ homMk (a.unit.app A.right) ⋯, naturality := ⋯ }.app A) ≫
        { app := fun A ↦ homMk (a.counit.app A.right) ⋯, naturality := ⋯ }.app ((post F).obj A)) =
    Hom.right (𝟙 ((post F).obj A))

Tactic:
simp [-Functor.id_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f g : Under X✝
φ : f ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Under (F.obj ((𝟭 T).obj X))
⊢ Hom.right
      ({ app := fun A ↦ homMk (a.unit.app A.right) ⋯, naturality := ⋯ }.app ((post G ⋙ map (a.unit.app X)).obj A) ≫
        (post G ⋙ map (a.unit.app X)).map ({ app := fun A ↦ homMk (a.counit.app A.right) ⋯, naturality := ⋯ }.app A)) =
    Hom.right (𝟙 ((post G ⋙ map (a.unit.app X)).obj A))

Tactic:
simp [-Functor.id_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝⁶ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁵ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝⁴ : F.IsEquivalence
inst✝³ : G.Faithful
inst✝² : G.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).IsEquivalence

Tactic:
by
  apply Comma.isEquivalenceMap

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
g : CostructuredArrow (Functor.diag T) X
⊢ (proj (Functor.diag T) X).obj g ⟶ X.1

Tactic:
exact g.hom.1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inl f f ≫ (pushoutSymmetry f f).hom = pushout.inl f f ≫ 𝟙 (pushout f f)

Tactic:
simp [inl_eq_inr_of_epi_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inr f f ≫ (pushoutSymmetry f f).hom = pushout.inr f f ≫ 𝟙 (pushout f f)

Tactic:
simp [inl_eq_inr_of_epi_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inr ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inr ≫ 𝟙 t.pt

Tactic:
simp [inl_eq_inr_of_epi_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : ∀ {c : Cone K} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
⊢ ⋯ = ⋯

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : ∀ {c : Cocone K} (hc : IsColimit c), Nonempty (IsColimit (F.mapCocone c))
⊢ ⋯ = ⋯

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : ∀ {K : J ⥤ C}, PreservesLimit K F
⊢ ⋯ = ⋯

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : ∀ {K : J ⥤ C}, PreservesColimit K F
⊢ ⋯ = ⋯

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : ∀ {J : Type w} [inst : Category.{w', w} J], PreservesLimitsOfShape J F
⊢ ⋯ = ⋯

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : ∀ {J : Type w} [inst : Category.{w', w} J], PreservesColimitsOfShape J F
⊢ ⋯ = ⋯

Tactic:
congr!

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ f = 0

Tactic:
by rw [← image.fac f, w, HasZeroMorphisms.comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
by
  apply preservesLimit_of_preserves_limit_cone terminalIsTerminal
  apply (isLimitMapConeEmptyConeEquiv _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f ≫ 𝟙 (⊥_ C) = f ≫ 0

Tactic:
congr!

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ 𝟙 (⊥_ C) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) ≫ f = 0 ≫ f

Tactic:
congr!

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) = 0