awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.snd ≫ h.Ω₀.arrow
rw₁ : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.fst ≫ π' ≫ h.Ω₀.arrow
rw₂ rw₃ : (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π' ≫ h.Ω₀.arrow = s.fst ≫ π' ≫ h.Ω₀.arrow
⊢ (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π' = s.snd

Tactic:
rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.arrow, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono, CategoryTheory.SubobjectRepresentableBy.Ω₀
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
m : s.pt ⟶ X
hm : m ≫ 𝟙 X = s.fst
h_1 : m ≫ π' = s.snd
⊢ m = (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s

Tactic:
simpa using hm
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
⊢ IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow

Tactic:
have : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow :=
      { isLimit' := ⟨PullbackCone.IsLimit.mk _ (fun s ↦ s.fst) (by simp)
          (fun s ↦ by rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc])
          (fun s m hm _ ↦ by simpa using hm) ⟩ }
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
this : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : π' ≫ h.Ω₀.arrow = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
rw₁ : h.χ (𝟙 X) = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
rw₂ : h.χ (𝟙 X) = 𝟙 X ≫ h.χ (𝟙 X)
rw₃ rw₄ : h.χ (𝟙 X) = h.χ (𝟙 X)
⊢ π' = (fun (X : C) ↦ h.π (𝟙 X)) X

Tactic:
rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
      ← (h.isPullback (𝟙 X)).w, Category.id_comp]

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono, CategoryTheory.SubobjectRepresentableBy.uniq, CategoryTheory.SubobjectRepresentableBy.isPullback, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.SubobjectRepresentableBy.Ω₀, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
⊢ HasTerminal.{v, u} C

Tactic:
h.isTerminalΩ₀.hasTerminal

Premises used: CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.SubobjectRepresentableBy.isTerminalΩ₀
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
⊢ m ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl U) ≫ m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
⊢ h.χ m ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl X) ≫ h.χ m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
⊢ h.Ω₀.arrow ≫ Iso.hom (Iso.refl Ω) =
    CategoryStruct.comp (Y := terminal.{v, u} C) (Iso.hom h.isoΩ₀) (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
⊢ m ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl U) ≫ m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
⊢ χ' ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl X) ≫ χ'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
⊢ Eq (α := terminal.{v, u} C ⟶ Ω) ((Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow) ≫ Iso.hom (Iso.refl Ω))
    (Iso.hom (Iso.symm h.isoΩ₀) ≫ h.Ω₀.arrow)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
⊢ IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow

Tactic:
have : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow :=
      sq.of_iso (Iso.refl _) (Iso.refl _) (h.isoΩ₀.symm) (Iso.refl _)
        (by simp) (h.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
this : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow
⊢ χ' = h.χ m

Tactic:
h.uniq this

Premises used: CategoryTheory.SubobjectRepresentableBy.uniq
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
this : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow
⊢ χ' = h.χ m

Tactic:
exact h.uniq this

Premises used: CategoryTheory.SubobjectRepresentableBy.uniq
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
mp : HasSubobjectClassifier.{v, u} C → IsRepresentable (Subobject.presheaf C)
mpr : IsRepresentable (Subobject.presheaf C) → HasSubobjectClassifier.{v, u} C
⊢ HasSubobjectClassifier.{v, u} C ↔ IsRepresentable (Subobject.presheaf C)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
h : HasSubobjectClassifier.{v, u} C
mp : ∀ (𝒞 : Subobject.Classifier.{v, u} C), IsRepresentable (Subobject.presheaf C)
⊢ IsRepresentable (Subobject.presheaf C)

Tactic:
obtain ⟨⟨𝒞⟩⟩ := h
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
𝒞 : Subobject.Classifier.{v, u} C
mp : RepresentableBy (Subobject.presheaf C) 𝒞.Ω
mp₁ : C
⊢ IsRepresentable (Subobject.presheaf C)

Tactic:
apply RepresentableBy.isRepresentable

Premises used: CategoryTheory.Functor.RepresentableBy.isRepresentable
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
h : IsRepresentable (Subobject.presheaf C)
mpr : ∀ (Ω : C) (h : RepresentableBy (Subobject.presheaf C) Ω), HasSubobjectClassifier.{v, u} C
⊢ HasSubobjectClassifier.{v, u} C

Tactic:
obtain ⟨Ω, ⟨h⟩⟩ := h
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : RepresentableBy (Subobject.presheaf C) Ω
mpr : Nonempty (Subobject.Classifier.{v, u} C)
⊢ HasSubobjectClassifier.{v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : RepresentableBy (Subobject.presheaf C) Ω
mpr : Subobject.Classifier.{v, u} C
⊢ Nonempty (Subobject.Classifier.{v, u} C)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : RepresentableBy (Subobject.presheaf C) Ω
⊢ Subobject.Classifier.{v, u} C

Tactic:
exact SubobjectRepresentableBy.classifier h

Premises used: CategoryTheory.SubobjectRepresentableBy.classifier
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞₁ 𝒞₂ 𝒞₃ : Classifier.{v, u} C
⊢ 𝒞₁.hom 𝒞₂ ≫ 𝒞₂.hom 𝒞₃ = 𝒞₁.hom 𝒞₃

Tactic:
𝒞₃.uniq _ <| (𝒞₂.isPullback _).paste_vert (𝒞₃.isPullback _)

Premises used: CategoryTheory.Subobject.Classifier.uniq, CategoryTheory.IsPullback.paste_vert, CategoryTheory.Subobject.Classifier.hom, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞₁ : Classifier.{v, u} C
⊢ 𝒞₁.hom 𝒞₁ = 𝟙 𝒞₁.Ω

Tactic:
(𝒞₁.uniq (χ₀' := 𝟙 _) 𝒞₁.truth IsPullback.of_id_snd).symm

Premises used: CategoryTheory.IsPullback.of_id_snd, CategoryTheory.Subobject.Classifier.uniq, CategoryTheory.Subobject.Classifier.hom, CategoryTheory.Subobject.Classifier.truth, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞₁ 𝒞₂ : Classifier.{v, u} C
X Y : C
m : X ⟶ Y
inst_1 : Mono m
⊢ 𝒞₁.χ m ≫ 𝒞₁.hom 𝒞₂ = 𝒞₂.χ m

Tactic:
𝒞₂.uniq m ((𝒞₁.isPullback m).paste_vert (𝒞₂.isPullback 𝒞₁.truth))

Premises used: CategoryTheory.Subobject.Classifier.uniq, CategoryTheory.IsPullback.paste_vert, CategoryTheory.Subobject.Classifier.truth, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞₁ 𝒞₂ : Classifier.{v, u} C
⊢ 𝒞₁.truth ≫ 𝒞₁.hom 𝒞₂ = 𝒞₂.χ₀ 𝒞₁.Ω₀ ≫ 𝒞₂.truth

Tactic:
(𝒞₂.isPullback _).w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.Subobject.Classifier.hom, CategoryTheory.CommSq.w, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞₁ 𝒞₂ : Classifier.{v, u} C
⊢ IsIso (𝒞₁.hom 𝒞₂)

Tactic:
(𝒞₁.uniqueUpToIso 𝒞₂).isIso_hom

Premises used: CategoryTheory.Subobject.Classifier.uniqueUpToIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.Subobject.Classifier.hom
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
rw : IsPullback m (𝒞.χ₀ F ≫ eΩ₀.hom) (𝒞.χ m ≫ eΩ.hom) t
⊢ IsPullback m (from' F) (𝒞.χ m ≫ eΩ.hom) t

Tactic:
rw [eΩ₀.comp_inv_eq.mp (Subsingleton.elim (from' F ≫ eΩ₀.inv) (𝒞.χ₀ F))]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Subobject.Classifier.χ₀, CategoryTheory.CategoryStruct.comp, Iff.mp, Subsingleton.elim, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
⊢ CommSq 𝒞.truth eΩ₀.hom eΩ.hom t

Tactic:
simp [ht]
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
⊢ IsPullback m (𝒞.χ₀ F ≫ eΩ₀.hom) (𝒞.χ m ≫ eΩ.hom) t

Tactic:
exact (𝒞.isPullback m).paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))

Premises used: CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsPullback.of_vert_isIso_mono, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
apply : IsPullback m (χ₀' ≫ eΩ₀.inv) (χ' ≫ eΩ.inv) 𝒞.truth
⊢ χ' ≫ eΩ.inv = 𝒞.χ m

Tactic:
apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)

Premises used: CategoryTheory.Subobject.Classifier.uniq
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ CommSq t eΩ₀.inv eΩ.inv 𝒞.truth

Tactic:
simp [ht]
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ IsPullback m (χ₀' ≫ eΩ₀.inv) (χ' ≫ eΩ.inv) 𝒞.truth

Tactic:
exact hχ'.paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))

Premises used: CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsPullback.of_vert_isIso_mono
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ χ' ≫ eΩ.inv = 𝒞.χ m

Tactic:
have : χ' ≫ eΩ.inv = 𝒞.χ m := by
      apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)
      exact hχ'.paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
this : χ' ≫ eΩ.inv = 𝒞.χ m
⊢ χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
simpa using this =≫ eΩ.hom

Premises used: CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
commfst : e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m
commsnd :
  e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))
commf :
  e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
    (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))
commg :
  e.functor.map 𝒞₁.truth ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
    Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) ≫ e.functor.map 𝒞₁.truth
⊢ IsPullback m (e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)))
    (e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))) (e.functor.map 𝒞₁.truth)

Tactic:
apply ((𝒞₁.isPullback (e.inverse.map m)).map e.functor).of_iso (e.counitIso.app _)
      (e.counitIso.app _) (.refl _) (.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map, CategoryTheory.IsPullback.of_iso, CategoryTheory.Iso.app, CategoryTheory.IsPullback.map, CategoryTheory.Subobject.Classifier.isPullback, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
⊢ e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
⊢ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
⊢ e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
    (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
⊢ e.functor.map 𝒞₁.truth ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
    Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) ≫ e.functor.map 𝒞₁.truth

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
apply :
  IsPullback (e.inverse.map m) (e.inverse.map χ₀' ≫ e.unitInv.app 𝒞₁.Ω₀) (e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω)
    𝒞₁.truth
⊢ e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)

Tactic:
apply 𝒞₁.uniq (e.inverse.map m) (χ₀' := e.inverse.map χ₀' ≫ e.unitInv.app _)

Premises used: CategoryTheory.Subobject.Classifier.uniq, CategoryTheory.Functor.map, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ IsPullback (e.inverse.map m) (e.inverse.map χ₀' ≫ e.unitInv.app 𝒞₁.Ω₀) (e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω)
    𝒞₁.truth

Tactic:
(hχ'.map e.inverse).paste_vert <| IsPullback.of_vert_isIso_mono .mk

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsPullback.map, CategoryTheory.IsPullback.of_vert_isIso_mono, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ IsPullback (e.inverse.map m) (e.inverse.map χ₀' ≫ e.unitInv.app 𝒞₁.Ω₀) (e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω)
    𝒞₁.truth

Tactic:
exact (hχ'.map e.inverse).paste_vert <| IsPullback.of_vert_isIso_mono .mk

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsPullback.map, CategoryTheory.IsPullback.of_vert_isIso_mono, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)

Tactic:
have : e.inverse.map χ' ≫ e.unitInv.app _ = 𝒞₁.χ (e.inverse.map m) := by
      apply 𝒞₁.uniq (e.inverse.map m) (χ₀' := e.inverse.map χ₀' ≫ e.unitInv.app _)
      exact (hχ'.map e.inverse).paste_vert <| IsPullback.of_vert_isIso_mono .mk
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
this : e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)
⊢ χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
simpa using congr(e.counitInv.app G ≫ e.functor.map $this)

Premises used: CategoryTheory.Equivalence.counitInv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Subobject.Comma
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
inst_2 : HasFiniteLimits.{v₁, u₁} C
inst_3 : PreservesFiniteLimits T
A : StructuredArrow S T
refine :
  ∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst_4 : Mono f] [inst_5 : Mono g] (i : A_1 ≅ B),
    i.hom ≫ g = f →
      Eq (α := Subobject.{v₁, u₁} A.right)
        ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) A_1 f inst_4)
        ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) B g inst_5)
⊢ Subobject A → Subobject.{v₁, u₁} A.right

Tactic:
refine Subobject.lift (fun P f hf => Subobject.mk f.right) ?_
-- Module: Mathlib.CategoryTheory.Subobject.Comma
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
inst_2 : HasFiniteLimits.{v₁, u₁} C
inst_3 : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ Eq (α := Subobject.{v₁, u₁} A.right)
    ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) P f hf)
    ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) Q g hg)

Tactic:
Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i) ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Functor.mapIso