awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.pt = t.pt

Tactic:
rfl

Premises used: CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.span, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.inl = t.inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.inr = t.inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.flip.inl ≫ Iso.hom (Iso.refl t.flip.flip.pt) = t.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.flip.inr ≫ Iso.hom (Iso.refl t.flip.flip.pt) = t.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
⊢ ∀ (s : PushoutCocone g f), t.inr ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s = s.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
⊢ ∀ (s : PushoutCocone g f), t.inl ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s = s.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
h₀ : t.inl ≫ m = t.inl ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
h₃ : t.inr ≫ m = t.inr ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
⊢ m = (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s

Tactic:
apply IsColimit.hom_ext ht

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ t.inl ≫ m = t.inl ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ t.inr ≫ m = t.inr ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
F : Functor.{0, v, 0, u} WalkingSpan C
t : Cocone F
⊢ Eq (α := (span (F.map fst) (F.map snd)).obj none ⟶ (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app none ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt))
    ((mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
F : Functor.{0, v, 0, u} WalkingSpan C
t : Cocone F
⊢ Eq (α :=
    (span (F.map fst) (F.map snd)).obj (some WalkingPair.left) ⟶
      (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.left) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt))
    ((mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
F : Functor.{0, v, 0, u} WalkingSpan C
t : Cocone F
⊢ Eq (α :=
    (span (F.map fst) (F.map snd)).obj (some WalkingPair.right) ⟶
      (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.right) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt))
    ((mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ s.cone.fst = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ s.cone.snd = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ s.cocone.inl = h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ s.cocone.inr = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
hQ : Q.IsInvertedBy F
h : P ≤ Q
⊢ P.IsInvertedBy F

Tactic:
fun _ _ _ hf => hQ _ (h _ hf)

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
hF : W.IsInvertedBy F
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)

Tactic:
haveI := hF f hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
hF : W.IsInvertedBy F
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
dsimp : IsIso (G.map (F.map f))
⊢ IsIso ((F ⋙ G).map f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
hF : W.IsInvertedBy F
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.map f.unop)

Tactic:
haveI := h f.unop hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso.{v', u'} (C := Dᵒᵖ) (X := Opposite.op (L.obj (Opposite.unop X))) (Y := Opposite.op (L.obj (Opposite.unop Y)))
    (L.map f.unop).op

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.map f.op)

Tactic:
haveI := h f.op hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso.{v', u'} (C := Dᵒᵖ) (X := Opposite.op (L.obj (Opposite.op X))) (Y := Opposite.op (L.obj (Opposite.op Y)))
    (L.map f.op).op

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.map f.unop)

Tactic:
haveI := h f.unop hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
dsimp : IsIso (L.map f.unop).unop
⊢ IsIso (L.leftOp.map f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).unop

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.map f.op)

Tactic:
haveI := h f.op hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
dsimp : IsIso (L.map f.op).unop
⊢ IsIso (L.unop.map f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).unop

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
E₁ : Type u_3
E₂ : Type u_4
inst_2 : Category.{v_3, u_3} E₁
inst_3 : Category.{v_4, u_4} E₂
F₁ : Functor.{v_1, v_3, u_1, u_3} C₁ E₁
F₂ : Functor.{v_2, v_4, u_2, u_4} C₂ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x x_1 : C₁ × C₂
f : x ⟶ x_1
hf : W₁.prod W₂ f
rw : IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2
⊢ IsIso ((F₁.prod F₂).map f)

Tactic:
rw [isIso_prod_iff]

Premises used: CategoryTheory.isIso_prod_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
E₁ : Type u_3
E₂ : Type u_4
inst_2 : Category.{v_3, u_3} E₁
inst_3 : Category.{v_4, u_4} E₂
F₁ : Functor.{v_1, v_3, u_1, u_3} C₁ E₁
F₂ : Functor.{v_2, v_4, u_2, u_4} C₂ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x x_1 : C₁ × C₂
f : x ⟶ x_1
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2

Tactic:
⟨h₁ _ hf.1, h₂ _ hf.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
E₁ : Type u_3
E₂ : Type u_4
inst_2 : Category.{v_3, u_3} E₁
inst_3 : Category.{v_4, u_4} E₂
F₁ : Functor.{v_1, v_3, u_1, u_3} C₁ E₁
F₂ : Functor.{v_2, v_4, u_2, u_4} C₂ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x x_1 : C₁ × C₂
f : x ⟶ x_1
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2

Tactic:
exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
J : Type w
C : J → Type u
D : J → Type u'
inst : (j : J) → Category.{v, u} (C j)
inst_1 : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty.{v, u} (C j)
F : (j : J) → Functor.{v, v', u, u'} (C j) (D j)
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X : (j : J) → C j
_ : ∀ ⦃Y : (j : J) → C j⦄ (f : X ⟶ Y), MorphismProperty.pi (C := C) W f → IsIso ((Functor.pi (C := C) (D := D) F).map f)
⊢ ∀ ⦃Y : (j : J) → C j⦄ (f : X ⟶ Y), MorphismProperty.pi (C := C) W f → IsIso ((Functor.pi (C := C) (D := D) F).map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
J : Type w
C : J → Type u
D : J → Type u'
inst : (j : J) → Category.{v, u} (C j)
inst_1 : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty.{v, u} (C j)
F : (j : J) → Functor.{v, v', u, u'} (C j) (D j)
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X Y : (j : J) → C j
f : X ⟶ Y
hf : MorphismProperty.pi (C := C) W f
rw : ∀ (i : J), IsIso ((Functor.pi (C := C) (D := D) F).map f i)
⊢ IsIso ((Functor.pi (C := C) (D := D) F).map f)

Tactic:
rw [isIso_pi_iff]

Premises used: CategoryTheory.isIso_pi_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
J : Type w
C : J → Type u
D : J → Type u'
inst : (j : J) → Category.{v, u} (C j)
inst_1 : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty.{v, u} (C j)
F : (j : J) → Functor.{v, v', u, u'} (C j) (D j)
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X Y : (j : J) → C j
f : X ⟶ Y
hf : MorphismProperty.pi (C := C) W f
j : J
⊢ IsIso ((Functor.pi (C := C) (D := D) F).map f j)

Tactic:
hF j _ (hf j)
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
J : Type w
C : J → Type u
D : J → Type u'
inst : (j : J) → Category.{v, u} (C j)
inst_1 : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty.{v, u} (C j)
F : (j : J) → Functor.{v, v', u, u'} (C j) (D j)
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X Y : (j : J) → C j
f : X ⟶ Y
hf : MorphismProperty.pi (C := C) W f
j : J
⊢ IsIso ((Functor.pi (C := C) (D := D) F).map f j)

Tactic:
exact hF j _ (hf j)
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₁ F₂ : FunctorsInverting.{v, u, v', u'} W D
h :
  F₁.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) =
    F₂.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
mk :
  ∀ (obj : Functor.{v, v', u, u'} C D) (property : W.IsInvertedBy obj)
    (h :
      ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
            property) =
        F₂.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)),
    ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property = F₂
⊢ F₁ = F₂

Tactic:
cases F₁
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₂ : FunctorsInverting.{v, u, v', u'} W D
obj : Functor.{v, v', u, u'} C D
property : W.IsInvertedBy obj
h :
  ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property) =
    F₂.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
mk :
  ∀ (obj_1 : Functor.{v, v', u, u'} C D) (property_1 : W.IsInvertedBy obj_1)
    (h :
      ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
            property) =
        ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1
            property_1)),
    Eq (α := FunctorsInverting.{v, u, v', u'} W D)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1
        property_1)
⊢ ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property = F₂

Tactic:
cases F₂
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
obj : Functor.{v, v', u, u'} C D
property : W.IsInvertedBy obj
obj_1 : Functor.{v, v', u, u'} C D
property_1 : W.IsInvertedBy obj_1
h :
  ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property) =
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1
        property_1)
mk :
  ∀
    (property_2 :
      W.IsInvertedBy
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
            property))),
    Eq (α := FunctorsInverting.{v, u, v', u'} W D)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
            property))
        property_2)
⊢ Eq (α := FunctorsInverting.{v, u, v', u'} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1 property_1)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
obj : Functor.{v, v', u, u'} C D
property : W.IsInvertedBy obj
property_1 :
  W.IsInvertedBy
    (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property))
⊢ Eq (α := FunctorsInverting.{v, u, v', u'} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property))
      property_1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : FunctorsInverting.{v, u, v', u'} W D
⊢ InducedCategory.Hom.hom (𝟙 F) = 𝟙 (F.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₁ F₂ F₃ : FunctorsInverting.{v, u, v', u'} W D
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₁ F₂ : FunctorsInverting.{v, u, v', u'} W D
α β : F₁ ⟶ F₂
h : α.hom.app = β.hom.app
⊢ α = β

Tactic:
ObjectProperty.hom_ext _ (NatTrans.ext h)

Premises used: CategoryTheory.NatTrans.ext, CategoryTheory.ObjectProperty.hom_ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} C D
e : F₁ ≅ F₂
⊢ (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₁.map f)) ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₂.map f)

Tactic:
simp only [NatIso.isIso_map_iff e]

Premises used: CategoryTheory.NatIso.isIso_map_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
mp : W.isoClosure.IsInvertedBy F → W.IsInvertedBy F
mpr : W.IsInvertedBy F → W.isoClosure.IsInvertedBy F
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.isoClosure.IsInvertedBy F
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)

Tactic:
h _ (W.le_isoClosure _ hf)

Premises used: CategoryTheory.MorphismProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.isoClosure.IsInvertedBy F
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)

Tactic:
exact h _ (W.le_isoClosure _ hf)

Premises used: CategoryTheory.MorphismProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
mpr : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : W f') (e : Arrow.mk f' ≅ Arrow.mk f), IsIso (F.map f)
⊢ W.isoClosure f → IsIso (F.map f)

Tactic:
⟨X', Y', f', hf', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
mpr : IsIso (F.map (Arrow.Hom.left e.inv) ≫ F.map f' ≫ F.map (Arrow.Hom.right e.hom))
⊢ IsIso (F.map f)

Tactic:
simp only [Arrow.iso_w' e, F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Arrow.iso_w'