awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
h : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ X
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g ⊗ₘ h))
    ((𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))) ≫ (f ⊗ₘ g ⊗ₘ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X : C
f : Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom (ρ_ (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X))))
      (f, PUnit.unit) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
            (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
              (tensorUnit.{v, u} C (𝒞 := inst))))
          (𝟙 (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X) ⊗ₘ
            ↾fun (x : (𝟙_ (Type v)) (𝒞 := types)) ↦ 𝟙 (unop (op (tensorUnit.{v, u} C (𝒞 := inst)))))
          (CategoryStruct.comp (Y :=
            Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
              (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))))
            ((fun (X Y : C) ↦
                (↾fun
                      (p :
                        tensorObj (𝒞 := types)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
                  tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                    Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                      (tensorObj.{v, u} (𝒞 := inst) X Y)))
              X (tensorUnit.{v, u} C (𝒞 := inst)))
            (Functor.map (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) (Iso.hom (ρ_ X))))))
      (f, PUnit.unit)

Tactic:
simp [unitors_inv_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_inv_equal
-- Module: Mathlib.CategoryTheory.Monoidal.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
X Y Z T : WideSubcategory P
⊢ Eq (α :=
    (tensorObj.{v_1, u_1} (𝒞 := category P) (tensorObj.{v_1, u_1} (𝒞 := category P) X Y)
            (tensorObj.{v_1, u_1} (𝒞 := category P) Z T)).obj
        (_P := P) ⟶
      (tensorObj.{v_1, u_1} (𝒞 := category P) (tensorObj.{v_1, u_1} (𝒞 := category P) X Z)
            (tensorObj.{v_1, u_1} (𝒞 := category P) Y T)).obj
        (_P := P))
    (InducedWideCategory.Hom.hom (P := P) (tensorμ X Y Z T))
    (tensorμ (X.obj (_P := P)) (Y.obj (_P := P)) (Z.obj (_P := P)) (T.obj (_P := P)))

Tactic:
rfl

Premises used: CategoryTheory.MonoidalCategory.tensorμ, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : SymmetricCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c c' : WideSubcategory P
h :
  InducedWideCategory.Hom.hom (P := P) (Iso.hom (β_ c c') ≫ Iso.hom (β_ c' c)) =
    InducedWideCategory.Hom.hom (P := P) (𝟙 (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := category P) c c'))
⊢ Iso.hom (β_ c c') ≫ Iso.hom (β_ c' c) = 𝟙 (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := category P) c c')

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : SymmetricCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c c' : WideSubcategory P
⊢ InducedWideCategory.Hom.hom (P := P) (Iso.hom (β_ c c') ≫ Iso.hom (β_ c' c)) =
    InducedWideCategory.Hom.hom (P := P) (𝟙 (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := category P) c c'))

Tactic:
SymmetricCategory.symmetry _ _

Premises used: CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.Monoidal.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : SymmetricCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c c' : WideSubcategory P
⊢ InducedWideCategory.Hom.hom (P := P) (Iso.hom (β_ c c') ≫ Iso.hom (β_ c' c)) =
    InducedWideCategory.Hom.hom (P := P) (𝟙 (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := category P) c c'))

Tactic:
exact SymmetricCategory.symmetry _ _

Premises used: CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : MorphismProperty.{v, u} C
⊢ P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) ⊤ fun (x x_1 : C) (x_2 : x ⟶ x_1) ↦ True

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W W' : MorphismProperty.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
h₁ : ∀ (X Y : C) (f : X ⟶ Y), W f = W' f
⊢ W = W'

Tactic:
funext X Y f
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W W' : MorphismProperty.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
h₁ h₂ : W' f = W' f
⊢ W f = W' f

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ⊤ f

Tactic:
simp only [top_eq]

Premises used: CategoryTheory.MorphismProperty.top_eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : MorphismProperty.{v, u} C
h : P = ⊤
X Y : C
f : X ⟶ Y
⊢ P f

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W W' : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (W ⊔ W') f ↔ W f ∨ W' f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
S : Set (MorphismProperty.{v, u} C)
X Y : C
f : X ⟶ Y
⊢ sSup S f ↔ ∃ W ∈ S, W f

Tactic:
simp +instances [MorphismProperty]

Premises used: CategoryTheory.MorphismProperty
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ iSup W f ↔ ∃ (i : ι), W i f

Tactic:
simp [← sSup_range]

Premises used: sSup_range
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W W' : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (W ⊓ W') f ↔ W f ∧ W' f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
S : Set (MorphismProperty.{v, u} C)
X Y : C
f : X ⟶ Y
⊢ sInf S f ↔ ∀ W ∈ S, W f

Tactic:
simp +instances [MorphismProperty]

Premises used: CategoryTheory.MorphismProperty
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ iInf W f ↔ ∀ (i : ι), W i f

Tactic:
simp [← sInf_range]

Premises used: sInf_range
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.op.unop = P

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : MorphismProperty.{v, u} Cᵒᵖ
⊢ P.unop.op = P

Tactic:
rfl

Premises used: Quiver.Hom.op, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage F f ↔ P (F.map f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ (P.inverseImage F).op = P.op.inverseImage F.op

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ Monotone (β := MorphismProperty.{v, u} C) fun (P : MorphismProperty.{v_1, u_1} D) ↦ P.inverseImage F

Tactic:
fun _ _ h _ _ _ hf ↦ h _ hf

Premises used: CategoryTheory.MorphismProperty.inverseImage, Monotone, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.inverseImage (𝟭 C) = P

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
P : MorphismProperty.{v_2, u_2} E
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
⊢ (P.inverseImage G).inverseImage F = P.inverseImage (F ⋙ G)

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.strictMap F (F.map f)

Tactic:
⟨hf⟩

Premises used: CategoryTheory.MorphismProperty.strictMap.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ Monotone (β := MorphismProperty.{v_1, u_1} D) fun (P : MorphismProperty.{v, u} C) ↦ P.strictMap F

Tactic:
fun _ _ h _ _ _ ⟨hf⟩ ↦ ⟨h _ hf⟩

Premises used: Monotone, _private.0.CategoryTheory.MorphismProperty.monotone_strictMap.match_1, CategoryTheory.MorphismProperty.strictMap.map, CategoryTheory.MorphismProperty.strictMap
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.strictMap (𝟭 C) f ↔ P f
⊢ P.strictMap (𝟭 C) = P

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ P.strictMap (𝟭 C) f ↔ P f

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.strictMap_id.match_1, Iff.intro, CategoryTheory.MorphismProperty.strictMap.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ P.strictMap (𝟭 C) f ↔ P f

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
h : ∀ ⦃X Y : E⦄ (f : X ⟶ Y), (P.strictMap F).strictMap G f ↔ P.strictMap (F ⋙ G) f
⊢ (P.strictMap F).strictMap G = P.strictMap (F ⋙ G)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : E
f : X ⟶ Y
⊢ (P.strictMap F).strictMap G f ↔ P.strictMap (F ⋙ G) f

Tactic:
⟨fun ⟨⟨h⟩⟩ ↦ ⟨h⟩, fun ⟨h⟩ ↦ ⟨⟨h⟩⟩⟩

Premises used: CategoryTheory.Functor.comp, Iff.intro, CategoryTheory.MorphismProperty.strictMap.map, _private.0.CategoryTheory.MorphismProperty.strictMap_strictMap.match_2, _private.0.CategoryTheory.MorphismProperty.strictMap_strictMap.match_1, CategoryTheory.MorphismProperty.strictMap
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : E
f : X ⟶ Y
⊢ (P.strictMap F).strictMap G f ↔ P.strictMap (F ⋙ G) f

Tactic:
exact ⟨fun ⟨⟨h⟩⟩ ↦ ⟨h⟩, fun ⟨h⟩ ↦ ⟨⟨h⟩⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P : MorphismProperty.{v, u} C
P' : MorphismProperty.{v_1, u_1} D
⊢ P.strictMap F ≤ P' ↔ P ≤ P'.inverseImage F

Tactic:
⟨fun h _ _ _ hf ↦ h _ ⟨hf⟩, fun h _ _ _ ⟨hf⟩ ↦ h _ hf⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.strictMap_le_iff_le_inverseImage.match_1, CategoryTheory.Functor.map, Iff.intro, CategoryTheory.MorphismProperty.strictMap.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ GaloisConnection (fun (x : MorphismProperty.{v, u} C) ↦ x.strictMap F) fun (x : MorphismProperty.{v_1, u_1} D) ↦
    x.inverseImage F

Tactic:
strictMap_le_iff_le_inverseImage F

Premises used: CategoryTheory.MorphismProperty.strictMap_le_iff_le_inverseImage, GaloisConnection
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
⊢ P ≤ (P.strictMap F).inverseImage F

Tactic:
(gc_strictMap F).le_u_l P

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.le_u_l
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ (P.inverseImage F).strictMap F ≤ P

Tactic:
(gc_strictMap F).l_u_le P

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.l_u_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
⊢ ((P.strictMap F).inverseImage F).strictMap F = P.strictMap F

Tactic:
(gc_strictMap F).l_u_l_eq_l P

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.l_u_l_eq_l
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ ((P.inverseImage F).strictMap F).inverseImage F = P.inverseImage F

Tactic:
(gc_strictMap F).u_l_u_eq_u P

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ strictMap ⊥ F = ⊥

Tactic:
(gc_strictMap F).l_bot

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.l_bot
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ (strictMap ⊤ F).inverseImage F = ⊤

Tactic:
(gc_strictMap F).u_l_top

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.u_l_top
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ inverseImage ⊥ F = ⊥

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ inverseImage ⊤ F = ⊤

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P P' : MorphismProperty.{v, u} C
⊢ (P ⊔ P').strictMap F = P.strictMap F ⊔ P'.strictMap F

Tactic:
(gc_strictMap F).l_sup

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.l_sup
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
ι : Type u_3
P : ι → MorphismProperty.{v, u} C
⊢ strictMap (⨆ (i : ι), P i) F = ⨆ (i : ι), (P i).strictMap F

Tactic:
(gc_strictMap F).l_iSup

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.l_iSup
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P : Set (MorphismProperty.{v, u} C)
⊢ (sSup P).strictMap F = ⨆ P' ∈ P, P'.strictMap F

Tactic:
(gc_strictMap F).l_sSup

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.l_sSup
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P P' : MorphismProperty.{v_1, u_1} D
⊢ (P ⊓ P').inverseImage F = P.inverseImage F ⊓ P'.inverseImage F

Tactic:
(gc_strictMap F).u_inf

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.u_inf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
ι : Type u_3
P : ι → MorphismProperty.{v_1, u_1} D
⊢ inverseImage (⨅ (i : ι), P i) F = ⨅ (i : ι), (P i).inverseImage F

Tactic:
(gc_strictMap F).u_iInf

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.u_iInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P : Set (MorphismProperty.{v_1, u_1} D)
⊢ (sInf P).inverseImage F = ⨅ P' ∈ P, P'.inverseImage F

Tactic:
(gc_strictMap F).u_sInf

Premises used: CategoryTheory.MorphismProperty.gc_strictMap, GaloisConnection.u_sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P P' : MorphismProperty.{v_1, u_1} D
⊢ (P ⊔ P').inverseImage F = P.inverseImage F ⊔ P'.inverseImage F

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
ι : Type u_3
P : ι → MorphismProperty.{v_1, u_1} D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), inverseImage (⨆ (i : ι), P i) F f ↔ (⨆ (i : ι), (P i).inverseImage F) f
⊢ inverseImage (⨆ (i : ι), P i) F = ⨆ (i : ι), (P i).inverseImage F

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
ι : Type u_3
P : ι → MorphismProperty.{v_1, u_1} D
X Y : C
f : X ⟶ Y
⊢ inverseImage (⨆ (i : ι), P i) F f ↔ (⨆ (i : ι), (P i).inverseImage F) f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P : Set (MorphismProperty.{v_1, u_1} D)
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (sSup P).inverseImage F f ↔ (⨆ P' ∈ P, P'.inverseImage F) f
⊢ (sSup P).inverseImage F = ⨆ P' ∈ P, P'.inverseImage F

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P : Set (MorphismProperty.{v_1, u_1} D)
X Y : C
f : X ⟶ Y
⊢ (sSup P).inverseImage F f ↔ (⨆ P' ∈ P, P'.inverseImage F) f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.map F (F.map f)

Tactic:
⟨X, Y, f, hf, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.MorphismProperty.map, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : D
f : X ⟶ Y
this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk (F.map f') ≅ Arrow.mk f), Q.map F f
⊢ (fun (x : MorphismProperty.{v, u} C) ↦ x.map F) P f → (fun (x : MorphismProperty.{v, u} C) ↦ x.map F) Q f

Tactic:
⟨X', Y', f', hf', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q.map F f

Tactic:
⟨X', Y', f', h _ hf', ⟨e⟩⟩

Premises used: Nonempty.intro, CategoryTheory.MorphismProperty.map, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q.map F f

Tactic:
exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
rw : ⊤ ≤ map ⊤ F
⊢ map ⊤ F = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
X Y : D
f : X ⟶ Y
_ : ⊤ f → map ⊤ F f
⊢ ⊤ f → map ⊤ F f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
X Y : D
f : X ⟶ Y
h : ⊤ f
⊢ map ⊤ F f

Tactic:
⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩

Premises used: CategoryTheory.Functor.preimage, Nonempty.intro, CategoryTheory.Functor.objPreimage, CategoryTheory.MorphismProperty.map, Exists.intro, True.intro