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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x'

Tactic:
by

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F G : J ⥤ Type w
φ : F ⟶ G
x : ↑F.sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (G.map f)) ((fun j ↦ (ConcreteCategory.hom (φ.app j)) (↑x j)) j) =
    (fun j ↦ (ConcreteCategory.hom (φ.app j)) (↑x j)) j'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : C
p : X = Y
q : Y = Z
x : F.obj X
⊢ (ConcreteCategory.hom (F.map (eqToHom q))) ((ConcreteCategory.hom (F.map (eqToHom p))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯))) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (ConcreteCategory.hom ((forget₂ C D).map (f ≫ g))) x =
    (ConcreteCategory.hom ((forget₂ C D).map g)) ((ConcreteCategory.hom ((forget₂ C D).map f)) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
D : Type u_3
inst✝² : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
obj : C → D
h_obj : ∀ (X : C), (forget D).obj (obj X) = (forget C).obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, (forget D).map (map f) ≍ (forget C).map f
⊢ Functor.Faithful.div (forget C) (forget D) obj h_obj map h_map ⋙ forget D = forget C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁸ : ConcreteCategory C FC
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
E : Type u_5
inst✝⁴ : Category.{v_3, u_5} E
FE : E → E → Type u_6
CE : E → Type w
inst✝³ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝² : ConcreteCategory E FE
inst✝¹ : HasForget₂ C D
inst✝ : HasForget₂ D E
⊢ (CategoryTheory.forget₂ C D ⋙ CategoryTheory.forget₂ D E) ⋙ forget E = forget C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (hom ((forget₂ C D).map (f ≫ g))) x = (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
⊢ ⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm

Tactic:
by

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

Goal state before:
pp: X : Type u
x y : X
⊢ x = y → homOfElement x = homOfElement y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
⊢ ↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)) = 𝟙 (m α)

Tactic:
by

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾_root_.Functor.map ⇑(Hom.hom (f ≫ g)) = ↾_root_.Functor.map ⇑(Hom.hom f) ≫ ↾_root_.Functor.map ⇑(Hom.hom g)

Tactic:
by

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

Goal state before:
pp: X Y : Type u
i : X ≅ Y
x : X
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by

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

Goal state before:
pp: X Y : Type u
i : X ≅ Y
y : Y
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) y) = y

Tactic:
by

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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ (P.map F).map G = P.map (F ⋙ G)

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Type u
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ↾Function.surjInv ⋯ ≫ f = 𝟙 Y✝

Tactic:
by

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ IsSplitEpi f

Tactic:
by

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 D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P.inverseImage F f
⊢ P.inverseImage F (e ≫ f)

Tactic:
by

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 D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P.inverseImage F f
⊢ P.inverseImage F (f ≫ e)

Tactic:
by

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 G : C ⥤ D
e : F ≅ G
⊢ P.map F = P.map G

Tactic:
by

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 D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor = P.map E.inverse

Tactic:
by

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 D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.inverseImage F).map F = P

Tactic:
by

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
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.map F).inverseImage F = P

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f ↔ IsIso f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ monomorphisms C f ↔ Mono f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ epimorphisms C f ↔ Epi f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (MorphismProperty.monomorphisms C).RespectsIso

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (MorphismProperty.epimorphisms C).RespectsIso

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (MorphismProperty.isomorphisms C).RespectsIso

Tactic:
by

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
F G : C ⥤ D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ (F.mapIso e).hom ≫ (Arrow.mk (α.app Y)).hom = (Arrow.mk (α.app X)).hom ≫ (G.mapIso e).hom

Tactic:
by

Goal state after:
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 R
H : X = Y
⊢ X.left = Y.left

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).left = eqToHom ⋯

Tactic:
by

Goal state after:
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 R
H : X = Y
⊢ X.right = Y.right

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).right = eqToHom ⋯

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (inv e).left = inv e.left

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ L.map e.left ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso ((forget C).map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
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'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫
      { left := F₁.obj Y.left, right := F₂.obj Y.right, hom := α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right }.hom =
    { left := F₁.obj X.left, right := F₂.obj X.right, hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right }.hom ≫
      R'.map (F₂.map φ.right)

Tactic:
by

Goal state after:
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' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X : Comma L R
⊢ ((map α β).obj X).hom = (α.app X.left ≫ F.map X.hom) ≫ β.app X.right

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1

Tactic:
by

Goal state after:
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₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
    (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f g : (End X)ˣ
⊢ { hom := ↑(f * g), inv := (f * g).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := ↑f, inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } *
      { hom := ↑g, inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by

Goal state after:
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₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut X
⊢ (fun y ↦ { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ((fun x ↦ { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut Y
⊢ (fun x ↦ { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ((fun y ↦ { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
⊢ ∀ (x y : Aut X),
    { hom := h.inv ≫ (x * y).hom ≫ h.hom, inv := h.inv ≫ (x * y).inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ } =
      { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ } *
        { hom := h.inv ≫ y.hom ≫ h.hom, inv := h.inv ≫ y.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by

Goal state after:
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₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right) =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right

Tactic:
by

Goal state after:
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₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))

Tactic:
by

Goal state after:
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₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ (map α β).map { left := F₁.preimage φ.left, right := F₂.preimage φ.right, w := ⋯ } = φ

Tactic:
by

Goal state after:
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₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    ((map α β).obj
          { left := F₁.objPreimage X.left, right := F₂.objPreimage X.right,
            hom :=
              F.preimage
                ((inv α).app (F₁.objPreimage X.left) ≫
                  L'.map (F₁.objObjPreimageIso X.left).hom ≫
                    X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ (inv β).app (F₂.objPreimage X.right)) }).hom ≫
      R'.map (F₂.objObjPreimageIso X.right).hom

Tactic:
by

Goal state after:
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₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    ((map α β).obj
          { left := F₁.objPreimage X.left, right := F₂.objPreimage X.right,
            hom :=
              F.preimage
                ((inv α).app (F₁.objPreimage X.left) ≫
                  L'.map (F₁.objObjPreimageIso X.left).hom ≫
                    X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ (inv β).app (F₂.objPreimage X.right)) }).hom ≫
      R'.map (F₂.objObjPreimageIso X.right).hom

Tactic:
by
            dsimp
            simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.map_preimage, assoc,
              IsIso.inv_hom_id, comp_id, IsIso.hom_inv_id_assoc]
            rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]

Goal state after: