awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X : C
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X), Epi p
have refine_1 : ∀ (ι : Type w) (s : ι → C) (hs : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (hc : 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), Epi p
Tactic: obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS X
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
⊢ IsIso i
have refine_2 : ∀ (ι : Type w) (s : ι → C) (hs : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (hc : IsColimit c) (p : c.pt ⟶ Y),
  ExtremalEpi p → IsIso i
Tactic: obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ Y
h_1 : ExtremalEpi p
⊢ IsIso i
have hi₁ : ∀ (j : ι), ∃ (a : s j ⟶ X), (fun (f : s j ⟶ X) ↦ f ≫ i) a = c.inj j ≫ p
Tactic: replace hi (j : ι) := hi (s j) (hs j) (c.inj j ≫ p)
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ Y
h_1 : ExtremalEpi p
hi : ∀ (j : ι), ∃ (a : s j ⟶ X), (fun (f : s j ⟶ X) ↦ f ≫ i) a = c.inj j ≫ p
⊢ IsIso i
have refine_2 : ∀ (φ : (j : ι) → s j ⟶ X) (hφ : ∀ (j : ι), (fun (f : s j ⟶ X) ↦ f ≫ i) (φ j) = c.inj j ≫ p), IsIso i
Tactic: choose φ hφ using hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ P.IsStrongGenerator ↔
    ∀ (X : C),
      ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
        ExtremalEpi p
have refine : ∀ (hP : P.IsStrongGenerator) (X : C),
  ∃ (ι : 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 hP X ↦ ?_, fun hP ↦ .mk_of_exists_extremalEpi hP⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (hypothesis)
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
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
    ExtremalEpi p
have this : HasCoproductsOfShape (CostructuredArrow P.ι X) C
Tactic: have := hasCoproductsOfShape_of_small.{w} C (CostructuredArrow P.ι X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
    ExtremalEpi p
have 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
Tactic: have := (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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.IsStrongGenerator
have 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
Tactic: rw [isStrongGenerator_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
have 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
Tactic: refine ⟨IsSeparating.mk_of_exists_colimitsOfShape hP, fun X Y i _ hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ IsIso i
have obtain : ∀ (r : Y ⟶ X) (fac : r ≫ i = 𝟙 Y), IsIso i
Tactic: obtain ⟨r, fac⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ IsIso i
have suffices : IsSplitEpi i
Tactic: suffices IsSplitEpi i by
    obtain ⟨r, fac⟩ := this
    exact ⟨r, by simp [← cancel_mono i, fac]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ IsSplitEpi i
have obtain : ∀ (J : Type w) (w : Category.{w', w} J) (p : ColimitOfShape.{w', w, v, u} P J Y), IsSplitEpi i
Tactic: obtain ⟨J, _, ⟨p⟩⟩ := hP Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ IsSplitEpi i
have 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
Tactic: choose φ hφ using fun j ↦ hi _ (p.prop_diag_obj j) (p.ι.app j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
have 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
Tactic: refine ⟨p.isColimit.desc c, p.isColimit.hom_ext (fun j ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ { 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
have dsimp : p.toColimitPresentation (P := P).ι.app j ≫ p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
  p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
Tactic: dsimp at hφ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ p.toColimitPresentation (P := P).ι.app j ≫ p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
    p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
have rw : c.ι.app j ≫ i = p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
Tactic: rw [p.isColimit.fac_assoc, hφ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ p.toColimitPresentation (P := P).ι.app j ≫ p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
    p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
have rw₁ : p.toColimitPresentation (P := P).ι.app j = p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
Tactic: rw [p.isColimit.fac_assoc, hφ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ p.toColimitPresentation (P := P).ι.app j ≫ p.toColimitPresentation (P := P).isColimit.desc c ≫ i =
    p.toColimitPresentation (P := P).ι.app j ≫ 𝟙 Y
have rw₂ : p.toColimitPresentation (P := P).ι.app j = p.toColimitPresentation (P := P).ι.app j
Tactic: rw [p.isColimit.fac_assoc, hφ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Type (goal)
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
⊢ f = g
have h₁ : ∀ (x : X), (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.t' i i j = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))
have 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
Tactic: have eq₁ := D.t_fac i i j
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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
⊢ D.t' i i j = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))
have 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))
Tactic: have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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 = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))
have 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)
Tactic: rw [D.t_id, Category.comp_id, eq₂] at eq₁
Cleared hypotheses: eq₁, eq₂
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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 = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))
have 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
Tactic: have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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 = Iso.hom (pullbackSymmetry (D.f i i) (D.f i j))
have 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
Tactic: rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃
Cleared hypotheses: eq₃
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.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))
have 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))
Tactic: rw [← Category.assoc, ← D.t_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ 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))
have 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))
Tactic: rw [← Category.assoc, ← D.t_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
have 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)))
Tactic: have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom =
      pullback.snd _ _ ≫ inv (pullback.fst _ _) := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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 ≫ D.t j i = 𝟙 (D.V (i, j))
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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)))
this : D.t' i j i ≫ D.t' j i i ≫ D.t' i i j = 𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
have this₁ : CategoryStruct.comp (Y := pullback (D.f j i) (D.f 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)))
    (CategoryStruct.comp (Y := pullback (D.f i i) (D.f i j))
      (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (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)))) =
  𝟙 (pullback (D.f i j) (D.f i i))
Tactic: rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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)))
this :
  CategoryStruct.comp (Y := pullback (D.f j i) (D.f 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)))
      (CategoryStruct.comp (Y := pullback (D.f i i) (D.f i j))
        (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (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)))) =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
have this₁ : pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
  𝟙 (pullback (D.f i j) (D.f i i))
Tactic: simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
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)))
this :
  pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
have this₁ : D.t i j ≫ D.t j i =
  (inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))) ≫ pullback.fst (D.f i j) (D.f i i)
Tactic: rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ D.t' i j k ≫
      Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j)) =
    𝟙 (pullback (D.f i j) (D.f i k))
have rw : (D.t' i j k ≫
      Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))) ≫
    pullback.fst (D.f i j) (D.f i k) =
  𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)
Tactic: rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j =
    Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))
have trans : D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)
Tactic: trans inv (D.t' i j k)
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
trans : D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)
⊢ D.t' j k i ≫ D.t' k i j =
    Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))
have trans₁ : inv (D.t' i j k) =
  Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))
Tactic: trans inv (D.t' i j k)
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ inv (D.t' i j k) =
    Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))
have rw : inv (D.t' i j k) ≫ pullback.fst (D.f i j) (D.f i k) =
  (Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))) ≫
    pullback.fst (D.f i j) (D.f i k)
Tactic: rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]