awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Tactic:
simpa [eqToHom_left, eqToHom_right] using iso_w (eqToIso h.symm)

Premises used: CategoryTheory.Arrow.eqToHom_left, CategoryTheory.eqToIso, CategoryTheory.Arrow.iso_w, Eq.symm, CategoryTheory.Arrow.eqToHom_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯
⊢ f = f'

Tactic:
simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
mpr mpr₁ : mk f' = mk f'
⊢ mk f = mk f'

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
h₁ : f.left = g.left
h₂ : f.right = g.right
h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom ⋯
⊢ ∃ (hX : f.left = g.left), ∃ (hY : f.right = g.right), f.hom = eqToHom hX ≫ g.hom ≫ eqToHom ⋯

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y Y' : T
f : X ⟶ Y
h : Y = Y'
⊢ (mk (f ≫ eqToHom h)).hom = eqToHom ⋯ ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X' X Y : T
f : X ⟶ Y
h : X' = X
⊢ (mk (eqToHom h ≫ f)).hom = eqToHom h ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow.{v, u} T
sq : mk f ⟶ g
⊢ Hom.left sq ≫ g.hom = f ≫ Hom.right sq

Tactic:
sq.w

Premises used: CategoryTheory.Arrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f : Arrow.{v, u} T
X Y : T
g : X ⟶ Y
sq : f ⟶ mk g
⊢ Hom.left sq ≫ g = f.hom ≫ Hom.right sq

Tactic:
sq.w

Premises used: CategoryTheory.Arrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
g : X' ⟶ Y'
sq : mk f ⟶ mk g
⊢ Hom.left sq ≫ g = f ≫ Hom.right sq

Tactic:
sq.w

Premises used: CategoryTheory.Arrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ Hom.left sq ≫ Hom.left (inv sq) = 𝟙 f.left ∧ Hom.left (inv sq) ≫ Hom.left sq = 𝟙 g.left

Tactic:
simp [← comp_left]

Premises used: CategoryTheory.Arrow.comp_left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ Hom.right sq ≫ Hom.right (inv sq) = 𝟙 f.right ∧ Hom.right (inv sq) ≫ Hom.right sq = 𝟙 g.right

Tactic:
simp [← comp_right]

Premises used: CategoryTheory.Arrow.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
inst_2 : IsIso f.hom
rw : IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)
⊢ IsIso g.hom

Tactic:
rw [iso_w (asIso sq)]

Premises used: CategoryTheory.Arrow.iso_w, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
inst_2 : IsIso f.hom
⊢ IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow.{v, u} T
sq : mk f ⟶ g
inst_1 : IsIso sq
inst_2 : IsIso f
⊢ IsIso (mk f).hom

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow.{v, u} T
sq : mk f ⟶ g
inst_1 : IsIso sq
inst_2 : IsIso f
⊢ IsIso (mk f).hom

Tactic:
have : IsIso (mk f).hom := by assumption
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow.{v, u} T
sq : mk f ⟶ g
inst_1 : IsIso sq
inst_2 : IsIso f
this : IsIso (mk f).hom
⊢ IsIso g.hom

Tactic:
apply isIso_of_isIso' sq

Premises used: CategoryTheory.Arrow.isIso_of_isIso'
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ IsIso f.hom ↔ IsIso g.hom

Tactic:
⟨fun _ => isIso_of_isIso' sq, fun _ => isIso_of_isIso' (inv sq)⟩

Premises used: CategoryTheory.Arrow.isIso_of_isIso', Iff.intro, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
W X Y Z : T
f : W ⟶ X
g : Y ⟶ Z
sq : mk f ⟶ mk g
inst_1 : IsIso sq
⊢ IsIso f ↔ IsIso g

Tactic:
isIso_hom_iff_isIso_hom_of_isIso sq

Premises used: CategoryTheory.Arrow.isIso_hom_iff_isIso_hom_of_isIso
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
Y Z : T
f : Arrow.{v, u} T
g : Y ⟶ Z
sq : f ⟶ mk g
inst_1 : IsIso sq
⊢ IsIso f.hom ↔ IsIso g

Tactic:
isIso_hom_iff_isIso_hom_of_isIso sq

Premises used: CategoryTheory.Arrow.isIso_hom_iff_isIso_hom_of_isIso
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ Hom.left sq ≫ Hom.left (inv sq) = 𝟙 f.left

Tactic:
simp [← comp_left]

Premises used: CategoryTheory.Arrow.comp_left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ Hom.right sq ≫ Hom.right (inv sq) = 𝟙 f.right

Tactic:
simp [← comp_right]

Premises used: CategoryTheory.Arrow.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ Hom.left sq ≫ g.hom ≫ inv (Hom.right sq) = f.hom

Tactic:
simp only [← Category.assoc, IsIso.comp_inv_eq, w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Arrow.w, CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : IsIso sq
⊢ inv (Hom.left sq) ≫ f.hom ≫ Hom.right sq = g.hom

Tactic:
simp only [w, IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Arrow.w
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
⊢ ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom

Tactic:
have : ∀ g, (aux g).right = g ≫ f.hom := fun g => rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
change : Hom.left (aux φ) = Hom.left (aux ψ)
⊢ φ = ψ

Tactic:
change (aux φ).left = (aux ψ).left

Premises used: CategoryTheory.Arrow.Hom.left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
e_f : aux φ = aux ψ
⊢ Hom.left (aux φ) = Hom.left (aux ψ)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
e_f : aux φ ≫ sq = aux ψ ≫ sq
⊢ aux φ = aux ψ

Tactic:
rw [← cancel_mono sq]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
e_f : Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)
e_f₁ : Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)
⊢ aux φ ≫ sq = aux ψ ≫ sq

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)

Tactic:
h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)

Tactic:
simp [this, ← Arrow.w_mk_right, reassoc_of% h]

Premises used: CategoryTheory.Arrow.w_mk_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
change : Hom.right (aux φ) = Hom.right (aux ψ)
⊢ φ = ψ

Tactic:
change (aux φ).right = (aux ψ).right

Premises used: CategoryTheory.Arrow.Hom.right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
e_f : aux φ = aux ψ
⊢ Hom.right (aux φ) = Hom.right (aux ψ)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
e_f : sq ≫ aux φ = sq ≫ aux ψ
⊢ aux φ = aux ψ

Tactic:
rw [← cancel_epi sq]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
e_f : Hom.left (sq ≫ aux φ) = Hom.left (sq ≫ aux ψ)
e_f₁ : Hom.right (sq ≫ aux φ) = Hom.right (sq ≫ aux ψ)
⊢ sq ≫ aux φ = sq ≫ aux ψ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ Hom.left (sq ≫ aux φ) = Hom.left (sq ≫ aux ψ)

Tactic:
simp only [comp_left, comp_left, aux, mk_left, homMk_left, w_assoc, h]

Premises used: CategoryTheory.Arrow.comp_left, CategoryTheory.Arrow.mk_left, CategoryTheory.Arrow.w_assoc, CategoryTheory.Arrow.homMk_left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ Hom.right (sq ≫ aux φ) = Hom.right (sq ≫ aux ψ)

Tactic:
h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ Hom.right (sq ≫ aux φ) = Hom.right (sq ≫ aux ψ)

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.left (e.hom ≫ e.inv) = 𝟙 f.left
rw₁ : Hom.left (𝟙 f) = 𝟙 f.left
rw₂ rw₃ : Eq.{v + 1} (α := f.left ⟶ f.left) (𝟙 f.left) (𝟙 f.left)
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left

Tactic:
rw [← comp_left, e.hom_inv_id, id_left]

Premises used: CategoryTheory.Arrow.comp_left, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Arrow.id_left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.left (e.inv ≫ e.hom) = 𝟙 g.left
rw₁ : Hom.left (𝟙 g) = 𝟙 g.left
rw₂ rw₃ : Eq.{v + 1} (α := g.left ⟶ g.left) (𝟙 g.left) (𝟙 g.left)
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left

Tactic:
rw [← comp_left, e.inv_hom_id, id_left]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Arrow.comp_left, CategoryTheory.Arrow.id_left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.right (e.hom ≫ e.inv) = 𝟙 f.right
rw₁ : Hom.right (𝟙 f) = 𝟙 f.right
rw₂ rw₃ : Eq.{v + 1} (α := f.right ⟶ f.right) (𝟙 f.right) (𝟙 f.right)
⊢ Hom.right e.hom ≫ Hom.right e.inv = 𝟙 f.right

Tactic:
rw [← comp_right, e.hom_inv_id, id_right]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Arrow.id_right, CategoryTheory.Arrow.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.right (e.inv ≫ e.hom) = 𝟙 g.right
rw₁ : Hom.right (𝟙 g) = 𝟙 g.right
rw₂ rw₃ : Eq.{v + 1} (α := g.right ⟶ g.right) (𝟙 g.right) (𝟙 g.right)
⊢ Hom.right e.inv ≫ Hom.right e.hom = 𝟙 g.right

Tactic:
rw [← comp_right, e.inv_hom_id, id_right]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Arrow.id_right, CategoryTheory.Arrow.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
i : Arrow.{v, u} T
X Y : T
p : X ≅ Y
sq : i ⟶ mk p.hom
⊢ i.hom ≫ Hom.right sq ≫ p.inv = Hom.left sq

Tactic:
simpa only [mk_right, Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm

Premises used: Iff.mpr, CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Arrow.w_mk_right, CategoryTheory.Arrow.mk_right, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
i : X ≅ Y
p : Arrow.{v, u} T
sq : mk i.hom ⟶ p
⊢ i.inv ≫ Hom.left sq ≫ p.hom = Hom.right sq

Tactic:
simp [Arrow.w_mk_left]

Premises used: CategoryTheory.Arrow.w_mk_left
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
C : Type u
inst_1 : Category.{v, u} C
X Y Z : C
i : Arrow.{v, u} C
f : X ⟶ Y
g : Y ⟶ Z
sq : i ⟶ mk (f ≫ g)
⊢ (Hom.left sq ≫ f) ≫ (mk g).hom = i.hom ≫ Hom.right sq

Tactic:
simp [w_mk sq]

Premises used: CategoryTheory.Arrow.w_mk
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : Arrow.{v₁, u₁} C
f : X ⟶ Y
⊢ F.map (Arrow.Hom.left f) ≫ (Arrow.mk (F.map Y.hom)).hom = (Arrow.mk (F.map X.hom)).hom ≫ F.map (Arrow.Hom.right f)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsEquivalence
⊢ F.mapArrow.IsEquivalence

Tactic:
(mapArrowEquivalence (asEquivalence F)).isEquivalence_functor

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.mapArrowEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Functor.mapArrow
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
S : Type u
as as_1 : S
f : Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S } ⟶ Functor.obj (𝟭 (Discrete S)) { as := as_1 : Discrete S }
obtain :
  ∀
    (f :
      Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S } ⟶
        Functor.obj (𝟭 (Discrete S))
          { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as : Discrete S }),
    (fun (s : S) ↦ mk (𝟙 { as := s : Discrete S }))
        ((fun (f : Arrow (Discrete S)) ↦ f.left.as)
          { left := { as := as }, right := { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as },
            hom := f }) =
      { left := { as := as : Discrete S },
        right := { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as : Discrete S }, hom := f :
        Comma (A := Discrete S) (𝟭 (Discrete S)) (𝟭 (Discrete S)) }
⊢ (fun (s : S) ↦ mk (𝟙 { as := s : Discrete S }))
      ((fun (f : Arrow (Discrete S)) ↦ f.left.as) { left := { as := as }, right := { as := as_1 }, hom := f }) =
    { left := { as := as : Discrete S }, right := { as := as_1 : Discrete S }, hom := f :
      Comma (A := Discrete S) (𝟭 (Discrete S)) (𝟭 (Discrete S)) }

Tactic:
obtain rfl := Discrete.eq_of_hom f

Premises used: CategoryTheory.Discrete.eq_of_hom, rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
S : Type u
as : S
f :
  Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S } ⟶
    Functor.obj (𝟭 (Discrete S)) { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as : Discrete S }
⊢ (fun (s : S) ↦ mk (𝟙 { as := s : Discrete S }))
      ((fun (f : Arrow (Discrete S)) ↦ f.left.as)
        { left := { as := as }, right := { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as },
          hom := f }) =
    { left := { as := as : Discrete S },
      right := { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as : Discrete S }, hom := f :
      Comma (A := Discrete S) (𝟭 (Discrete S)) (𝟭 (Discrete S)) }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
⊢ F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)

Tactic:
have := h f
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
⊢ ∃ (hX : F.obj (mk f).left = G.obj (mk f).left),
    ∃ (hY : F.obj (mk f).right = G.obj (mk f).right), F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯

Tactic:
simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this

Premises used: CategoryTheory.Functor.mapArrow_obj, CategoryTheory.Arrow.mk_eq_mk_iff
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this :
  ∃ (hX : F.obj (mk f).left = G.obj (mk f).left),
    ∃ (hY : F.obj (mk f).right = G.obj (mk f).right), F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯
tauto tauto₁ tauto₂ :
  ∀ (w : F.obj (mk f).left = G.obj (mk f).left) (w_1 : F.obj (mk f).right = G.obj (mk f).right),
    F.map (mk f).hom = eqToHom w ≫ G.map (mk f).hom ≫ eqToHom ⋯ → F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
tauto
-- 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 R L
self : CommaMorphism Y X
⊢ Y.hom ≫ L.map self.right = R.map self.left ≫ X.hom

Tactic:
self.w.symm

Premises used: CategoryTheory.CommaMorphism.w, Eq.symm
-- 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
f g : X ⟶ Y
h₁ : f.left = g.left
h₂ : f.right = g.right
⊢ f = g

Tactic:
CommaMorphism.ext h₁ h₂

Premises used: CategoryTheory.CommaMorphism.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
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X : Comma L R
⊢ CommaMorphism.left (𝟙 X) = 𝟙 X.left

Tactic:
rfl

Premises used: 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 Z : Comma L R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).left = f.left ≫ g.left

Tactic:
rfl

Premises used: 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
H : X = Y
refl : X.left = X.left
⊢ X.left = Y.left

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
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.left = X.left

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.left (eqToHom ⋯) = eqToHom ⋯
⊢ CommaMorphism.left (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.left (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
H : X = Y
refl : X.right = X.right
⊢ X.right = Y.right

Tactic:
cases H