awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj W) (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj W) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z)) ≫
            F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫
              F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z ≫
                F.obj W ◁ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom ≫
                    F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                      Iso.hom
                        (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) =
    Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
      Iso.hom (α_ (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X)) (F.obj Y) (F.obj Z)) ≫
        F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) ◁ (fData.μIso Y Z).hom ≫
          (fData.μIso W X).inv ▷ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z) ≫
            Iso.hom (α_ (F.obj W) (F.obj X) (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
              F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have slice_lhs : Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
    (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
      Iso.hom (α_ (F.obj W) (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj W) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z)) ≫
          (((F.obj W ◁
                    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z)) ≫
                  F.obj W ◁ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z))) ≫
                F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom) ≫
              F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
            Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) =
  Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
    Iso.hom (α_ (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X)) (F.obj Y) (F.obj Z)) ≫
      F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) ◁ (fData.μIso Y Z).hom ≫
        (fData.μIso W X).inv ▷ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z) ≫
          Iso.hom (α_ (F.obj W) (F.obj X) (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
            F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
Tactic: slice_lhs 5 6 =>
      rw [← whiskerLeft_comp, hom_inv_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ Eq (α :=
    F.obj
        (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
          Y) ⟶
      F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (F.map (Iso.hom (α_ X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) Y) ≫ X ◁ Iso.hom (λ_ Y))) (F.map (Iso.hom (ρ_ X) ▷ Y))
have mk : ∀
  (μIso :
    (X Y : D) → tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)),
  (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso X Y₂).hom) →
    (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso X₂ Y).hom) →
      (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
          F.map (f ⊗ₘ g) = (μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso Y₁ Y₂).hom) →
        ∀ (εIso : tensorUnit.{v₁, u₁} C (𝒞 := inst) ≅ F.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))),
          (∀ (X Y Z : D),
              F.map (Iso.hom (α_ X Y Z)) =
                ((Iso.symm (μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≪≫
                      ((μIso X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
                    α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                      (Iso.refl (F.obj X) ⊗ᵢ μIso Y Z) ≪≫ μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)).hom) →
            (∀ (X : D),
                F.map (Iso.hom (λ_ X)) =
                  ((Iso.symm (μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ≪≫ (εIso.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫
                      λ_ (F.obj X)).hom) →
              (∀ (X : D),
                  F.map (Iso.hom (ρ_ X)) =
                    ((Iso.symm (μIso X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso.symm)) ≪≫
                        ρ_ (F.obj X)).hom) →
                Eq (α :=
                  F.obj
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2)
                        (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) Y) ⟶
                    F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
                  (F.map (Iso.hom (α_ X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) Y) ≫ X ◁ Iso.hom (λ_ Y)))
                  (F.map (Iso.hom (ρ_ X) ▷ Y))
Tactic: cases fData
Cleared hypotheses: fData
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Types.Coyoneda (goal)
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
⊢ (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h)) ≫
      Iso.hom (α_ X Y Z) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h))
have h₁ : (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X Y Z) =
  f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h)
Tactic: simp only [Category.assoc, Iso.cancel_iso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Types.Coyoneda (goal)
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
| (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X Y Z)
have rw : tensorUnit.{v, u} C (𝒞 := inst) ◁ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g ⊗ₘ h)
Tactic: rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Types.Coyoneda (goal)
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
⊢ (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X Y Z) =
    f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h)
have h₁ : 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))
  (f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h))
Tactic: conv_lhs =>
        rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Types.Coyoneda (goal)
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
| f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h)
have rw : (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))) ≫ (f ⊗ₘ g ⊗ₘ h)
Tactic: rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Types.Coyoneda (goal)
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))
    (f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h))
have h₁ : 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: conv_rhs => rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Widesubcategory (goal)
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
⊢ Iso.hom (β_ c c') ≫ Iso.hom (β_ c' c) = 𝟙 (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := category P) c c')
have 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'))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
⊢ W = W'
have h₁ : ∀ (X Y : C) (f : X ⟶ Y), W f = W' f
Tactic: funext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
⊢ W f = W' f
have h₁ : W' f = W' f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.strictMap (𝟭 C) = P
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.strictMap (𝟭 C) f ↔ P f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
⊢ (P.strictMap F).strictMap G = P.strictMap (F ⋙ G)
have h : ∀ ⦃X Y : E⦄ (f : X ⟶ Y), (P.strictMap F).strictMap G f ↔ P.strictMap (F ⋙ G) f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), inverseImage (⨆ (i : ι), P i) F f ↔ (⨆ (i : ι), (P i).inverseImage F) f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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)
⊢ (sSup P).inverseImage F = ⨆ P' ∈ P, P'.inverseImage F
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (sSup P).inverseImage F f ↔ (⨆ P' ∈ P, P'.inverseImage F) f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
⊢ (fun (x : MorphismProperty.{v, u} C) ↦ x.map F) P f → (fun (x : MorphismProperty.{v, u} C) ↦ x.map F) Q f
have this : ∀ (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', hf', ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
⊢ map ⊤ F = ⊤
have rw : ⊤ ≤ map ⊤ F
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
have refine_1 : F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y)
Tactic: refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
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
refine_1 : F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y)
⊢ map ⊤ F f
have refine_2 : Arrow.mk (X := F.obj (F.objPreimage X)) (Y := F.obj (F.objPreimage Y))
    (F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))) ≅
  Arrow.mk f
Tactic: refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty.{v, u} C
⊢ Eq (α := Set (Arrow.{v, u} C)) (toSet (⨆ (i : ι), W i)) (⋃ (i : ι), (W i).toSet)
have h : ∀ (x : Arrow.{v, u} C),
  Membership.mem (γ := Set (Arrow.{v, u} C)) (toSet (⨆ (i : ι), W i)) x ↔
    Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : ι), (W i).toSet) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ P f'
have rw : ∀ (hf : Arrow.mk f ∈ P.toSet) {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y')
  (h : f' = eqToHom sorry ≫ f ≫ eqToHom hY), Arrow.mk f' ∈ P.toSet
Tactic: rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢
Cleared hypotheses: hf, X', Y', f', hX, hY, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ ofHoms f g ↔ ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)
have mp : ofHoms f g → ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
mp : ofHoms f g → ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g ↔ ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)
have mpr : (∃ (i : ι), Arrow.mk g = Arrow.mk (f i)) → ofHoms f g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g
have mpr : ofHoms f (f i)
Tactic: rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ ofHoms P.homFamily = P
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), ofHoms P.homFamily f ↔ P f
Tactic: ext _ _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ofHoms P.homFamily f ↔ P f
have h : ofHoms P.homFamily f → P f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h : ofHoms P.homFamily f → P f
⊢ ofHoms P.homFamily f ↔ P f
have h₁ : P f → ofHoms P.homFamily f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : ofHoms P.homFamily f
⊢ P f
have hf₁ : ∃ (i : (↑P.toSet : Type (max u v))), Arrow.mk f = Arrow.mk (P.homFamily i)
Tactic: rw [ofHoms_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∃ (i : (↑P.toSet : Type (max u v))), Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f
have h : ∀ (f : Arrow.{v, u} C) (hf : f ∈ P.toSet),
  P (X := (↑(Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf) : Arrow C).left)
    (P.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf))
Tactic: obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf
Cleared hypotheses: X, Y, f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_3
ι : α → Type u_4
A B : (a : α) → ι a → C
f : (a : α) → (i : ι a) → A a i ⟶ B a i
⊢ Eq (α := MorphismProperty.{v, u} C) (⨆ (a : α), ofHoms (f a))
    (ofHoms (X := fun (j : (a : α) × ι a) ↦ A (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) (Y :=
      fun (j : (a : α) × ι a) ↦ B (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))
      fun (j : (a : α) × ι a) ↦ f (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))
have h : ∀ ⦃f_1 Y : C⦄ (f_2 : f_1 ⟶ Y),
  (⨆ (a : α), ofHoms (f a)) f_2 ↔
    ofHoms (X := fun (j : (a : α) × ι a) ↦ A (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) (Y :=
      fun (j : (a : α) × ι a) ↦ B (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))
      (fun (j : (a : α) × ι a) ↦ f (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) f_2
Tactic: ext f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X Y Z : C
x : X ⟶ Y
hi : Q x
x_1 : Y ⟶ Z
hf : InfSet.sInf W x_1
⊢ InfSet.sInf W (x ≫ x_1)
have rw : ∀ (hf : ∀ W_1 ∈ W, W_1 x_1), ∀ W_1 ∈ W, W_1 (x ≫ x_1)
Tactic: rw [sInf_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsRight Q
X Y Z : C
x : Y ⟶ Z
hi : Q x
x_1 : X ⟶ Y
hf : InfSet.sInf W x_1
⊢ InfSet.sInf W (x_1 ≫ x)
have rw : ∀ (hf : ∀ W_1 ∈ W, W_1 x_1), ∀ W_1 ∈ W, W_1 (x_1 ≫ x)
Tactic: rw [sInf_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (op (isomorphisms C)) (isomorphisms Cᵒᵖ)
have h : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), op (isomorphisms C) f ↔ isomorphisms.{v, u} Cᵒᵖ (X := X) (Y := Y) f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : C
f : X ⟶ Y
⊢ P.isoClosure f → Q.isoClosure f
have this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk f' ≅ Arrow.mk f), Q.isoClosure f
Tactic: ⟨X', Y', f', hf', ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ P (e ≫ f)
have refine : (asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom = (Arrow.mk f).hom ≫ Iso.hom (Iso.refl (Arrow.mk f).right)
Tactic: refine hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ P (f ≫ e)
have refine : Iso.hom (Iso.refl (Arrow.mk f).left) ≫ (Arrow.mk (f ≫ e)).hom = (Arrow.mk f).hom ≫ (asIso e).hom
Tactic: refine hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.isoClosure = P ↔ P.RespectsIso
have refine : ∀ (hP : P.RespectsIso), P.isoClosure ≤ P
Tactic: refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
⊢ P.isoClosure f → P f
have this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk f' ≅ Arrow.mk f), P f
Tactic: ⟨X', Y', f', hf', ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
⊢ P.isoClosure ≤ Q ↔ P ≤ Q
have mp : P.isoClosure ≤ Q → P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
mp : P.isoClosure ≤ Q → P ≤ Q
⊢ P.isoClosure ≤ Q ↔ P ≤ Q
have mpr : P ≤ Q → P.isoClosure ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
h : P ≤ Q
⊢ Q.isoClosure ≤ Q
have rw : Q ≤ Q
Tactic: rw [Q.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
⊢ W.map F = (W.strictMap F).isoClosure
have h : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), W.map F f ↔ (W.strictMap F).isoClosure f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X Y : D
f : X ⟶ Y
⊢ W.map F f ↔ (W.strictMap F).isoClosure f
have h : (W.strictMap F).isoClosure f →
  ∀ (w w_1 : D) (f_1 : w ⟶ w_1) (hf : W.strictMap F f_1) (hf' : Nonempty.{v_1 + 1} (Arrow.mk f_1 ≅ Arrow.mk f)),
    W.map F f
Tactic: refine ⟨fun ⟨_, _, f, hf, hf'⟩ ↦ ⟨_, _, _, ⟨hf⟩, hf'⟩, fun ⟨_, _, f, hf, hf'⟩ ↦ ?_⟩