awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.Small.{w, v, u} P
hP : P.IsStrongGenerator
X : C
this : HasCoproductsOfShape (CostructuredArrow P.ι X) C
have :
  ∀
    (this :
      IsColimit.{w, v, w, u} (J := Discrete (Shrink.{w, max u v} (CostructuredArrow P.ι X))) (F :=
        Equivalence.functor (Equivalence.symm (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X)))) ⋙
          Discrete.functor (P.coproductFromFamily X))
        (Cocone.whisker
          (Equivalence.functor (Equivalence.symm (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X)))))
          (Cofan.mk (∐ P.coproductFromFamily X) (Sigma.ι (P.coproductFromFamily X))))),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
    ExtremalEpi p

Tactic:
have := (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.Small.{w, v, u} P
hP : P.IsStrongGenerator
X : C
this_1 : HasCoproductsOfShape (CostructuredArrow P.ι X) C
this :
  IsColimit.{w, v, w, u} (J := Discrete (Shrink.{w, max u v} (CostructuredArrow P.ι X))) (F :=
    Equivalence.functor (Equivalence.symm (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X)))) ⋙
      Discrete.functor (P.coproductFromFamily X))
    (Cocone.whisker
      (Equivalence.functor (Equivalence.symm (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X)))))
      (Cofan.mk (∐ P.coproductFromFamily X) (Sigma.ι (P.coproductFromFamily X))))
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
    ExtremalEpi p

Tactic:
⟨_, fun j ↦ ((equivShrink.{w} (CostructuredArrow P.ι X)).symm j).left.1,
    fun j ↦ ((equivShrink.{w} _).symm j).1.2, _,
    (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm, _, hP.extremalEpi_coproductFrom X⟩

Premises used: CategoryTheory.Limits.IsColimit.whiskerEquivalence, CategoryTheory.ObjectProperty.ι, CategoryTheory.Comma.left, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.CostructuredArrow, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Discrete.equivalence, CategoryTheory.ObjectProperty.IsStrongGenerator.extremalEpi_coproductFrom, CategoryTheory.ObjectProperty.coproductFromFamily, Exists.intro, Equiv.symm, equivShrink, CategoryTheory.CostructuredArrow.left, DFunLike.coe, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.Small.{w, v, u} P
hP : P.IsStrongGenerator
X : C
this_1 : HasCoproductsOfShape (CostructuredArrow P.ι X) C
this :
  IsColimit.{w, v, w, u} (J := Discrete (Shrink.{w, max u v} (CostructuredArrow P.ι X))) (F :=
    Equivalence.functor (Equivalence.symm (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X)))) ⋙
      Discrete.functor (P.coproductFromFamily X))
    (Cocone.whisker
      (Equivalence.functor (Equivalence.symm (Discrete.equivalence (equivShrink (CostructuredArrow P.ι X)))))
      (Cofan.mk (∐ P.coproductFromFamily X) (Sigma.ι (P.coproductFromFamily X))))
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
    ExtremalEpi p

Tactic:
refine ⟨_, fun j ↦ ((equivShrink.{w} (CostructuredArrow P.ι X)).symm j).left.1,
    fun j ↦ ((equivShrink.{w} _).symm j).1.2, _,
    (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm, _, hP.extremalEpi_coproductFrom X⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
rw :
  P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
⊢ P.IsStrongGenerator

Tactic:
rw [isStrongGenerator_iff]

Premises used: CategoryTheory.ObjectProperty.isStrongGenerator_iff
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
⊢ P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
⟨IsSeparating.mk_of_exists_colimitsOfShape hP, fun X Y i _ hi ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_colimitsOfShape, And.intro
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
refine :
  ∀ (X Y : C) (i : X ⟶ Y),
    Mono i → ∀ (hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i), IsIso i
⊢ P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
refine ⟨IsSeparating.mk_of_exists_colimitsOfShape hP, fun X Y i _ hi ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
this : IsSplitEpi i
obtain : ∀ (r : Y ⟶ X) (fac : r ≫ i = 𝟙 Y), IsIso i
⊢ IsIso i

Tactic:
obtain ⟨r, fac⟩ := this
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
r : Y ⟶ X
fac : r ≫ i = 𝟙 Y
⊢ i ≫ r = 𝟙 X ∧ r ≫ i = 𝟙 Y

Tactic:
simp [← cancel_mono i, fac]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
r : Y ⟶ X
fac : r ≫ i = 𝟙 Y
⊢ IsIso i

Tactic:
exact ⟨r, by simp [← cancel_mono i, fac]⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
suffices : IsSplitEpi i
⊢ IsIso i

Tactic:
suffices IsSplitEpi i by
    obtain ⟨r, fac⟩ := this
    exact ⟨r, by simp [← cancel_mono i, fac]⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
obtain : ∀ (J : Type w) (w : Category.{w', w} J) (p : ColimitOfShape.{w', w, v, u} P J Y), IsSplitEpi i
⊢ IsSplitEpi i

Tactic:
obtain ⟨J, _, ⟨p⟩⟩ := hP Y
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v, u} P J Y
choose :
  ∀ (φ : (j : J) → p.toColimitPresentation (P := P).diag.obj j ⟶ X)
    (hφ :
      ∀ (j : J),
        (fun (f : p.toColimitPresentation (P := P).diag.obj j ⟶ X) ↦ f ≫ i) (φ j) =
          p.toColimitPresentation (P := P).ι.app j),
    IsSplitEpi i
⊢ IsSplitEpi i

Tactic:
choose φ hφ using fun j ↦ hi _ (p.prop_diag_obj j) (p.ι.app j)

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v, u} P J Y
φ : (j : J) → p.toColimitPresentation (P := P).diag.obj j ⟶ X
hφ :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := P).diag.obj j ⟶ X) ↦ f ≫ i) (φ j) = p.toColimitPresentation (P := P).ι.app j
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ p.toColimitPresentation (P := P).diag.map f ≫ φ j₂ = φ j₁ ≫ Functor.map (Functor.obj (Functor.const J) X) f

Tactic:
simp [← cancel_mono i, hφ]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v, u} P J Y
φ : (j : J) → p.toColimitPresentation (P := P).diag.obj j ⟶ X
hφ :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := P).diag.obj j ⟶ X) ↦ f ≫ i) (φ j) = p.toColimitPresentation (P := P).ι.app j
c : Cocone p.toColimitPresentation (P := P).diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
⊢ IsSplitEpi i

Tactic:
⟨p.isColimit.desc c, p.isColimit.hom_ext (fun j ↦ ?_)⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.hom_ext, Nonempty.intro, CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.IsSplitEpi.mk, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v, u} P J Y
φ : (j : J) → p.toColimitPresentation (P := P).diag.obj j ⟶ X
hφ :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := P).diag.obj j ⟶ X) ↦ f ≫ i) (φ j) = p.toColimitPresentation (P := P).ι.app j
c : Cocone p.toColimitPresentation (P := P).diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
refine :
  ∀ (j : J),
    { pt := Y, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j ≫
        p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
      { pt := Y, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j ≫ 𝟙 Y
⊢ IsSplitEpi i

Tactic:
refine ⟨p.isColimit.desc c, p.isColimit.hom_ext (fun j ↦ ?_)⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v, u} P J Y
φ : (j : J) → p.toColimitPresentation (P := P).diag.obj j ⟶ X
hφ :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := P).diag.obj j ⟶ X) ↦ f ≫ i) (φ j) = p.toColimitPresentation (P := P).ι.app j
c : Cocone p.toColimitPresentation (P := P).diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
dsimp :
  p.toColimitPresentation (P := P).ι.app j ≫ p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
    p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
⊢ { pt := Y, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j ≫
      p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
    { pt := Y, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j ≫ 𝟙 Y

Tactic:
dsimp at hφ ⊢
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v, u} P J X
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v, u} P J Y
φ : (j : J) → p.toColimitPresentation (P := P).diag.obj j ⟶ X
hφ : ∀ (j : J), φ j ≫ i = p.toColimitPresentation (P := P).ι.app j
c : Cocone p.toColimitPresentation (P := P).diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
rw : c.ι.app j ≫ i = p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
rw₁ : p.toColimitPresentation (P := P).ι.app j = p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
rw₂ rw₃ : p.toColimitPresentation (P := P).ι.app j = p.toColimitPresentation (P := P).ι.app j
⊢ p.toColimitPresentation (P := P).ι.app j ≫ p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
    p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y

Tactic:
rw [p.isColimit.fac_assoc, hφ, Category.comp_id]

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Category.comp_id, CategoryTheory.Limits.IsColimit.fac_assoc, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Generator.Type
Goal:
X Y : Type u
f g : X ⟶ Y
h : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
h₁ :
  ∀ (x : X), (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun x
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Generator.Type
Goal:
X Y : Type u
f g : X ⟶ Y
h : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
x : X
⊢ ObjectProperty.singleton PUnit.{u + 1} PUnit.{u + 1}

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Type
Goal:
X Y : Type u
f g : X ⟶ Y
h : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
x : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun x

Tactic:
exact ConcreteCategory.congr_hom (h PUnit (by simp) (↾fun _ ↦ x))
    .unit

Premises used: TypeCat.ofHom, PUnit, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i

Tactic:
have eq₁ := D.t_fac i i j
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i
⊢ Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))

Tactic:
have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i
eq₂ :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))
⊢ D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)

Tactic:
rw [D.t_id, Category.comp_id, eq₂] at eq₁

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.GlueData.t_id
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i
eq₂ :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))
eq₃ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
⊢ Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))

Tactic:
rw [D.t_id, Category.comp_id, eq₂] at eq₁

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.GlueData.t_id
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))
⊢ (D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i)) ≫ D.f i i = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j

Tactic:
have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))
eq₃ : (D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i)) ≫ D.f i i = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ (D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i)) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j

Tactic:
rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))
eq₃ : (D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i)) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ D.t' i i j = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))

Tactic:
Mono.right_cancellation _ _
      ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)

Premises used: CategoryTheory.Mono.right_cancellation, Eq.symm, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst, Eq.trans
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ D.V (i, i)) (pullback.fst (D.f i i) (D.f i j))
    ((pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i))
eq₃ : (D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i)) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ D.t' i i j = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))

Tactic:
exact
    Mono.right_cancellation _ _
      ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)

Premises used: CategoryTheory.Mono.right_cancellation, Eq.symm, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst, Eq.trans
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
rw : D.t' j i i = (D.t' j i i ≫ pullback.snd (D.f i i) (D.f i j)) ≫ inv (pullback.snd (D.f i i) (D.f i j))
⊢ D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
rw [← Category.assoc, ← D.t_fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GlueData.t_fac
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.t' j i i = (D.t' j i i ≫ pullback.snd (D.f i i) (D.f i j)) ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
rw : D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (pullback.snd (D.f j i) (D.f j i))
⊢ D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
rw [← Category.assoc, ← D.t_fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GlueData.t_fac
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))

Tactic:
have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom =
      pullback.snd _ _ ≫ inv (pullback.fst _ _) := by simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))
⊢ D.t' i j i ≫ D.t' j i i ≫ D.t' i i j = 𝟙 (pullback (D.f i j) (D.f i i))

Tactic:
have := D.cocycle i j i