awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
D : Set C
c d e : C
p : c ⟶ d
left : c ∈ D
right : d ∈ D
q : d ⟶ e
left_1 : d ∈ D
right_1 : e ∈ D
⊢ e ∈ D

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D : Set C
⊢ objs.{u, u_1} (full D) = D

Tactic:
Set.ext fun _ => ⟨fun ⟨_, h, _⟩ => h, fun h => ⟨𝟙 _, h, h⟩⟩

Premises used: Set.ext, Membership.mem, CategoryTheory.CategoryStruct.id, And.intro, _private.0.CategoryTheory.Subgroupoid.full_objs.match_1, Iff.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D : Set C
c d : C
f : c ⟶ d
⊢ Membership.mem (γ := Set (c ⟶ d)) (arrows (full D) c d) f ↔ c ∈ D ∧ d ∈ D

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D : Set C
c : C
rw rw₁ : c ∈ D ↔ c ∈ D
⊢ c ∈ objs.{u, u_1} (full D) ↔ c ∈ D

Tactic:
rw [full_objs]

Premises used: CategoryTheory.Subgroupoid.full_objs
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
arrows :
  ∀ (x x_1 : C) (x_2 : x ⟶ x_1),
    Membership.mem (γ := Set (x ⟶ x_1)) (Subgroupoid.arrows (full ∅) x x_1) x_2 ↔
      Membership.mem (γ := Set (x ⟶ x_1)) (Subgroupoid.arrows ⊥ x x_1) x_2
⊢ Eq (α := Subgroupoid.{u, u_1} C) (full ∅) ⊥

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
x x_1 : C
x_2 : x ⟶ x_1
⊢ Membership.mem (γ := Set (x ⟶ x_1)) (arrows (full ∅) x x_1) x_2 ↔
    Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊥ x x_1) x_2

Tactic:
simp only [Bot.bot, mem_full_iff, mem_empty_iff_false, and_self_iff]

Premises used: Bot.bot, CategoryTheory.Subgroupoid.mem_full_iff, Set.mem_empty_iff_false, and_self_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
arrows :
  ∀ (x x_1 : C) (x_2 : x ⟶ x_1),
    Membership.mem (γ := Set (x ⟶ x_1)) (Subgroupoid.arrows (full univ) x x_1) x_2 ↔
      Membership.mem (γ := Set (x ⟶ x_1)) (Subgroupoid.arrows ⊤ x x_1) x_2
⊢ Eq (α := Subgroupoid.{u, u_1} C) (full univ) ⊤

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
x x_1 : C
x_2 : x ⟶ x_1
⊢ Membership.mem (γ := Set (x ⟶ x_1)) (arrows (full univ) x x_1) x_2 ↔
    Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊤ x x_1) x_2

Tactic:
simp only [mem_full_iff, mem_univ, and_self, mem_top]

Premises used: and_self, Set.mem_univ, CategoryTheory.Subgroupoid.mem_full_iff, CategoryTheory.Subgroupoid.mem_top
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D E : Set C
h : D ≤ E
rw : ∀ {c d : C}, Subset.{u_1} (α := Set (c ⟶ d)) (arrows (full D) c d) (arrows (full E) c d)
⊢ LE.le (α := Subgroupoid.{u, u_1} C) (full D) (full E)

Tactic:
rw [le_iff]

Premises used: CategoryTheory.Subgroupoid.le_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D E : Set C
h : D ≤ E
c d : C
f : c ⟶ d
⊢ c ∈ D ∧ d ∈ D → c ∈ E ∧ d ∈ E

Tactic:
fun ⟨hc, hd⟩ => ⟨h hc, h hd⟩

Premises used: Membership.mem, _private.0.CategoryTheory.Subgroupoid.full_mono.match_1, And, And.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D E : Set C
h : D ≤ E
c d : C
f : c ⟶ d
⊢ c ∈ D ∧ d ∈ D → c ∈ E ∧ d ∈ E

Tactic:
exact fun ⟨hc, hd⟩ => ⟨h hc, h hd⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D : Set C
c d : (↑(objs.{u, u_1} (full D)) : Type u)
f g : c ⟶ d
⊢ f = g ↔ (↑f : (↑c : C) ⟶ (↑d : C)) = (↑g : (↑c : C) ⟶ (↑d : C))

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.CategoryTheory.Groupoid.VertexGroup
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c : C
γ : c ⟶ c
⊢ γ⁻¹ = CategoryTheory.inv γ

Tactic:
Groupoid.inv_eq_inv γ

Premises used: CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.VertexGroup
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
simp_rw simp_rw₁ : f ≫ (inv f ≫ γ ≫ f) ≫ inv f = γ
simp_rw₂ : f ≫ inv f ≫ γ ≫ f ≫ inv f = γ
simp_rw₃ : f ≫ inv f ≫ γ ≫ 𝟙 c = γ
simp_rw₄ : f ≫ inv f ≫ γ = γ
simp_rw₅ : (f ≫ inv f) ≫ γ = γ
simp_rw₆ : 𝟙 c ≫ γ = γ
⊢ (fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) ((fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) γ) = γ

Tactic:
simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
      Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Groupoid.comp_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Groupoid.VertexGroup
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
δ : d ⟶ d
simp_rw simp_rw₁ : inv f ≫ (f ≫ δ ≫ inv f) ≫ f = δ
simp_rw₂ : inv f ≫ f ≫ δ ≫ inv f ≫ f = δ
simp_rw₃ : inv f ≫ f ≫ δ ≫ 𝟙 d = δ
simp_rw₄ : ((inv f ≫ f) ≫ δ) ≫ 𝟙 d = δ
simp_rw₅ : (𝟙 d ≫ δ) ≫ 𝟙 d = δ
simp_rw₆ : δ ≫ 𝟙 d = δ
⊢ (fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) ((fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) δ) = δ

Tactic:
simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Groupoid.inv_comp, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Groupoid.VertexGroup
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ₁ γ₂ : c ⟶ c
⊢ inv f ≫ (γ₁ * γ₂) ≫ f = inv f ≫ γ₁ ≫ f * inv f ≫ γ₂ ≫ f

Tactic:
simp only [vertexGroup_mul, inv_eq_inv, Category.assoc, IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Groupoid.inv_eq_inv, CategoryTheory.Groupoid.vertexGroup_mul
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
f : X ⟶ Y
⊢ IsIso f

Tactic:
⟨⟨Groupoid.inv f, Groupoid.comp_inv f, Groupoid.inv_comp f⟩⟩

Premises used: CategoryTheory.Groupoid.inv, CategoryTheory.Groupoid.inv_comp, And.intro, Exists.intro, CategoryTheory.IsIso.mk, CategoryTheory.Groupoid.comp_inv
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
f : X ⟶ Y
⊢ inv f = CategoryTheory.inv f

Tactic:
IsIso.eq_inv_of_hom_inv_id <| Groupoid.comp_inv f

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id, CategoryTheory.Groupoid.comp_inv
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
f : X ⟶ Y
⊢ inv (inv f) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
f : Y ⟶ X
⊢ inv (inv f) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y a b : C
f : a ⟶ b
dsimp : Groupoid.inv (Groupoid.inv f) = f
⊢ Quiver.reverse (Quiver.reverse f) = f

Tactic:
dsimp [Quiver.reverse]

Premises used: Quiver.reverse
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y a b : C
f : a ⟶ b
⊢ Groupoid.inv (Groupoid.inv f) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Quiver.reverse f = inv f

Tactic:
rfl

Premises used: Quiver.reverse, rfl
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
u v : C
f : u ⟶ v
⊢ F.toPrefunctor.map (Quiver.reverse f) = Quiver.reverse (F.toPrefunctor.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
𝒞 : Category.{u_2, u_1} C
D : Type u
inst : Groupoid.{v, u} D
F : Functor.{u_2, v, u_1, u} C D
h : F.FullyFaithful
X Y : C
f : X ⟶ Y
apply : F.map (h.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)
⊢ h.preimage (inv (F.map f)) ≫ f = 𝟙 Y

Tactic:
apply h.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
𝒞 : Category.{u_2, u_1} C
D : Type u
inst : Groupoid.{v, u} D
F : Functor.{u_2, v, u_1, u} C D
h : F.FullyFaithful
X Y : C
f : X ⟶ Y
⊢ F.map (h.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
𝒞 : Category.{u_2, u_1} C
D : Type u
inst : Groupoid.{v, u} D
F : Functor.{u_2, v, u_1, u} C D
h : F.FullyFaithful
X Y : C
f : X ⟶ Y
apply : F.map (f ≫ h.preimage (inv (F.map f))) = F.map (𝟙 X)
⊢ f ≫ h.preimage (inv (F.map f)) = 𝟙 X

Tactic:
apply h.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
𝒞 : Category.{u_2, u_1} C
D : Type u
inst : Groupoid.{v, u} D
F : Functor.{u_2, v, u_1, u} C D
h : F.FullyFaithful
X Y : C
f : X ⟶ Y
⊢ F.map (f ≫ h.preimage (inv (F.map f))) = F.map (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u
D : Type u₂
inst : Category.{v, u₂} D
inst_1 : IsGroupoid.{v, u₂} D
F : C → D
⊢ IsGroupoid.{v, u} (InducedCategory D F)

Tactic:
isGroupoid_of_reflects_iso (inducedFunctor F)

Premises used: CategoryTheory.inducedFunctor, CategoryTheory.isGroupoid_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
I : Type u
J : I → Type u₂
inst : (i : I) → Groupoid.{v, u₂} (J i)
X Y : (i : I) → J i
f : X ⟶ Y
h : ∀ (i : I), Eq.{v + 1} (((fun (i : I) ↦ Groupoid.inv (f i)) ≫ f) i) (𝟙 Y i)
⊢ (fun (i : I) ↦ Groupoid.inv (f i)) ≫ f = 𝟙 Y

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
I : Type u
J : I → Type u₂
inst : (i : I) → Groupoid.{v, u₂} (J i)
X Y : (i : I) → J i
f : X ⟶ Y
i : I
⊢ Eq.{v + 1} (((fun (i : I) ↦ Groupoid.inv (f i)) ≫ f) i) (𝟙 Y i)

Tactic:
apply Groupoid.inv_comp

Premises used: CategoryTheory.Groupoid.inv_comp
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
I : Type u
J : I → Type u₂
inst : (i : I) → Groupoid.{v, u₂} (J i)
X Y : (i : I) → J i
f : X ⟶ Y
h : ∀ (i : I), Eq.{v + 1} ((f ≫ fun (i : I) ↦ Groupoid.inv (f i)) i) (𝟙 X i)
⊢ (f ≫ fun (i : I) ↦ Groupoid.inv (f i)) = 𝟙 X

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
I : Type u
J : I → Type u₂
inst : (i : I) → Groupoid.{v, u₂} (J i)
X Y : (i : I) → J i
f : X ⟶ Y
i : I
⊢ Eq.{v + 1} ((f ≫ fun (i : I) ↦ Groupoid.inv (f i)) i) (𝟙 X i)

Tactic:
apply Groupoid.comp_inv

Premises used: CategoryTheory.Groupoid.comp_inv
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
mp : IsGroupoid.{v_1, u_1} C → Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
mpr : Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤ → IsGroupoid.{v_1, u_1} C
⊢ IsGroupoid.{v_1, u_1} C ↔ Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
mp : IsGroupoid.{v_1, u_1} C → LE.le (α := MorphismProperty.{v_1, u_1} C) ⊤ (isomorphisms C)
⊢ IsGroupoid.{v_1, u_1} C → Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsGroupoid.{v_1, u_1} C
mp : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), ⊤ f → isomorphisms C f
⊢ LE.le (α := MorphismProperty.{v_1, u_1} C) ⊤ (isomorphisms C)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsGroupoid.{v_1, u_1} C
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), True → IsIso f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
⊢ IsGroupoid.{v_1, u_1} C

Tactic:
⟨of_eq_top h⟩

Premises used: CategoryTheory.MorphismProperty.of_eq_top, CategoryTheory.IsGroupoid.mk
-- Module: Mathlib.CategoryTheory.Groupoid
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
⊢ IsGroupoid.{v_1, u_1} C

Tactic:
exact ⟨of_eq_top h⟩
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
a : X₂ ⟶ T.obj X₁
b : L.obj X₁ ⟶ X₃
comm : R.map a ≫ w.app X₁ ≫ B.map b = g
⊢ ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom

Tactic:
simpa using comm
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.StructuredArrowRightwards g
obtain :
  ∀ (g_1 : CostructuredArrow L X₃) (φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj g_1),
    ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g),
      StructuredArrow.mk φ = mk w g X₁ a b comm
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Tactic:
obtain ⟨g, φ, rfl⟩ := StructuredArrow.mk_surjective f

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g_1 : R.obj X₂ ⟶ B.obj X₃
g : CostructuredArrow L X₃
φ : CostructuredArrow.mk g_1 ⟶ (w.costructuredArrowRightwards X₃).obj g
obtain :
  ∀ (X₁ : C₁) (b : L.obj X₁ ⟶ X₃)
    (φ : CostructuredArrow.mk g_1 ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)),
    ∃ (X₁_1 : C₁) (a : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g_1),
      StructuredArrow.mk φ = mk w g_1 X₁_1 a b_1 comm
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g_1),
    StructuredArrow.mk φ = mk w g_1 X₁ a b comm

Tactic:
obtain ⟨X₁, b, rfl⟩ := g.mk_surjective

Premises used: CategoryTheory.CostructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)
obtain :
  ∀ (a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left)
    (ha :
      R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom),
    ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
      StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm
⊢ ∃ (X₁_1 : C₁) (a : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g),
    StructuredArrow.mk φ = mk w g X₁_1 a b_1 comm

Tactic:
obtain ⟨a, ha, rfl⟩ := CostructuredArrow.homMk_surjective φ

Premises used: rfl, CategoryTheory.CostructuredArrow.homMk_surjective
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left
ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom
⊢ R.map a ≫ w.app X₁ ≫ B.map b = g

Tactic:
simpa using ha
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left
ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom
⊢ ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
    StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm

Tactic:
exact ⟨X₁, a, b, by simpa using ha, rfl⟩
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.CostructuredArrowDownwards g
obtain :
  ∀ (g_1 : StructuredArrow X₂ T) (φ : (w.structuredArrowDownwards X₂).obj g_1 ⟶ StructuredArrow.mk g),
    ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g),
      CostructuredArrow.mk φ = mk w g X₁ a b comm
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Tactic:
obtain ⟨g, φ, rfl⟩ := CostructuredArrow.mk_surjective f

Premises used: CategoryTheory.CostructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g_1 : R.obj X₂ ⟶ B.obj X₃
g : StructuredArrow X₂ T
φ : (w.structuredArrowDownwards X₂).obj g ⟶ StructuredArrow.mk g_1
obtain :
  ∀ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁)
    (φ : (w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a) ⟶ StructuredArrow.mk g_1),
    ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b = g_1),
      CostructuredArrow.mk φ = mk w g_1 X₁_1 a_1 b comm
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g_1),
    CostructuredArrow.mk φ = mk w g_1 X₁ a b comm

Tactic:
obtain ⟨X₁, a, rfl⟩ := g.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
a : X₂ ⟶ T.obj X₁
φ : (w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a) ⟶ StructuredArrow.mk g
obtain :
  ∀ (b : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).right ⟶ (StructuredArrow.mk g).right)
    (hb : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom),
    ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
      CostructuredArrow.mk (StructuredArrow.homMk b hb) = mk w g X₁_1 a_1 b_1 comm
⊢ ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b = g),
    CostructuredArrow.mk φ = mk w g X₁_1 a_1 b comm

Tactic:
obtain ⟨b, hb, rfl⟩ := StructuredArrow.homMk_surjective φ

Premises used: rfl, CategoryTheory.StructuredArrow.homMk_surjective
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
a : X₂ ⟶ T.obj X₁
b : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).right ⟶ (StructuredArrow.mk g).right
hb : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom
⊢ R.map a ≫ w.app X₁ ≫ B.map b = g

Tactic:
simpa using hb
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
a : X₂ ⟶ T.obj X₁
b : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).right ⟶ (StructuredArrow.mk g).right
hb : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom
⊢ ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
    CostructuredArrow.mk (StructuredArrow.homMk b hb) = mk w g X₁_1 a_1 b_1 comm

Tactic:
exact ⟨X₁, a, b, by simpa using hb, rfl⟩
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.StructuredArrowRightwards g
⊢ ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk (StructuredArrow.hom f).left)).hom ≫
      B.map (StructuredArrow.right f).hom =
    (StructuredArrow.mk g).hom

Tactic:
simpa using CostructuredArrow.w f.hom

Premises used: CategoryTheory.StructuredArrow.hom, CategoryTheory.CostructuredArrow.w