awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
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
refine : Iso.hom (Iso.refl (Arrow.mk f).left) ≫ (Arrow.mk (f ≫ e)).hom = (Arrow.mk f).hom ≫ (asIso e).hom
⊢ P (f ≫ e)

Tactic:
refine hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf

Premises used: CategoryTheory.Iso.refl, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.mk, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
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
⊢ Iso.hom (Iso.refl (Arrow.mk f).left) ≫ (Arrow.mk (f ≫ e)).hom = (Arrow.mk f).hom ≫ (asIso e).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.isoClosure = P ↔ P.RespectsIso

Tactic:
⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩

Premises used: Eq.rec, le_antisymm, Iff.intro, CategoryTheory.MorphismProperty.le_isoClosure, CategoryTheory.MorphismProperty.isoClosure_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
refine : ∀ (hP : P.RespectsIso), P.isoClosure ≤ P
⊢ P.isoClosure = P ↔ P.RespectsIso

Tactic:
refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk f' ≅ Arrow.mk f), P f
⊢ P.isoClosure f → P f

Tactic:
⟨X', Y', f', hf', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ P f

Tactic:
(P.arrow_mk_iso_iff e).1 hf'

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ P f

Tactic:
exact (P.arrow_mk_iso_iff e).1 hf'

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 rwa rwa₁ rwa₂ rwa₃ : P.RespectsIso
⊢ P.isoClosure = P

Tactic:
rwa [isoClosure_eq_iff]

Premises used: CategoryTheory.MorphismProperty.isoClosure_eq_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.isoClosure.isoClosure = P.isoClosure

Tactic:
P.isoClosure.isoClosure_eq_self

Premises used: CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.MorphismProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
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
mpr : P ≤ Q → P.isoClosure ≤ Q
⊢ P.isoClosure ≤ Q ↔ P ≤ Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
⊢ P.isoClosure ≤ Q → P ≤ Q

Tactic:
P.le_isoClosure.trans

Premises used: LE.le.trans, CategoryTheory.MorphismProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
⊢ P.isoClosure ≤ Q → P ≤ Q

Tactic:
exact P.le_isoClosure.trans

Premises used: LE.le.trans, CategoryTheory.MorphismProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
h : P ≤ Q
rw rw₁ : Q ≤ Q
⊢ Q.isoClosure ≤ Q

Tactic:
rw [Q.isoClosure_eq_self]

Premises used: CategoryTheory.MorphismProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.RespectsIso
h : P ≤ Q
⊢ P.isoClosure ≤ Q

Tactic:
exact (monotone_isoClosure h).trans (by rw [Q.isoClosure_eq_self])

Premises used: LE.le.trans, CategoryTheory.MorphismProperty.monotone_isoClosure
-- 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.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure

Tactic:
fun _ _ _ ⟨⟨_, _, _, hf, ⟨i⟩⟩⟩ ↦ ⟨_, _, _, ⟨hf⟩, ⟨F.mapArrow.mapIso i⟩⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.isoClosure_strictMap_le.match_1, Nonempty.intro, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.MorphismProperty.strictMap.map, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.mapIso, CategoryTheory.MorphismProperty.strictMap, CategoryTheory.Functor.obj
-- 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
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
h : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), W.map F f ↔ (W.strictMap F).isoClosure f
⊢ W.map F = (W.strictMap F).isoClosure

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
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

Tactic:
⟨fun ⟨_, _, f, hf, hf'⟩ ↦ ⟨_, _, _, ⟨hf⟩, hf'⟩, fun ⟨_, _, f, hf, hf'⟩ ↦ ?_⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.map_eq_isoClosure.match_1, CategoryTheory.Functor.map, _private.0.CategoryTheory.MorphismProperty.map_eq_isoClosure.match_2, CategoryTheory.MorphismProperty.map, Iff.intro, Exists.intro, CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.MorphismProperty.strictMap.map, CategoryTheory.MorphismProperty.strictMap, CategoryTheory.Functor.obj
-- 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
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X Y : D
f : X ⟶ Y
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
⊢ W.map F f ↔ (W.strictMap F).isoClosure f

Tactic:
refine ⟨fun ⟨_, _, f, hf, hf'⟩ ↦ ⟨_, _, _, ⟨hf⟩, hf'⟩, fun ⟨_, _, f, hf, hf'⟩ ↦ ?_⟩
-- 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
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X Y : D
f_1 : X ⟶ Y
h_1 : (W.strictMap F).isoClosure f_1
w w_1 : D
f : w ⟶ w_1
hf : W.strictMap F f
hf' : Nonempty.{v_1 + 1} (Arrow.mk f ≅ Arrow.mk f_1)
h :
  ∀ ⦃X_1 Y_1 : D⦄ {X_2 Y_2 : C} {f : X_2 ⟶ Y_2} (hf : W f)
    (hf' : Nonempty.{v_1 + 1} (Arrow.mk (F.map f) ≅ Arrow.mk f_1)), W.map F f_1
⊢ W.map F f_1

Tactic:
obtain ⟨hf⟩ := hf
-- 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
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X_1 Y_1 : D
f : X_1 ⟶ Y_1
h : (W.strictMap F).isoClosure f
X Y : D
X_2 Y_2 : C
f_1 : X_2 ⟶ Y_2
hf : W f_1
hf' : Nonempty.{v_1 + 1} (Arrow.mk (F.map f_1) ≅ Arrow.mk f)
⊢ W.map F f

Tactic:
⟨_, _, _, hf, hf'⟩

Premises used: 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
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X_1 Y_1 : D
f : X_1 ⟶ Y_1
h : (W.strictMap F).isoClosure f
X Y : D
X_2 Y_2 : C
f_1 : X_2 ⟶ Y_2
hf : W f_1
hf' : Nonempty.{v_1 + 1} (Arrow.mk (F.map f_1) ≅ Arrow.mk f)
⊢ W.map F f

Tactic:
exact ⟨_, _, _, hf, hf'⟩
-- 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
rw : (P.strictMap F).isoClosure.RespectsIso
⊢ (P.map F).RespectsIso

Tactic:
rw [map_eq_isoClosure]

Premises used: CategoryTheory.MorphismProperty.map_eq_isoClosure
-- 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).isoClosure.RespectsIso

Tactic:
infer_instance
-- 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
Q : MorphismProperty.{v_1, u_1} D
inst_2 : Q.RespectsIso
rw : (P.strictMap F).isoClosure ≤ Q ↔ P ≤ Q.inverseImage F
rw₁ : P.strictMap F ≤ Q ↔ P ≤ Q.inverseImage F
rw₂ rw₃ : P ≤ Q.inverseImage F ↔ P ≤ Q.inverseImage F
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F

Tactic:
rw [map_eq_isoClosure, isoClosure_le_iff, strictMap_le_iff_le_inverseImage]

Premises used: CategoryTheory.MorphismProperty.isoClosure_le_iff, CategoryTheory.MorphismProperty.strictMap_le_iff_le_inverseImage, CategoryTheory.MorphismProperty.map_eq_isoClosure
-- 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
a : P.isoClosure.map F ≤ P.map F
a₁ : P.map F ≤ P.isoClosure.map F
⊢ P.isoClosure.map F = P.map F

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
a : P.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure
⊢ P.isoClosure.map F ≤ P.map F

Tactic:
rw [map_eq_isoClosure, map_eq_isoClosure, isoClosure_le_iff]

Premises used: CategoryTheory.MorphismProperty.isoClosure_le_iff, CategoryTheory.MorphismProperty.map_eq_isoClosure
-- 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.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure

Tactic:
isoClosure_strictMap_le _ _

Premises used: CategoryTheory.MorphismProperty.isoClosure_strictMap_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.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure

Tactic:
exact isoClosure_strictMap_le _ _

Premises used: CategoryTheory.MorphismProperty.isoClosure_strictMap_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.map F ≤ P.isoClosure.map F

Tactic:
monotone_map _ (le_isoClosure P)

Premises used: CategoryTheory.MorphismProperty.monotone_map, CategoryTheory.MorphismProperty.le_isoClosure
-- 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.map F ≤ P.isoClosure.map F

Tactic:
exact monotone_map _ (le_isoClosure P)

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

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.isoClosure, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
rw : P.isoClosure = P
rw₁ rw₂ : P = P
⊢ P.map (𝟭 C) = P

Tactic:
rw [map_id_eq_isoClosure, P.isoClosure_eq_self]

Premises used: CategoryTheory.MorphismProperty.isoClosure_eq_self, CategoryTheory.MorphismProperty.map_id_eq_isoClosure
-- 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
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
a : (P.map F).map G ≤ P.map (F ⋙ G)
a₁ : P.map (F ⋙ G) ≤ (P.map F).map G
⊢ (P.map F).map G = P.map (F ⋙ G)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
a : P.map F ≤ (P.map (F ⋙ G)).inverseImage G
⊢ (P.map F).map G ≤ P.map (F ⋙ G)

Tactic:
rw [map_le_iff]

Premises used: CategoryTheory.MorphismProperty.map_le_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
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : D
f : X ⟶ Y
a : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk (F.map f') ≅ Arrow.mk f), (P.map (F ⋙ G)).inverseImage G f
⊢ P.map F f → (P.map (F ⋙ G)).inverseImage G 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
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ (P.map (F ⋙ G)).inverseImage G f

Tactic:
⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩

Premises used: CategoryTheory.MorphismProperty.inverseImage, Nonempty.intro, CategoryTheory.MorphismProperty.map, Exists.intro, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.mapIso
-- 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
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ (P.map (F ⋙ G)).inverseImage G f

Tactic:
exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso 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
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
a : P ≤ ((P.map F).map G).inverseImage (F ⋙ G)
⊢ P.map (F ⋙ G) ≤ (P.map F).map G

Tactic:
rw [map_le_iff]

Premises used: CategoryTheory.MorphismProperty.map_le_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
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : C
f : X ⟶ Y
hf : P f
⊢ ((P.map F).map G).inverseImage (F ⋙ G) f

Tactic:
map_mem_map _ _ _ (map_mem_map _ _ _ hf)

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.map, CategoryTheory.MorphismProperty.map_mem_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
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : C
f : X ⟶ Y
hf : P f
⊢ ((P.map F).map G).inverseImage (F ⋙ G) f

Tactic:
exact map_mem_map _ _ _ (map_mem_map _ _ _ hf)

Premises used: CategoryTheory.MorphismProperty.map_mem_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
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P.inverseImage F f
⊢ P.inverseImage F (e ≫ f)

Tactic:
simpa [MorphismProperty.inverseImage, cancel_left_of_respectsIso] using hf

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- 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
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P.inverseImage F f
⊢ P.inverseImage F (f ≫ e)

Tactic:
simpa [MorphismProperty.inverseImage, cancel_right_of_respectsIso] using hf

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- 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 G : Functor.{v, v_1, u, u_1} C D
e : F ≅ G
revert : ∀ {F G : Functor.{v, v_1, u, u_1} C D} (e : F ≅ G), P.map F = P.map G
⊢ P.map F = P.map G

Tactic:
revert F G 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
P : MorphismProperty.{v, u} C
suffices : ∀ {F G : Functor.{v, v_1, u, u_1} C D} (x : F ≅ G), P.map F ≤ P.map G
⊢ ∀ {F G : Functor.{v, v_1, u, u_1} C D} (e : F ≅ G), P.map F = P.map G

Tactic:
suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
    fun F G e => le_antisymm (this e) (this e.symm)
-- 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 G : Functor.{v, v_1, u, u_1} C D
e : F ≅ G
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), P.map G f
⊢ P.map F f → P.map G 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
P : MorphismProperty.{v, u} C
F G : Functor.{v, v_1, u, u_1} C D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f

Tactic:
⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩

Premises used: CategoryTheory.Functor.mapArrowFunctor, Nonempty.intro, CategoryTheory.Iso.trans, CategoryTheory.MorphismProperty.map, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- 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 G : Functor.{v, v_1, u, u_1} C D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f

Tactic:
exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ 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
P : MorphismProperty.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ (P.inverseImage F).map F ≤ P.isoClosure

Tactic:
fun _ _ _ ⟨_, _, f, hf, ⟨e⟩⟩ => ⟨_, _, F.map f, hf, ⟨e⟩⟩

Premises used: Nonempty.intro, _private.0.CategoryTheory.MorphismProperty.map_inverseImage_le.match_1, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.Functor.obj
-- 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
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
a : P.inverseImage E.functor ≤ P.map E.inverse
a₁ : P.map E.inverse ≤ P.inverseImage E.functor
⊢ P.inverseImage E.functor = P.map E.inverse

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ P.map E.inverse f

Tactic:
⟨_, _, _, hf, ⟨?_⟩⟩

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
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
a : Arrow.mk (E.inverse.map (E.functor.map f)) ≅ Arrow.mk f
⊢ P.map E.inverse f

Tactic:
refine ⟨_, _, _, hf, ⟨?_⟩⟩
-- 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
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ Arrow.mk (E.inverse.map (E.functor.map f)) ≅ Arrow.mk f

Tactic:
exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- 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
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
a : P ≤ (P.inverseImage E.functor).inverseImage E.inverse
⊢ P.map E.inverse ≤ P.inverseImage E.functor

Tactic:
rw [map_le_iff]

Premises used: CategoryTheory.MorphismProperty.map_le_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
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
X Y : D
f : X ⟶ Y
hf : P f
⊢ (P.inverseImage E.functor).inverseImage E.inverse f

Tactic:
(P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso
-- 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
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
X Y : D
f : X ⟶ Y
hf : P f
⊢ (P.inverseImage E.functor).inverseImage E.inverse f

Tactic:
exact (P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

Premises used: Iff.mpr, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso