awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasImages.{v₁, u₁} C
f : X ⟶ Y
inst_2 : Mono f
⊢ «exists» f = map f

Tactic:
lower_iso _ _ (MonoOver.existsIsoMap f)

Premises used: CategoryTheory.Subobject.exists, CategoryTheory.MonoOver.existsIsoMap, CategoryTheory.Subobject.map, CategoryTheory.Subobject.lower_iso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : X ⟶ Y
x : Subobject.{v₁, u₁} X
this : ImageFactorisation (x.arrow ≫ f) :=
  (Image.imageFactorisation (x.arrow ≫ f)).ofIsoI (I' := Functor.obj underlying ((«exists» f).obj x))
    (Iso.symm (existsIsoImage f x))
⊢ ((«exists» f).obj x).arrow = this.F.m

Tactic:
simpa [this, -Over.w] using (Over.w ((existsCompRepresentativeIso f).app x).hom.hom).symm

Premises used: CategoryTheory.Over.w, CategoryTheory.Iso.app, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Subobject.existsCompRepresentativeIso, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
c : Classifier.{v, u} C
Y : C
f : Y ⟶ c.Ω₀
⊢ c.χ (𝟙 Y) = c.χ₀ Y ≫ c.truth

Tactic:
simp [← (c.isPullback (𝟙 Y)).w]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
c : Classifier.{v, u} C
⊢ IsTerminal.from isTerminalΩ₀ = c.χ₀

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ IsPullback (Y := Classifier.Ω₀.{v, u} (Nonempty.some ⋯)) (Z := Ω.{v, u} C) m (Classifier.χ₀ (Nonempty.some ⋯) U) (χ m)
    (truth C)

Tactic:
Classifier.isPullback _ m

Premises used: CategoryTheory.HasSubobjectClassifier.χ, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Eq (α := U ⟶ Ω.{v, u} C) (m ≫ χ m) (Classifier.χ₀ (Nonempty.some ⋯) U ≫ truth C)

Tactic:
(isPullback_χ m).w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.HasSubobjectClassifier.isPullback_χ
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
χ' : X ⟶ Ω.{v, u} C
hχ' : IsPullback m (Classifier.χ₀ (Nonempty.some ⋯) U) χ' (truth C)
⊢ χ' = χ m

Tactic:
Classifier.uniq _ m hχ'

Premises used: CategoryTheory.HasSubobjectClassifier.χ, CategoryTheory.Subobject.Classifier.uniq
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ IsSplitMono.{v, u} (X := Ω₀.{v, u} C) (truth C)

Tactic:
Subobject.Classifier.isTerminalΩ₀.isSplitMono_from _

Premises used: CategoryTheory.Subobject.Classifier.isTerminalΩ₀, CategoryTheory.Limits.IsTerminal.isSplitMono_from
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ IsRegularMono.{v, u} (X := Ω₀.{v, u} C) (truth C)

Tactic:
⟨⟨truthIsRegularMono⟩⟩

Premises used: Nonempty.intro, CategoryTheory.HasSubobjectClassifier.truthIsRegularMono, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
D : Type u₀
inst_3 : Category.{v₀, u₀} D
F : Functor.{v, v₀, u, u₀} C D
inst_4 : F.Faithful
⊢ F.ReflectsIsomorphisms

Tactic:
reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms F

Premises used: CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasSubobjectClassifier.{v, u} C
U X : C
m : U ⟶ X
inst_2 : Mono m
D : Type u₀
inst_3 : Category.{v₀, u₀} D
F : Functor.{v, v₀, u, u₀} Cᵒᵖ D
inst_4 : F.Faithful
⊢ F.ReflectsIsomorphisms

Tactic:
reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms F

Premises used: CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X : C
φ : X ⟶ 𝒞.Ω
⊢ IsPullback (P := Limits.pullback φ 𝒞.truth) (pullback.fst φ 𝒞.truth) (pullback.snd φ 𝒞.truth) φ 𝒞.truth

Tactic:
IsPullback.of_hasPullback φ 𝒞.truth

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Subobject.Classifier.truth
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X : C
φ : X ⟶ 𝒞.Ω
⊢ IsPullback (P := Limits.pullback φ 𝒞.truth) (pullback.fst φ 𝒞.truth) (pullback.snd φ 𝒞.truth) φ 𝒞.truth

Tactic:
convert! IsPullback.of_hasPullback φ 𝒞.truth

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Subobject.Classifier.truth
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
Z X : C
i : Z ⟶ X
inst_2 : Mono i
⊢ (pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = Subobject.mk i

Tactic:
Subobject.pullback_obj_mk (𝒞.isPullback i).flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.Subobject.pullback_obj_mk, CategoryTheory.Subobject.Classifier.isPullback
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X : C
φ : X ⟶ 𝒞.Ω
obtain : ∀ (Z : C) (i : Z ⟶ X) (w : Mono i), 𝒞.χ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow = 𝒞.χ i
⊢ 𝒞.χ ((pullback φ).obj 𝒞.truth_as_subobject).arrow = φ

Tactic:
obtain ⟨Z, i, _, rfl⟩ := 𝒞.surjective_χ φ

Premises used: CategoryTheory.Subobject.Classifier.surjective_χ, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ 𝒞.χ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow = 𝒞.χ i

Tactic:
(𝒞.uniq _ (?_ : IsPullback _ (𝒞.χ₀ _) _ _)).symm

Premises used: CategoryTheory.Subobject.Classifier.uniq, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
refine :
  IsPullback ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
    (𝒞.χ₀ (obj underlying ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject))) (𝒞.χ i) 𝒞.truth
⊢ 𝒞.χ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow = 𝒞.χ i

Tactic:
refine (𝒞.uniq _ (?_ : IsPullback _ (𝒞.χ₀ _) _ _)).symm

Premises used: CategoryTheory.Subobject.Classifier.uniq, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ 𝒞.χ i ≫ Iso.hom (Iso.refl 𝒞.Ω) = Iso.hom (Iso.refl X) ≫ 𝒞.χ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ 𝒞.truth ≫ Iso.hom (Iso.refl 𝒞.Ω) = Iso.hom (Iso.refl 𝒞.Ω₀) ≫ 𝒞.truth

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
refine :
  pullback.snd 𝒞.truth (𝒞.χ i) ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (underlyingIso (pullback.snd (obj (MonoOver.forget 𝒞.Ω) (MonoOver.mk 𝒞.truth)).hom (𝒞.χ i)))) ≫
      ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
⊢ IsPullback ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
    (𝒞.χ₀ (obj underlying ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject))) (𝒞.χ i) 𝒞.truth

Tactic:
refine (IsPullback.of_hasPullback 𝒞.truth (𝒞.χ i)).flip.of_iso
    (underlyingIso _).symm (Iso.refl _) (Iso.refl _) (Iso.refl _)
    ?_ (𝒞.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)

Premises used: CategoryTheory.Subobject.Classifier.χ, CategoryTheory.Subobject.underlyingIso, CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_iso, CategoryTheory.IsPullback.flip, CategoryTheory.Iso.symm, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Subobject.Classifier.isTerminalΩ₀, CategoryTheory.Subobject.Classifier.truth
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
dsimp :
  pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    Iso.inv (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))) ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (underlyingIso (pullback.snd (obj (MonoOver.forget 𝒞.Ω) (MonoOver.mk 𝒞.truth)).hom (𝒞.χ i)))) ≫
      ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
rw :
  (Subobject.mk (A := Limits.pullback 𝒞.truth (𝒞.χ i)) (pullback.snd 𝒞.truth (𝒞.χ i))).arrow =
    ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    Iso.inv (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))) ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
rw [Iso.eq_inv_comp, comp_id, underlyingIso_hom_comp_eq_mk]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ (Subobject.mk (A := Limits.pullback 𝒞.truth (𝒞.χ i)) (pullback.snd 𝒞.truth (𝒞.χ i))).arrow =
    ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
rfl
-- 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
𝒞 : Classifier.{v, u} C
X : C
φ : X ⟶ 𝒞.Ω
⊢ (fun (x : obj (Subobject.presheaf C) (Opposite.op X)) ↦ 𝒞.χ (arrow x))
      ((fun (φ : X ⟶ 𝒞.Ω) ↦ (pullback φ).obj 𝒞.truth_as_subobject) φ) =
    φ

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
𝒞 : Classifier.{v, u} C
X : C
x : obj (Subobject.presheaf C) (Opposite.op X)
⊢ (fun (φ : X ⟶ 𝒞.Ω) ↦ (pullback φ).obj 𝒞.truth_as_subobject)
      ((fun (x : obj (Subobject.presheaf C) (Opposite.op X)) ↦ 𝒞.χ (arrow x)) x) =
    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
𝒞 : Classifier.{v, u} C
X X' : C
x : X ⟶ X'
x_1 : X' ⟶ 𝒞.Ω
⊢ Eq (α := obj (Subobject.presheaf C) (Opposite.op X))
    (({ toFun := fun (φ : X ⟶ 𝒞.Ω) ↦ (pullback φ).obj 𝒞.truth_as_subobject,
            invFun := fun (x : obj (Subobject.presheaf C) (Opposite.op X)) ↦ 𝒞.χ (arrow x), left_inv := ⋯,
            right_inv := ⋯ } :
          (a : X ⟶ 𝒞.Ω) → (Subobject.presheaf C).obj (Opposite.op X))
        (x ≫ x_1) :
      obj (Subobject.presheaf C) (Opposite.op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Subobject.presheaf C) x.op) :
          (a : (fun (X : Type (max u v)) ↦ X) ((Subobject.presheaf C).obj (Opposite.op X'))) →
            (fun (X : Type (max u v)) ↦ X) ((Subobject.presheaf C).obj (Opposite.op X)))
        (({ toFun := fun (φ : X' ⟶ 𝒞.Ω) ↦ (pullback φ).obj 𝒞.truth_as_subobject,
              invFun := fun (x : obj (Subobject.presheaf C) (Opposite.op X')) ↦ 𝒞.χ (arrow x), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : X' ⟶ 𝒞.Ω) → (Subobject.presheaf C).obj (Opposite.op X'))
          x_1) :
      (fun (X : Type (max u v)) ↦ X) (obj (Subobject.presheaf C) (Opposite.op X)))

Tactic:
simp [pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_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} Ω
X : C
f : X ⟶ Ω
⊢ (h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) f = (Subobject.pullback f).obj h.Ω₀

Tactic:
simpa using h.homEquiv_comp f (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.RepresentableBy.homEquiv_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} Ω
X : C
x : Subobject.{v, u} X
rw :
  (h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X))
      ((Equiv.symm h.homEquiv : (a : (Subobject.presheaf C).obj (Opposite.op X)) → X ⟶ Ω) x) =
    x
rw₁ rw₂ : x = x
⊢ obj (Subobject.pullback ((Equiv.symm h.homEquiv : (a : (Subobject.presheaf C).obj (Opposite.op X)) → X ⟶ Ω) x)) h.Ω₀ =
    x

Tactic:
rw [← homEquiv_eq, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.SubobjectRepresentableBy.homEquiv_eq
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
dsimp :
  Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫
      Over.Hom.left (InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫ pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫ h.π m = pullbackπ (h.χ m) h.Ω₀

Tactic:
dsimp only [π]

Premises used: CategoryTheory.SubobjectRepresentableBy.π
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
rw :
  Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫
      pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫
      Over.Hom.left (InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫ pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀

Tactic:
rw [← Over.comp_left_assoc]

Premises used: CategoryTheory.Over.comp_left_assoc
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ 𝟙 (obj representative ((Subobject.pullback (h.χ m)).obj h.Ω₀)).obj (P := Over.isMono X).left ≫
      pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀

Tactic:
Category.id_comp _

Premises used: 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
h₁ :
  Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) =
    𝟙 (obj representative ((Subobject.pullback (h.χ m)).obj h.Ω₀)).obj (P := Over.isMono X).left
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫
      pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀

Tactic:
convert! Category.id_comp _ using 2

Premises used: 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) =
    𝟙 (obj representative ((Subobject.pullback (h.χ m)).obj h.Ω₀)).obj (P := Over.isMono X).left

Tactic:
(MonoOver.forget _ ⋙ Over.forget _).congr_map (h.iso m).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.SubobjectRepresentableBy.iso, CategoryTheory.Functor.comp, Quotient.map, CategoryTheory.Over.forget, Quotient.mk', CategoryTheory.MonoOver.forget, Quot.map, CategoryTheory.Functor.congr_map
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) =
    𝟙 (obj representative ((Subobject.pullback (h.χ m)).obj h.Ω₀)).obj (P := Over.isMono X).left

Tactic:
exact (MonoOver.forget _ ⋙ Over.forget _).congr_map (h.iso m).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.SubobjectRepresentableBy.iso, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.MonoOver.forget, CategoryTheory.Functor.congr_map
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫ m = ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow

Tactic:
MonoOver.w (h.iso m).inv

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.SubobjectRepresentableBy.iso, CategoryTheory.MonoOver.w, CategoryTheory.Iso.inv
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
commfst :
  ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ m
commsnd :
  Eq (α := obj underlying ((Subobject.pullback (h.χ m)).obj h.Ω₀) ⟶ obj underlying h.Ω₀)
    (pullbackπ (h.χ m) h.Ω₀ ≫ Iso.hom (Iso.refl (obj underlying h.Ω₀)))
    (Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ h.π m)
commf : h.χ m ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl X) ≫ h.χ m
commg : h.Ω₀.arrow ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl (obj underlying h.Ω₀)) ≫ h.Ω₀.arrow
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow

Tactic:
fapply (Subobject.isPullback (h.χ m) h.Ω₀).flip.of_iso
    (((MonoOver.forget _ ⋙ Over.forget _).mapIso (h.iso m)).symm) (Iso.refl _)
    (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.SubobjectRepresentableBy.iso, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_iso, CategoryTheory.SubobjectRepresentableBy.χ, CategoryTheory.IsPullback.flip, CategoryTheory.MonoOver.forget, CategoryTheory.Subobject.isPullback, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso, CategoryTheory.SubobjectRepresentableBy.Ω₀
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ m

Tactic:
simp [MonoOver.forget]

Premises used: CategoryTheory.MonoOver.forget
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Eq (α := obj underlying ((Subobject.pullback (h.χ m)).obj h.Ω₀) ⟶ obj underlying h.Ω₀)
    (pullbackπ (h.χ m) h.Ω₀ ≫ Iso.hom (Iso.refl (obj underlying h.Ω₀)))
    (Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ h.π m)

Tactic:
simp [MonoOver.forget]

Premises used: CategoryTheory.MonoOver.forget
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ h.χ m ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl X) ≫ h.χ m

Tactic:
simp [MonoOver.forget]

Premises used: CategoryTheory.MonoOver.forget
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ h.Ω₀.arrow ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl (obj underlying h.Ω₀)) ≫ h.Ω₀.arrow

Tactic:
simp [MonoOver.forget]

Premises used: CategoryTheory.MonoOver.forget
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
χ' : X ⟶ Ω
π : U ⟶ obj underlying h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
a :
  Eq (α := obj (Subobject.presheaf C) (Opposite.op X))
    ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) χ' :
      obj (Subobject.presheaf C) (Opposite.op X))
    ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) (h.χ m) :
      obj (Subobject.presheaf C) (Opposite.op X))
⊢ χ' = h.χ m

Tactic:
apply h.homEquiv.injective

Premises used: Equiv.injective, CategoryTheory.Functor.RepresentableBy.homEquiv
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
χ' : X ⟶ Ω
π : U ⟶ obj underlying h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
a : (Subobject.pullback χ').obj h.Ω₀ = Subobject.mk m
⊢ Eq (α := obj (Subobject.presheaf C) (Opposite.op X))
    ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) χ' :
      obj (Subobject.presheaf C) (Opposite.op X))
    ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) (h.χ m) :
      obj (Subobject.presheaf C) (Opposite.op X))

Tactic:
simp only [χ, Equiv.apply_symm_apply, homEquiv_eq]

Premises used: Equiv.apply_symm_apply, CategoryTheory.SubobjectRepresentableBy.homEquiv_eq, CategoryTheory.SubobjectRepresentableBy.χ
-- 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} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
χ' : X ⟶ Ω
π : U ⟶ obj underlying h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ (Subobject.pullback χ').obj h.Ω₀ = Subobject.mk m

Tactic:
simpa using Subobject.pullback_obj_mk sq.flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.Subobject.pullback_obj_mk
-- 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),
    (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ 𝟙 X = s.fst

Tactic:
simp