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

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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
⊢ { obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f ≫
      { app := fun c ↦ Y.map (τ.app c), naturality := ⋯ } =
    { app := fun c ↦ X.map (τ.app c), naturality := ⋯ } ≫
      { obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ ({ obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f ≫
          { app := fun c ↦ Y.map (τ.app c), naturality := ⋯ }).app
      x✝ =
    ({ app := fun c ↦ X.map (τ.app c), naturality := ⋯ } ≫
          { obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f).app
      x✝
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f ↔ IsIso f.1 ∧ IsIso f.2

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.1 ∧ IsIso f.2

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2 → IsIso f
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
⊢ { obj := fun F ↦ F ⋙ X✝, map := fun {X Y} α ↦ whiskerRight α X✝, map_id := ⋯, map_comp := ⋯ }.map f ≫
      { app := fun c ↦ τ.app (Y.obj c), naturality := ⋯ } =
    { app := fun c ↦ τ.app (X.obj c), naturality := ⋯ } ≫
      { obj := fun F ↦ F ⋙ Y✝, map := fun {X Y} α ↦ whiskerRight α Y✝, map_id := ⋯, map_comp := ⋯ }.map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ ({ obj := fun F ↦ F ⋙ X✝, map := fun {X Y} α ↦ whiskerRight α X✝, map_id := ⋯, map_comp := ⋯ }.map f ≫
          { app := fun c ↦ τ.app (Y.obj c), naturality := ⋯ }).app
      x✝ =
    ({ app := fun c ↦ τ.app (X.obj c), naturality := ⋯ } ≫
          { obj := fun F ↦ F ⋙ Y✝, map := fun {X Y} α ↦ whiskerRight α Y✝, map_id := ⋯, map_comp := ⋯ }.map f).app
      x✝
Module: Mathlib.CategoryTheory.Whiskering

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
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
⊢ F.whiskerLeft β ≫ whiskerRight α K = whiskerRight α H ≫ G.whiskerLeft β

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
x✝ : C
⊢ (F.whiskerLeft β ≫ whiskerRight α K).app x✝ = (whiskerRight α H ≫ G.whiskerLeft β).app x✝
Module: Mathlib.CategoryTheory.Whiskering

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
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
⊢ α ◫ β = F.whiskerLeft β ≫ whiskerRight α K

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
x✝ : C
⊢ (α ◫ β).app x✝ = (F.whiskerLeft β ≫ whiskerRight α K).app x✝
Module: Mathlib.CategoryTheory.Whiskering

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
F G : C ⥤ D
H K : D ⥤ E
α : F ≅ G
β : H ≅ K
⊢ F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H K : D ⥤ E
α : F ≅ G
β : H ≅ K
x✝ : C
⊢ (F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K).hom.app x✝ = (isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β).hom.app x✝
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : α
⊢ (as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a

Tactic:
simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op = f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop = f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)

Tactic:
constructor

Goal state after:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f → ∀ (i : I), IsIso (f i)

case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ (∀ (i : I), IsIso (f i)) → IsIso f
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
⊢ NatTrans.op α.hom ≫ NatTrans.op α.inv = 𝟙 G.op

Tactic:
ext

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ᵒᵖ
⊢ (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x✝ = (𝟙 G.op).app x✝
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
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op

Tactic:
ext

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ᵒᵖ
⊢ (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x✝ = (𝟙 F.op).app x✝
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' ↔ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
constructor

Goal state after:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' → ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ (∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'
Module: Mathlib.CategoryTheory.Groupoid

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

Tactic:
constructor

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

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ isomorphisms C = ⊤ → IsGroupoid C
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.strictMap (𝟭 C) = P

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ P.strictMap (𝟭 C) f✝ ↔ P 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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
P : MorphismProperty C
F : C ⥤ D
G : D ⥤ E
⊢ (P.strictMap F).strictMap G = P.strictMap (F ⋙ G)

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
P : MorphismProperty C
F : C ⥤ D
G : D ⥤ E
X✝ Y✝ : E
f✝ : X✝ ⟶ Y✝
⊢ (P.strictMap F).strictMap G f✝ ↔ P.strictMap (F ⋙ G) 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
F : C ⥤ D
ι : Type u_3
P : ι → MorphismProperty D
⊢ (⨆ i, P i).inverseImage F = ⨆ i, (P i).inverseImage F

Tactic:
ext

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
ι : Type u_3
P : ι → MorphismProperty D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (⨆ i, P i).inverseImage F f✝ ↔ (⨆ i, (P i).inverseImage F) 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
F : C ⥤ D
P : Set (MorphismProperty D)
⊢ (sSup P).inverseImage F = ⨆ P' ∈ P, P'.inverseImage F

Tactic:
ext

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
P : Set (MorphismProperty D)
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (sSup P).inverseImage F f✝ ↔ (⨆ P' ∈ P, P'.inverseImage F) f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty C
⊢ (⨆ i, W i).toSet = ⋃ i, (W i).toSet

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty C
x✝ : Arrow C
⊢ x✝ ∈ (⨆ i, W i).toSet ↔ x✝ ∈ ⋃ i, (W i).toSet
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: 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
⊢ ofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i)

Tactic:
constructor

Goal state after:
case mp
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
⊢ ofHoms f g → ∃ i, Arrow.mk g = Arrow.mk (f i)

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
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 : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)

Tactic:
constructor

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f ↔ P f

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f → P f

case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ P f → ofHoms P.homFamily f
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
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ l₁ = l₂

Tactic:
ext

Goal state after:
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
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ l₁.l = l₂.l
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ aux φ ≫ sq = aux ψ ≫ sq

Tactic:
ext

Goal state after:
case h₁
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := ⋯
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)

case h₂
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := ⋯
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)
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 ↔ Nonempty sq.LiftStruct

Tactic:
constructor

Goal state after:
case mp
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 → Nonempty sq.LiftStruct

case mpr
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
⊢ Nonempty sq.LiftStruct → sq.HasLift
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (isomorphisms C).op = isomorphisms Cᵒᵖ

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (isomorphisms C).op f✝ ↔ isomorphisms Cᵒᵖ f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P.isoClosure ≤ Q → P ≤ Q

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P ≤ Q → P.isoClosure ≤ Q
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
W : MorphismProperty C
F : C ⥤ D
⊢ W.map F = (W.strictMap F).isoClosure

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
W : MorphismProperty C
F : C ⥤ D
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ W.map F f✝ ↔ (W.strictMap F).isoClosure f✝
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
f : X → Y
⊢ Mono (↾f) ↔ Function.Injective f

Tactic:
constructor

Goal state after:
case mp
X Y : Type u
f : X → Y
⊢ Mono (↾f) → Function.Injective f

case mpr
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
f : X → Y
⊢ Epi (↾f) ↔ Function.Surjective f

Tactic:
constructor

Goal state after:
case mp
X Y : Type u
f : X → Y
⊢ Epi (↾f) → Function.Surjective f

case mpr
X Y : Type u
f : X → Y
⊢ Function.Surjective f → Epi (↾f)
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
⊢ X.hom = X.hom ≫ R₁.map r.hom ≫ R₁.map r.inv

Tactic:
← R₁.map_comp

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
⊢ X.hom = X.hom ≫ R₁.map (r.hom ≫ 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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝¹ : F₁.Faithful
inst✝ : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f = g

Tactic:
ext

Goal state after:
case h₁
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
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝¹ : F₁.Faithful
inst✝ : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.left = g.left

case h₂
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
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝¹ : F₁.Faithful
inst✝ : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.right = g.right
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (α.conjAut f)).hom = ((F.mapIso α).conjAut (F.mapIso f)).hom
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
ext

Goal state after:
X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
ext

Goal state after:
X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
ext

Goal state after:
X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
ext

Goal state after:
X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝
x✝ : X
⊢ a₁✝ x✝ = a₂✝ x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝
x✝ : X
⊢ a₁✝ x✝ = a₂✝ x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
⊢ (GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
ext

Goal state after:
X Y : GrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
⊢ (GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
ext

Goal state after:
X Y : GrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
⊢ (CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
ext

Goal state after:
X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
⊢ (CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
ext

Goal state after:
X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
ext

Goal state after:
R S : SemiRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
ext

Goal state after:
R S : SemiRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
ext

Goal state after:
R S : RingCat
e : R ≅ S
x✝ : ↑S
⊢ ((RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
ext

Goal state after:
R S : RingCat
e : R ≅ S
x✝ : ↑R
⊢ ((RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
ext

Goal state after:
R S : CommSemiRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
ext

Goal state after:
R S : CommSemiRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
ext

Goal state after:
R S : CommRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
ext

Goal state after:
R S : CommRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝