awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_4 : F.Faithful
⊢ (map₂ α β).Faithful

Tactic:
apply Comma.faithful_map

Premises used: CategoryTheory.Comma.faithful_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : G.Faithful
inst_6 : F.Full
inst_7 : IsIso α
inst_8 : IsIso β
inst :
  IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
⊢ (map₂ α β).Full

Tactic:
apply +allowSynthFailures Comma.full_map

Premises used: CategoryTheory.Comma.full_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : G.Faithful
inst_6 : F.Full
inst_7 : IsIso α
inst_8 : IsIso β
inst :
  ∀ (X : Discrete PUnit.{1}),
    IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
      (Functor.fromPUnit L ⋙ G).obj X) (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α) X)
⊢ IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : G.Faithful
inst_6 : F.Full
inst_7 : IsIso α
inst_8 : IsIso β
X : Discrete PUnit.{1}
inst : IsIso α
⊢ IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
    (Functor.fromPUnit L ⋙ G).obj X) (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_4 : G.Faithful
inst_5 : F.Full
inst_6 : IsIso α
inst_7 : IsIso β
X : Discrete PUnit.{1}
⊢ IsIso α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : F.EssSurj
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
inst :
  IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
⊢ (map₂ α β).EssSurj

Tactic:
apply +allowSynthFailures Comma.essSurj_map

Premises used: CategoryTheory.Comma.essSurj_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : F.EssSurj
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
inst :
  ∀ (X : Discrete PUnit.{1}),
    IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
      (Functor.fromPUnit L ⋙ G).obj X) (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α) X)
⊢ IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : F.EssSurj
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
X : Discrete PUnit.{1}
inst : IsIso α
⊢ IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
    (Functor.fromPUnit L ⋙ G).obj X) (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_4 : F.EssSurj
inst_5 : G.Full
inst_6 : IsIso α
inst_7 : IsIso β
X : Discrete PUnit.{1}
⊢ IsIso α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : F.IsEquivalence
inst_6 : G.Faithful
inst_7 : G.Full
inst_8 : IsIso α
inst_9 : IsIso β
inst :
  IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
⊢ (map₂ α β).IsEquivalence

Tactic:
apply +allowSynthFailures Comma.isEquivalenceMap

Premises used: CategoryTheory.Comma.isEquivalenceMap
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : F.IsEquivalence
inst_6 : G.Faithful
inst_7 : G.Full
inst_8 : IsIso α
inst_9 : IsIso β
inst :
  ∀ (X : Discrete PUnit.{1}),
    IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
      (Functor.fromPUnit L ⋙ G).obj X) (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α) X)
⊢ IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_5 : F.IsEquivalence
inst_6 : G.Faithful
inst_7 : G.Full
inst_8 : IsIso α
inst_9 : IsIso β
X : Discrete PUnit.{1}
inst : IsIso α
⊢ IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
    (Functor.fromPUnit L ⋙ G).obj X) (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_4 : F.IsEquivalence
inst_5 : G.Faithful
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
X : Discrete PUnit.{1}
⊢ IsIso α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f g : StructuredArrow S T
h : f.IsUniversal
η : f ⟶ g
⊢ η = IsInitial.to h g

Tactic:
h.hom_ext η (h.to g)

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsInitial.to
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
h : f.IsUniversal
g : StructuredArrow S T
⊢ f.hom ≫ T.map (h.desc g) = g.hom

Tactic:
(h.to g).w

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, CategoryTheory.Limits.IsInitial.to, CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η : f.right ⟶ c
⊢ η = h.desc (mk (f.hom ≫ T.map η))

Tactic:
let g := mk <| f.hom ≫ T.map η
  congrArg CommaMorphism.right (h.hom_ext (homMk η rfl : f ⟶ g) (h.to g))

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.StructuredArrow.IsUniversal.desc, congrArg, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, CategoryTheory.CommaMorphism.right, CategoryTheory.Limits.IsInitial.to, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
rw : h.desc (mk (f.hom ≫ T.map η)) = η'
rw₁ :
  Eq (α := f.right ⟶ c) (h.desc (mk (f.hom ≫ T.map η)) : f.right ⟶ (mk (f.hom ≫ T.map η)).right)
    (h.desc (mk (f.hom ≫ T.map η')))
rw₂ rw₃ :
  Eq (α := f.right ⟶ c) (h.desc (mk (f.hom ≫ T.map η')) : f.right ⟶ (mk (f.hom ≫ T.map η')).right)
    (h.desc (mk (f.hom ≫ T.map η')))
⊢ η = η'

Tactic:
rw [h.hom_desc η, h.hom_desc η', w]

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_desc
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f_1 : StructuredArrow S T
h : f_1.IsUniversal
g : StructuredArrow S T
f : f_1.right ⟶ g.right
w : (fun (η : f_1.right ⟶ g.right) ↦ f_1.hom ≫ T.map η = g.hom) f
⊢ f_1.hom ≫ T.map f = f_1.hom ≫ T.map (h.desc g)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
X Y : CostructuredArrow S T
f : X ⟶ Y
⊢ S.map f.left ≫ Y.hom = X.hom

Tactic:
simpa using CommaMorphism.w f

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
X Y : CostructuredArrow S T
f : X ⟶ Y
⊢ S.map f.left ≫ Y.hom = X.hom

Tactic:
CostructuredArrow.w f

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f.left = g.left
⊢ f = g

Tactic:
CommaMorphism.ext h (Subsingleton.elim _ _)

Premises used: CategoryTheory.CommaMorphism.ext, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f = g
rw rw₁ : g.left = g.left
⊢ f.left = g.left

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ (mk f).left = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ (mk f).right = { as := PUnit.unit }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ (mk f).hom = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : CostructuredArrow S T
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).left = f.left ≫ g.left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X : CostructuredArrow S T
⊢ CommaMorphism.left (𝟙 X) = 𝟙 X.left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y_1 Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : CostructuredArrow S T
h : X = Y
rw rw₁ : Y.left = Y.left
⊢ X.left = Y.left

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X Y : CostructuredArrow S T
h : X = Y
subst : CommaMorphism.left (eqToHom ⋯) = eqToHom ⋯
⊢ CommaMorphism.left (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X : CostructuredArrow S T
⊢ CommaMorphism.left (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, id_left]

Premises used: CategoryTheory.CostructuredArrow.id_left, CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
X Y : CostructuredArrow S T
f : X ⟶ Y
⊢ f.right = 𝟙 X.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f f' : CostructuredArrow S T
φ : f ⟶ f'
⊢ ∃ (ψ : f.left ⟶ f'.left) (hψ : S.map ψ ≫ f'.hom = f.hom), φ = homMk ψ hψ

Tactic:
⟨φ.left, CostructuredArrow.w φ, rfl⟩

Premises used: CategoryTheory.CostructuredArrow.w, CategoryTheory.CommaMorphism.left, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
⊢ f.homMk' (𝟙 f.left) = eqToHom ⋯

Tactic:
simp [eqToHom_left]

Premises used: CategoryTheory.CostructuredArrow.eqToHom_left
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ mk (S.map (𝟙 Y) ≫ (mk f).hom) = mk f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ (mk f).homMk' (𝟙 Y) = eqToHom ⋯

Tactic:
homMk'_id _

Premises used: CategoryTheory.CostructuredArrow.homMk'_id
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f.hom) = mk (S.map g' ≫ (mk (S.map g ≫ f.hom)).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y' Y'' : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ f.homMk' (g' ≫ g) = eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g

Tactic:
simp [eqToHom_left]

Premises used: CategoryTheory.CostructuredArrow.eqToHom_left
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ (mk f).hom) = mk (S.map g' ≫ (mk (S.map g ≫ f)).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y Y' Y'' : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ (mk f).homMk' (g' ≫ g) = eqToHom ⋯ ≫ (mk (S.map g ≫ f)).homMk' g' ≫ (mk f).homMk' g

Tactic:
homMk'_comp _ _ _

Premises used: CategoryTheory.CostructuredArrow.homMk'_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ mk (S.map (𝟙 Y) ≫ f) = mk f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
⊢ mkPrecomp f (𝟙 Y) = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f) = mk (S.map g' ≫ S.map g ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
Y Y' Y'' : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mkPrecomp f (g' ≫ g) = eqToHom ⋯ ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ f.right = f'.right

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ S.map g.hom ≫ f'.hom = f.hom ≫ Functor.map (Functor.fromPUnit T) (Iso.hom (eqToIso ⋯))

Tactic:
simpa using w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
x y : CostructuredArrow S T
hl : x.left = y.left
hh : S.map (eqToHom hl) ≫ y.hom = x.hom
mk :
  ∀ (left : C) (right : Discrete PUnit.{1}) (hom : S.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right)
    (hl : CostructuredArrow.left { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y.left)
    (hh : S.map (eqToHom hl) ≫ y.hom = CostructuredArrow.hom { left := left, right := right, hom := hom }),
    { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y
⊢ x = y

Tactic:
cases x