awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
G : Type u_1
inst : Groupoid.{u_2, u_1} G
inst_1 : IsPreconnected.{u_2, u_1} G
⊢ _root_.Equivalence fun (x y : G) ↦ Nonempty.{u_2 + 1} (x ⟶ y)

Tactic:
⟨fun j => ⟨𝟙 _⟩,
     fun {j₁ j₂} => Nonempty.map fun f => inv f,
     fun {_ _ _} => Nonempty.map2 (· ≫ ·)⟩

Premises used: Nonempty.map2, CategoryTheory.CategoryStruct.id, Nonempty.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, Equivalence.mk, Nonempty.map
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
G : Type u_1
inst : Groupoid.{u_2, u_1} G
inst_1 : IsPreconnected.{u_2, u_1} G
⊢ _root_.Equivalence fun (x y : G) ↦ Nonempty.{u_2 + 1} (x ⟶ y)

Tactic:
exact
    ⟨fun j => ⟨𝟙 _⟩,
     fun {j₁ j₂} => Nonempty.map fun f => inv f,
     fun {_ _ _} => Nonempty.map2 (· ≫ ·)⟩
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type w₂
inst_2 : Category.{w₁, w₂} C
inst_3 : Subsingleton J
α : Type u₁
F : Functor.{v₁, u₁, u₁, u₁} J (Discrete α)
j x : J
⊢ F.obj x = obj.{v₁, u₁, u₁, u₁} (obj (const J) (F.obj j)) x

Tactic:
simp [Subsingleton.allEq x j]

Premises used: Subsingleton.allEq
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv = α.inv ≫ β.hom ≫ β.inv

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv ≫ β.hom ≫ β.inv = β.inv

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
this : α.inv = β.inv
⊢ α = β

Tactic:
grind [Iso]

Premises used: CategoryTheory.Iso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α.symm.hom = α.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hom : X ⟶ Y
inv : Y ⟶ X
hom_inv_id : hom ≫ inv = 𝟙 X
inv_hom_id : inv ≫ hom = 𝟙 Y
⊢ { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id : X ≅ Y }.symm =
    { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id }

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α.symm.symm = α

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
⊢ Function.Bijective.{v + 1, v + 1} (α := X ≅ Y) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm_eq, symm_symm_eq⟩

Premises used: Iff.mpr, CategoryTheory.Iso.symm_symm_eq, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α β : X ≅ Y
⊢ α.symm = β.symm ↔ α = β

Tactic:
symm_bijective.injective.eq_iff

Premises used: Function.Injective.eq_iff, Function.Bijective.injective, CategoryTheory.Iso.symm_bijective
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
⊢ Nonempty.{v + 1} (X ≅ Y) ↔ Nonempty.{v + 1} (Y ≅ X)

Tactic:
⟨fun h => ⟨h.some.symm⟩, fun h => ⟨h.some.symm⟩⟩

Premises used: Nonempty.some, Nonempty.intro, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Nonempty.{v + 1} (X ≅ X)

Tactic:
⟨default⟩

Premises used: Inhabited.default, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ≅ X) (symm (refl X)) (refl X)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
hom : X ⟶ Y
inv : Y ⟶ X
hom_inv_id : hom ≫ inv = 𝟙 X
inv_hom_id : inv ≫ hom = 𝟙 Y
hom' : Y ⟶ Z
inv' : Z ⟶ Y
hom_inv_id' : hom' ≫ inv' = 𝟙 Y
inv_hom_id' : inv' ≫ hom' = 𝟙 Z
hom_inv_id'' : (hom ≫ hom') ≫ inv' ≫ inv = 𝟙 X
inv_hom_id'' : (inv' ≫ inv) ≫ hom ≫ hom' = 𝟙 Z
⊢ { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id : X ≅ Y } ≪≫
      { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' : Y ≅ Z } =
    { hom := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ (α ≪≫ β).symm = β.symm ≪≫ α.symm

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
w : ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom

Tactic:
simp only [trans_hom, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.trans_hom
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
w : (refl X ≪≫ α).hom = α.hom
⊢ refl X ≪≫ α = α

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom

Tactic:
apply Category.id_comp

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
w : (α ≪≫ refl Y).hom = α.hom
⊢ α ≪≫ refl Y = α

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom

Tactic:
apply Category.comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α.symm ≪≫ α = refl Y

Tactic:
ext α.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α ≪≫ α.symm = refl X

Tactic:
ext α.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
rw : (α.symm ≪≫ α) ≪≫ β = β
rw₁ : refl Y ≪≫ β = β
rw₂ rw₃ : β = β
⊢ α.symm ≪≫ α ≪≫ β = β

Tactic:
rw [← trans_assoc, symm_self_id, refl_trans]

Premises used: CategoryTheory.Iso.symm_self_id, CategoryTheory.Iso.refl_trans, CategoryTheory.Iso.trans_assoc
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
rw : (α ≪≫ α.symm) ≪≫ β = β
rw₁ : refl X ≪≫ β = β
rw₂ rw₃ : β = β
⊢ α ≪≫ α.symm ≪≫ β = β

Tactic:
rw [← trans_assoc, self_symm_id, refl_trans]

Premises used: CategoryTheory.Iso.self_symm_id, CategoryTheory.Iso.refl_trans, CategoryTheory.Iso.trans_assoc
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : α.inv ≫ f = g
⊢ f = α.hom ≫ g

Tactic:
simp [H.symm]

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : f = α.hom ≫ g
⊢ α.inv ≫ f = g

Tactic:
simp [H]
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
⊢ g = α.inv ≫ f ↔ α.hom ≫ g = f

Tactic:
(inv_comp_eq α.symm).symm

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Iso.symm, Iff.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f ≫ α.inv = g
⊢ f = g ≫ α.hom

Tactic:
simp [H.symm]

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f = g ≫ α.hom
⊢ f ≫ α.inv = g

Tactic:
simp [H]
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
⊢ g = f ≫ α.inv ↔ g ≫ α.hom = f

Tactic:
(comp_inv_eq α.symm).symm

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm, Iff.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 : X ≅ Y
X_1 Y_1 : C
f g : X_1 ≅ Y_1
h : f.hom = g.hom
rw rw₁ : g.inv = g.inv
⊢ f.inv = g.inv

Tactic:
rw [ext h]

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
rw : f = α.inv ≫ 𝟙 X ↔ f = α.inv
rw₁ rw₂ : f = α.inv ↔ f = α.inv
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv

Tactic:
rw [← eq_inv_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
rw : f = 𝟙 Y ≫ α.inv ↔ f = α.inv
rw₁ rw₂ : f = α.inv ↔ f = α.inv
⊢ f ≫ α.hom = 𝟙 Y ↔ f = α.inv

Tactic:
rw [← eq_comp_inv, id_comp]

Premises used: CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
rw : β.hom = α.symm.hom ↔ β.hom = α.inv
⊢ α.hom = β.inv ↔ β.hom = α.inv

Tactic:
rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]

Premises used: CategoryTheory.Iso.symm_inv, eq_comm, CategoryTheory.Iso.symm, CategoryTheory.Iso.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
α : X ≅ Y
Z : C
⊢ Function.LeftInverse (fun (g : Z ⟶ Y) ↦ g ≫ α.inv) fun (f : Z ⟶ X) ↦ f ≫ α.hom

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
α : X ≅ Y
Z : C
⊢ Function.RightInverse (fun (g : Z ⟶ Y) ↦ g ≫ α.inv) fun (f : Z ⟶ X) ↦ f ≫ α.hom

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
out : ∃ (inv : X ⟶ Y), inv ≫ f = 𝟙 X ∧ f ≫ inv = 𝟙 Y
⊢ ∃ (inv : X ⟶ Y), f ≫ inv = 𝟙 Y ∧ inv ≫ f = 𝟙 X

Tactic:
simp_all only [and_comm]

Premises used: and_comm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : IsIso f
⊢ f ≫ inv f = 𝟙 X

Tactic:
(Classical.choose_spec I.1).left

Premises used: Classical.choose_spec, And.left, CategoryTheory.inv, CategoryTheory.IsIso.out
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : IsIso f
⊢ inv f ≫ f = 𝟙 Y

Tactic:
(Classical.choose_spec I.1).right

Premises used: Classical.choose_spec, And.right, CategoryTheory.inv, CategoryTheory.IsIso.out
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ e.hom ≫ e.inv = 𝟙 X

Tactic:
simp only [hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
⊢ IsIso e.inv

Tactic:
e.symm.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ (asIso f).hom = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ (asIso f).inv = inv f

Tactic:
rfl

Premises used: Classical.choose, CategoryTheory.inv, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : IsIso f
Z_1 : C
g h : Y ⟶ Z_1
w : f ≫ g = f ≫ h
rw : inv f ≫ f ≫ g = h
rw₁ : inv f ≫ f ≫ h = h
rw₂ rw₃ : h = h
⊢ g = h

Tactic:
rw [← IsIso.inv_hom_id_assoc f g, w, IsIso.inv_hom_id_assoc f h]

Premises used: CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ Eq.{v + 1} (α := Y ⟶ X) ((fun (x : X ⟶ X) ↦ inv f ≫ x) (f ≫ g)) ((fun (x : X ⟶ X) ↦ inv f ≫ x) (𝟙 X))

Tactic:
have := congrArg (inv f ≫ ·) hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
this : Eq.{v + 1} (α := Y ⟶ X) ((fun (x : X ⟶ X) ↦ inv f ≫ x) (f ≫ g)) ((fun (x : X ⟶ X) ↦ inv f ≫ x) (𝟙 X))
⊢ inv f = g

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ g = inv f

Tactic:
(inv_eq_of_hom_inv_id hom_inv_id).symm

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z X : C
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X) ∧ Eq.{v + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst_1 : IsIso f
⊢ IsIso (inv f)

Tactic:
(asIso f).isIso_inv

Premises used: CategoryTheory.Iso.isIso_inv, Classical.choose, CategoryTheory.inv, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso h
⊢ IsIso (f ≫ h)

Tactic:
(asIso f ≪≫ asIso h).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Iso.trans, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
h_1 : IsIso f
h_2 : IsIso h
⊢ IsIso (f ≫ h)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hom_inv_id : Eq.{v + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X)
⊢ Eq.{v + 1} (α := X ⟶ X) (inv (𝟙 X)) (𝟙 X)

Tactic:
apply inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso h
hom_inv_id : (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X
⊢ inv (f ≫ h) = inv h ≫ inv f

Tactic:
apply inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso h
⊢ (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
hom_inv_id : inv f ≫ f = 𝟙 Y
⊢ inv (inv f) = f

Tactic:
apply inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ inv f ≫ f = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ≅ Y
hom_inv_id : f.inv ≫ f.hom = 𝟙 Y
⊢ inv f.inv = f.hom

Tactic:
apply inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.inv ≫ f.hom = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ⟶ Y
inst_1 : IsIso α
f : X ⟶ Z
g : Y ⟶ Z
⊢ inv α ≫ f = g ↔ f = α ≫ g

Tactic:
(asIso α).inv_comp_eq

Premises used: CategoryTheory.Iso.inv_comp_eq, Classical.choose, CategoryTheory.inv, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ⟶ Y
inst_1 : IsIso α
f : X ⟶ Z
g : Y ⟶ Z
⊢ g = inv α ≫ f ↔ α ≫ g = f

Tactic:
(asIso α).eq_inv_comp

Premises used: Classical.choose, CategoryTheory.inv, CategoryTheory.Iso.eq_inv_comp, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso (f ≫ g)
rw : IsIso (inv f ≫ f ≫ g)
⊢ IsIso g

Tactic:
rw [← id_comp g, ← inv_hom_id f, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : IsIso f
hh : IsIso h
w : f ≫ g = h
⊢ IsIso (f ≫ g)

Tactic:
rw [← w] at hh
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : IsIso f
hh : IsIso h
w : f ≫ g = h
hh₁ : IsIso (f ≫ g)
⊢ f ≫ g = h

Tactic:
rw [← w] at hh
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g

Tactic:
of_isIso_comp_left f g

Premises used: CategoryTheory.IsIso.of_isIso_comp_left
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g

Tactic:
exact of_isIso_comp_left f g

Premises used: CategoryTheory.IsIso.of_isIso_comp_left
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
⊢ IsIso (f ≫ g) ↔ IsIso g

Tactic:
⟨fun _ ↦ IsIso.of_isIso_comp_left f g, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
p : inv f = inv g
apply : inv f ≫ f = inv f ≫ g
⊢ f = g

Tactic:
apply (cancel_epi (inv f)).1

Premises used: Iff.mp, CategoryTheory.inv, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
p : inv f = inv g
rw : 𝟙 Y = inv f ≫ g
rw₁ : 𝟙 Y = inv g ≫ g
rw₂ rw₃ : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) (𝟙 Y)
⊢ inv f ≫ f = inv f ≫ g

Tactic:
rw [inv_hom_id, p, inv_hom_id]

Premises used: CategoryTheory.IsIso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
⊢ inv f = inv g ↔ f = g

Tactic:
Iso.inv_eq_inv (asIso f) (asIso g)

Premises used: Classical.choose, CategoryTheory.inv, CategoryTheory.asIso, CategoryTheory.Iso.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : IsIso g
f : Y ⟶ X
⊢ g ≫ f = 𝟙 X ↔ f = inv g

Tactic:
(asIso g).hom_comp_eq_id

Premises used: Classical.choose, CategoryTheory.inv, CategoryTheory.Iso.hom_comp_eq_id, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : IsIso g
f : X ⟶ Y
⊢ inv g ≫ f = 𝟙 Y ↔ f = g

Tactic:
(asIso g).inv_comp_eq_id

Premises used: CategoryTheory.Iso.inv_comp_eq_id, Classical.choose, CategoryTheory.inv, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
rw : IsIso (inv g)
⊢ IsIso f

Tactic:
rw [(hom_comp_eq_id _).mp h]

Premises used: CategoryTheory.hom_comp_eq_id, Iff.mp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso (inv g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ≅ Y
g : Y ⟶ X
hom_inv_id : f.hom ≫ g = 𝟙 X
⊢ f.inv = g

Tactic:
((hom_comp_eq_id f).1 hom_inv_id).symm

Premises used: Iff.mp, Eq.symm, CategoryTheory.Iso.hom_comp_eq_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ≅ Y
g : Y ⟶ X
hom_inv_id : f.hom ≫ g = 𝟙 X
⊢ g = f.inv

Tactic:
(hom_comp_eq_id f).1 hom_inv_id

Premises used: Iff.mp, CategoryTheory.Iso.hom_comp_eq_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ≅ Y
g g' : Y ⟶ Z
⊢ f.hom ≫ g = f.hom ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f f' : X ⟶ Y
g : Y ≅ Z
⊢ f ≫ g.hom = f' ≫ g.hom ↔ f = f'

Tactic:
simp only [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
W X X' Y Z : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
h : Y ≅ Z
⊢ f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g'

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
W X X' Y Z : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
h : Z ≅ Y
⊢ f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g'

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
X Y : C
e : X ≅ Y
F : Functor.{v, v_1, u, u_1} C D
⊢ F.map e.hom ≫ F.map e.inv = 𝟙 (F.obj X)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
X Y : C
e : X ≅ Y
F : Functor.{v, v_1, u, u_1} C D
⊢ F.map e.inv ≫ F.map e.hom = 𝟙 (F.obj Y)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
i : X ≅ Y
⊢ F.mapIso i.symm = (F.mapIso i).symm

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
w : (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom

Tactic:
apply Functor.map_comp

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X : C
⊢ F.mapIso (Iso.refl X) = Iso.refl (F.obj X)

Tactic:
Iso.ext <| F.map_id X

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
inst_2 : IsIso f
⊢ IsIso (F.map f)

Tactic:
(F.mapIso (asIso f)).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
hom_inv_id : F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
⊢ F.map (inv f) = inv (F.map f)

Tactic:
apply eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp