awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f

Tactic:
exact ⟨_, _, _, _, _, hf⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W₁ f
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W₁.transfiniteCompositionsOfShape J f

Tactic:
rw [transfiniteCompositions_iff] at hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W₁.transfiniteCompositionsOfShape J f
obtain :
  ∀ (J : Type w) (w : LinearOrder J) (w_1 : SuccOrder J) (w_2 : OrderBot J) (w_3 : WellFoundedLT J)
    (hf : W₁.transfiniteCompositionsOfShape J f), transfiniteCompositions.{w, v, u} W₂ f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
obtain ⟨J, _, _, _, _, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
w : LinearOrder J
w_1 : SuccOrder J
w_2 : OrderBot J
w_3 : WellFoundedLT J
hf : W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
transfiniteCompositionsOfShape_le_transfiniteCompositions _ _ _
    (transfiniteCompositionsOfShape_monotone J h _ hf)

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
w : LinearOrder J
w_1 : SuccOrder J
w_2 : OrderBot J
w_3 : WellFoundedLT J
hf : W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
exact transfiniteCompositionsOfShape_le_transfiniteCompositions _ _ _
    (transfiniteCompositionsOfShape_monotone J h _ hf)

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ W ≤ transfiniteCompositions.{w, v, u} W

Tactic:
le_trans (fun _ _ _ hf ↦
    (MorphismProperty.TransfiniteCompositionOfShape.ofOrderIso (.ofMem _ hf)
      (orderIsoShrink.{w} (Fin 2)).symm).mem)
    (transfiniteCompositionsOfShape_le_transfiniteCompositions _ _)

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofMem, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofOrderIso, OrderIso.symm, orderIsoShrink, OfNat.ofNat, Fin, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W f → W f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W f → W f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W f
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f

Tactic:
rw [transfiniteCompositions_iff] at hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
hf :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f
obtain :
  ∀ (J : Type w) (w : LinearOrder J) (w_1 : SuccOrder J) (w_2 : OrderBot J) (w_3 : WellFoundedLT J)
    (hf : W.transfiniteCompositionsOfShape J f), W f
⊢ W f

Tactic:
obtain ⟨J, _, _, _, _, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
J : Type w
w : LinearOrder J
w_1 : SuccOrder J
w_2 : OrderBot J
w_3 : WellFoundedLT J
hf : W.transfiniteCompositionsOfShape J f
⊢ W f

Tactic:
W.transfiniteCompositionsOfShape_le J _ hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
J : Type w
w : LinearOrder J
w_1 : SuccOrder J
w_2 : OrderBot J
w_3 : WellFoundedLT J
hf : W.transfiniteCompositionsOfShape J f
⊢ W f

Tactic:
exact W.transfiniteCompositionsOfShape_le J _ hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
mp : transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q
mpr : P ≤ Q → transfiniteCompositions.{w, v, u} P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
(le_transfiniteCompositions P).trans

Premises used: LE.le.trans, CategoryTheory.MorphismProperty.le_transfiniteCompositions
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
exact (le_transfiniteCompositions P).trans

Premises used: LE.le.trans, CategoryTheory.MorphismProperty.le_transfiniteCompositions
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
h : P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q

Tactic:
(transfiniteCompositions_monotone.{w} h).trans Q.transfiniteCompositions_le

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_le, LE.le.trans, CategoryTheory.MorphismProperty.transfiniteCompositions_monotone
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
h : P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q

Tactic:
exact (transfiniteCompositions_monotone.{w} h).trans Q.transfiniteCompositions_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
inst_5 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
i j : J
φ : i ⟶ j
⊢ W (h.toTransfiniteCompositionOfShape (W := W).F.map φ)

Tactic:
W.transfiniteCompositionsOfShape_le _ _ ((h.iic j).ici ⟨i, leOfHom φ⟩).mem

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, Subtype.mk, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ici, CategoryTheory.leOfHom, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.iic
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
inst_5 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
⊢ W (h.toTransfiniteCompositionOfShape (W := W).incl.app j)

Tactic:
W.transfiniteCompositionsOfShape_le _ _ (h.ici j).mem

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ici
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
⊢ IsStableUnderTransfiniteCompositionOfShape.{w, v, u} (isomorphisms C) J

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : TransfiniteCompositionOfShape (isomorphisms C) J f
⊢ IsIso f

Tactic:
(isomorphisms C).transfiniteCompositionsOfShape_le _ _ h.mem

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, CategoryTheory.MorphismProperty.isomorphisms
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
X Y : C
f_1 : X ⟶ Y
h : TransfiniteCompositionOfShape (isomorphisms C) J f_1
i j : J
f : i ⟶ j
⊢ IsIso (h.toTransfiniteCompositionOfShape (W := isomorphisms C).F.map f)

Tactic:
h.mem_map f

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_map
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : TransfiniteCompositionOfShape (isomorphisms C) J f
j : J
⊢ IsIso (h.toTransfiniteCompositionOfShape (W := isomorphisms C).incl.app j)

Tactic:
h.mem_incl_app j

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_incl_app
-- Module: Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
inst_1 : W₁.IsWeakFactorizationSystem W₂
⊢ W₁.rlp = W₂

Tactic:
IsWeakFactorizationSystem.rlp

Premises used: CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
inst_1 : W₁.IsWeakFactorizationSystem W₂
⊢ W₂.llp = W₁

Tactic:
IsWeakFactorizationSystem.llp

Premises used: CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.llp
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
X : C
⊢ α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
X : C
⊢ α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
e : F ≅ G
X₁ : C
X₂ : D
⊢ (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 ((F.obj X₁).obj X₂)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
e : F ≅ G
X₁ : C
X₂ : D
⊢ (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 ((G.obj X₁).obj X₂)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ Functor.{v₃, v₄, u₃, u₄} E E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 (((F.obj X₁).obj X₂).obj X₃)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ Functor.{v₃, v₄, u₃, u₄} E E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 (((G.obj X₁).obj X₂).obj X₃)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
β : G ≅ H
X : C
⊢ (α ≪≫ β).app X = α.app X ≪≫ β.app X

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
X : C
⊢ α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
X : C
⊢ α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
X : C
Y : D
g g' : G.obj X ⟶ Y
⊢ α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi, refl]

Premises used: CategoryTheory.cancel_epi, refl
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
X : C
Y : D
g g' : F.obj X ⟶ Y
⊢ α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi, refl]

Premises used: CategoryTheory.cancel_epi, refl
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
W X X' : D
Y : C
f : W ⟶ X
g : X ⟶ F.obj Y
f' : W ⟶ X'
g' : X' ⟶ F.obj Y
⊢ f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono, refl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, refl
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
W X X' : D
Y : C
f : W ⟶ X
g : X ⟶ G.obj Y
f' : W ⟶ X'
g' : X' ⟶ G.obj Y
⊢ f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono, refl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, refl
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
X : C
⊢ inv (e.inv.app X) = e.hom.app X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
α : F ⟶ G
f : X ⟶ Y
h : IsIso (α.app X)
⊢ inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
α : F ⟶ G
f : X ⟶ Y
h : IsIso (α.app Y)
⊢ α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : C
α : F ⟶ G
inst_4 : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : C
α : F ⟶ G
inst_4 : IsIso α
X : C
⊢ (inv α).app X ≫ α.app X = 𝟙 (G.obj X)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : IsIso α
X : C
⊢ (inv α).app X = inv (α.app X)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
X Y : C
e : X ≅ Y
Z : D
⊢ inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := G.obj X ⟶ F.obj Y)
    ((fun (f : F.obj X ⟶ G.obj Y) ↦ (app X).inv ≫ f ≫ (app Y).inv) ((app X).hom ≫ G.map f))
    ((fun (f : F.obj X ⟶ G.obj Y) ↦ (app X).inv ≫ f ≫ (app Y).inv) (F.map f ≫ (app Y).hom))

Tactic:
have h := congr_arg (fun f => (app X).inv ≫ f ≫ (app Y).inv) (naturality f).symm
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
h :
  Eq.{v₂ + 1} (α := G.obj X ⟶ F.obj Y)
    ((fun (f : F.obj X ⟶ G.obj Y) ↦ (app X).inv ≫ f ≫ (app Y).inv) ((app X).hom ≫ G.map f))
    ((fun (f : F.obj X ⟶ G.obj Y) ↦ (app X).inv ≫ f ≫ (app Y).inv) (F.map f ≫ (app Y).hom))
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f

Tactic:
simp only [Iso.inv_hom_id_assoc, Iso.hom_inv_id, assoc, comp_id] at h

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
h : G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f

Tactic:
h
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
h : G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
app' : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f
X : C
w w₁ w₂ w₃ : ((ofComponents app' @naturality).app X).hom = (app' X).hom
⊢ (ofComponents app' @naturality).app X = app' X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : ∀ (X : C), IsIso (α.app X)
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    F.map f ≫ Iso.hom ((fun (X : C) ↦ asIso (α.app X)) Y) = Iso.hom ((fun (X : C) ↦ asIso (α.app X)) X) ≫ G.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
revert : ∀ {F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D} (e : F₁ ≅ F₂), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
revert F₁ F₂
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
suffices : ∀ {F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D} (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.map f)
⊢ ∀ {F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D} (e : F₁ ≅ F₂), IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from
    fun F₁ F₂ e => ⟨this e, this e.symm⟩
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X) ∧
    (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)

Tactic:
exact IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, by cat_disch⟩

Premises used: CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.IsIso.mk, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app