awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X : Comma L R
⊢ X.right = X.right

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
H : X = Y
refl : CommaMorphism.right (eqToHom ⋯) = eqToHom ⋯
⊢ CommaMorphism.right (eqToHom H) = eqToHom ⋯

Tactic:
cases H
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X : Comma L R
⊢ CommaMorphism.right (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_6 : IsIso e
⊢ IsIso e.left

Tactic:
(Comma.fst L R).map_isIso e

Premises used: CategoryTheory.Comma.fst, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_6 : IsIso e
⊢ IsIso e.right

Tactic:
(Comma.snd L R).map_isIso e

Premises used: CategoryTheory.Functor.map_isIso, CategoryTheory.Comma.snd
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : e.left ≫ (inv e).left = 𝟙 X.left
⊢ (inv e).left = inv e.left

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : (e ≫ inv e).left = 𝟙 X.left
hom_inv_id₁ : CommaMorphism.left (𝟙 X) = 𝟙 X.left
hom_inv_id₂ hom_inv_id₃ : Eq.{v₁ + 1} (α := X.left ⟶ X.left) (𝟙 X.left) (𝟙 X.left)
⊢ e.left ≫ (inv e).left = 𝟙 X.left

Tactic:
rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Premises used: CategoryTheory.Comma.comp_left, CategoryTheory.Comma.id_left, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : e.right ≫ (inv e).right = 𝟙 X.right
⊢ (inv e).right = inv e.right

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : (e ≫ inv e).right = 𝟙 X.right
hom_inv_id₁ : CommaMorphism.right (𝟙 X) = 𝟙 X.right
hom_inv_id₂ hom_inv_id₃ : Eq.{v₂ + 1} (α := X.right ⟶ X.right) (𝟙 X.right) (𝟙 X.right)
⊢ e.right ≫ (inv e).right = 𝟙 X.right

Tactic:
rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Premises used: CategoryTheory.Comma.comp_right, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Comma.id_right
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
⊢ L.map e.left ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
⊢ L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} 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
rw : X.hom = X.hom ≫ R₁.map (r.hom ≫ r.inv)
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv

Tactic:
rw [← L₁.mapIso_inv l, Iso.inv_comp_eq, L₁.mapIso_hom, ← Category.assoc, h,
          Category.assoc, ← R₁.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} 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)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
dsimp :
  L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)
⊢ 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 :
          Comma L' R' }.hom =
    { left := F₁.obj X.left, right := F₂.obj X.right, hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right :
          Comma L' R' }.hom ≫
      R'.map (F₂.map φ.right)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
rw :
  α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right
⊢ L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)

Tactic:
rw [assoc, assoc, ← Functor.comp_map, α.naturality_assoc, ← Functor.comp_map,
          ← β.naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
dsimp :
  α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
⊢ α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
rw :
  α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
rw₁ :
  α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right
rw₂ rw₃ :
  α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right
⊢ α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right

Tactic:
rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w]

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
h₁ : f.left = g.left
h₂ : f.right = g.right
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.left = g.left

Tactic:
F₁.map_injective (congr_arg CommaMorphism.left h)

Premises used: congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.left = g.left

Tactic:
exact F₁.map_injective (congr_arg CommaMorphism.left h)

Premises used: congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.right = g.right

Tactic:
F₂.map_injective (congr_arg CommaMorphism.right h)

Premises used: congr_arg, CategoryTheory.CommaMorphism.right, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f.right = g.right

Tactic:
exact F₂.map_injective (congr_arg CommaMorphism.right h)

Premises used: congr_arg, CategoryTheory.CommaMorphism.right, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
rw :
  α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))

Tactic:
rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
erw :
  (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)
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right

Tactic:
erw [← α.naturality_assoc, β.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
dsimp :
  L'.map (F₁.map (F₁.preimage φ.left)) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map (F₂.map (F₂.preimage φ.right))
⊢ (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:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
rw :
  L'.map φ.left ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map φ.right
⊢ L'.map (F₁.map (F₁.preimage φ.left)) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map (F₂.map (F₂.preimage φ.right))

Tactic:
rw [F₁.map_preimage, F₂.map_preimage]

Premises used: CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ L'.map φ.left ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map φ.right

Tactic:
simpa using φ.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.EssSurj
inst_7 : F₂.EssSurj
inst_8 : F.Full
inst_9 : IsIso α
inst_10 : IsIso β
X : Comma L' R'
dsimp :
  Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (CategoryStruct.comp (Y := R'.obj (F₂.obj (F₂.objPreimage X.right)))
      (α.app (F₁.objPreimage X.left) ≫
        F.map
            (F.preimage
              ((inv α).app (F₁.objPreimage X.left) ≫
                L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫
                  X.hom ≫ R'.map (Iso.inv (F₂.objObjPreimageIso X.right)) ≫ (inv β).app (F₂.objPreimage X.right))) ≫
          β.app (F₂.objPreimage X.right))
      (R'.map (Iso.hom (F₂.objObjPreimageIso X.right))))
⊢ L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ 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 (Iso.hom (F₁.objObjPreimageIso X.left)) ≫
                    X.hom ≫ R'.map (Iso.inv (F₂.objObjPreimageIso X.right)) ≫ (inv β).app (F₂.objPreimage X.right)) :
            Comma L R }).hom ≫
      R'.map (Iso.hom (F₂.objObjPreimageIso X.right))

Tactic:
dsimp