awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
h₀ :
  Eq (α := pullback f g ⟶ X'')
    (CategoryStruct.comp (Y := pullback f'' g'')
      (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
      (fst f'' g''))
    (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯) (fst f'' g''))
⊢ Eq (α := pullback f g ⟶ pullback f'' g'')
    (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
    (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯)
have h₁ : Eq (α := pullback f g ⟶ Y'')
  (CategoryStruct.comp (Y := pullback f'' g'')
    (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
    (snd f'' g''))
  (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) sorry sorry) (snd f'' g''))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = 𝟙 (pullback f g)
have h₀ : CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) sorry sorry) (fst f g) = 𝟙 (pullback f g) ≫ fst f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
h₀ : CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (fst f g) = 𝟙 (pullback f g) ≫ fst f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = 𝟙 (pullback f g)
have h₁ : CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) sorry sorry) (snd f g) = 𝟙 (pullback f g) ≫ snd f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''
have rw : i₁ ≫ f' ≫ j₂ = (i₁ ≫ j₁) ≫ f''
Tactic: rw [reassoc_of% e₁, e₃, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
rw : i₁ ≫ f' ≫ j₂ = (i₁ ≫ j₁) ≫ f''
⊢ f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''
have rw₁ : i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
Tactic: rw [reassoc_of% e₁, e₃, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
rw : i₁ ≫ f' ≫ j₂ = (i₁ ≫ j₁) ≫ f''
rw₁ : i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
⊢ f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''
have rw₂ : i₁ ≫ j₁ ≫ f'' = i₁ ≫ j₁ ≫ f''
Tactic: rw [reassoc_of% e₁, e₃, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''
have rw : i₁ ≫ g' ≫ j₃ = (i₁ ≫ j₁) ≫ g''
Tactic: rw [reassoc_of% e₂, e₄, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
rw : i₁ ≫ g' ≫ j₃ = (i₁ ≫ j₁) ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''
have rw₁ : i₁ ≫ j₁ ≫ g'' = (i₁ ≫ j₁) ≫ g''
Tactic: rw [reassoc_of% e₂, e₄, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
rw : i₁ ≫ g' ≫ j₃ = (i₁ ≫ j₁) ≫ g''
rw₁ : i₁ ≫ j₁ ≫ g'' = (i₁ ≫ j₁) ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''
have rw₂ : i₁ ≫ j₁ ≫ g'' = i₁ ≫ j₁ ≫ g''
Tactic: rw [reassoc_of% e₂, e₄, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ Eq (α := pushout f g ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄))
    (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯)
have h₀ : Eq (α := Y ⟶ pushout f'' g'')
  (CategoryStruct.comp (Y := pushout f g) (inl f g)
    (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
  (CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
h₀ :
  Eq (α := Y ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f g) (inl f g)
      (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
    (CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯))
⊢ Eq (α := pushout f g ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄))
    (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯)
have h₁ : Eq (α := Z ⟶ pushout f'' g'')
  (CategoryStruct.comp (Y := pushout f g) (inr f g)
    (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
  (CategoryStruct.comp (Y := pushout f g) (inr f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (pushout f g)
have h₀ : CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) sorry sorry) = inl f g ≫ 𝟙 (pushout f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
h₀ : CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯) = inl f g ≫ 𝟙 (pushout f g)
⊢ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (pushout f g)
have h₁ : CategoryStruct.comp (Y := pushout f g) (inr f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) sorry sorry) = inr f g ≫ 𝟙 (pushout f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
⊢ IsIso (X := pullback f₁ f₂) (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_1 : g₁ ≫ inv i₃ = inv i₁ ≫ f₁
Tactic: refine ⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ ≫ inv i₃ = inv i₁ ≫ f₁
⊢ IsIso (X := pullback f₁ f₂) (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_2 : g₂ ≫ inv i₃ = inv i₂ ≫ f₂
Tactic: refine ⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ ≫ inv i₃ = inv i₁ ≫ f₁
refine_2 : g₂ ≫ inv i₃ = inv i₂ ≫ f₂
⊢ IsIso (X := pullback f₁ f₂) (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_3 : CategoryStruct.comp (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
    (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) sorry sorry) =
  𝟙 (pullback f₁ f₂)
Tactic: refine ⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ ≫ inv i₃ = inv i₁ ≫ f₁
refine_2 : g₂ ≫ inv i₃ = inv i₂ ≫ f₂
refine_3 :
  CategoryStruct.comp (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
      (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯) =
    𝟙 (pullback f₁ f₂)
⊢ IsIso (X := pullback f₁ f₂) (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_4 : CategoryStruct.comp (Y := pullback f₁ f₂) (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) sorry sorry)
    (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
  𝟙 (pullback g₁ g₂)
Tactic: refine ⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
⊢ g₁ ≫ inv i₃ = inv i₁ ≫ f₁
have refine_1 : g₁ = (inv i₁ ≫ f₁) ≫ i₃
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ = (inv i₁ ≫ f₁) ≫ i₃
⊢ g₁ ≫ inv i₃ = inv i₁ ≫ f₁
have refine_1₁ : g₁ = inv i₁ ≫ f₁ ≫ i₃
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ = (inv i₁ ≫ f₁) ≫ i₃
refine_1₁ : g₁ = inv i₁ ≫ f₁ ≫ i₃
⊢ g₁ ≫ inv i₃ = inv i₁ ≫ f₁
have refine_1₂ : g₁ = inv i₁ ≫ i₁ ≫ g₁
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ = (inv i₁ ≫ f₁) ≫ i₃
refine_1₁ : g₁ = inv i₁ ≫ f₁ ≫ i₃
refine_1₂ : g₁ = inv i₁ ≫ i₁ ≫ g₁
⊢ g₁ ≫ inv i₃ = inv i₁ ≫ f₁
have refine_1₃ : g₁ = g₁
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
⊢ g₂ ≫ inv i₃ = inv i₂ ≫ f₂
have refine_2 : g₂ = (inv i₂ ≫ f₂) ≫ i₃
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₂ ≫ f₂) ≫ i₃
⊢ g₂ ≫ inv i₃ = inv i₂ ≫ f₂
have refine_2₁ : g₂ = inv i₂ ≫ f₂ ≫ i₃
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₂ ≫ f₂) ≫ i₃
refine_2₁ : g₂ = inv i₂ ≫ f₂ ≫ i₃
⊢ g₂ ≫ inv i₃ = inv i₂ ≫ f₂
have refine_2₂ : g₂ = inv i₂ ≫ i₂ ≫ g₂
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₂ ≫ f₂) ≫ i₃
refine_2₁ : g₂ = inv i₂ ≫ f₂ ≫ i₃
refine_2₂ : g₂ = inv i₂ ≫ i₂ ≫ g₂
⊢ g₂ ≫ inv i₃ = inv i₂ ≫ f₂
have refine_2₃ : g₂ = g₂
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ Eq (α := pullback f₂ g₂ ⟶ pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
have h₀ : Eq (α := pullback f₂ g₂ ⟶ X) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (fst f₁ g₁))
  (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) sorry sorry) (fst f₁ g₁))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
h₀ :
  Eq (α := pullback f₂ g₂ ⟶ X) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (fst f₁ g₁))
    (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (fst f₁ g₁))
⊢ Eq (α := pullback f₂ g₂ ⟶ pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
have h₃ : Eq (α := pullback f₂ g₂ ⟶ Y) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (snd f₁ g₁))
  (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) sorry sorry) (snd f₁ g₁))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
⊢ IsIso (X := pushout f₁ f₂) (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_1 : g₁ ≫ inv i₁ = inv i₃ ≫ f₁
Tactic: refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ ≫ inv i₁ = inv i₃ ≫ f₁
⊢ IsIso (X := pushout f₁ f₂) (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_2 : g₂ ≫ inv i₂ = inv i₃ ≫ f₂
Tactic: refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ ≫ inv i₁ = inv i₃ ≫ f₁
refine_2 : g₂ ≫ inv i₂ = inv i₃ ≫ f₂
⊢ IsIso (X := pushout f₁ f₂) (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_3 : CategoryStruct.comp (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
    (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) sorry sorry) =
  𝟙 (pushout f₁ f₂)
Tactic: refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ ≫ inv i₁ = inv i₃ ≫ f₁
refine_2 : g₂ ≫ inv i₂ = inv i₃ ≫ f₂
refine_3 :
  CategoryStruct.comp (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
      (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯) =
    𝟙 (pushout f₁ f₂)
⊢ IsIso (X := pushout f₁ f₂) (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
have refine_4 : CategoryStruct.comp (Y := pushout f₁ f₂) (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) sorry sorry)
    (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
  𝟙 (pushout g₁ g₂)
Tactic: refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
⊢ g₁ ≫ inv i₁ = inv i₃ ≫ f₁
have refine_1 : g₁ = (inv i₃ ≫ f₁) ≫ i₁
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ = (inv i₃ ≫ f₁) ≫ i₁
⊢ g₁ ≫ inv i₁ = inv i₃ ≫ f₁
have refine_1₁ : g₁ = inv i₃ ≫ f₁ ≫ i₁
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ = (inv i₃ ≫ f₁) ≫ i₁
refine_1₁ : g₁ = inv i₃ ≫ f₁ ≫ i₁
⊢ g₁ ≫ inv i₁ = inv i₃ ≫ f₁
have refine_1₂ : g₁ = inv i₃ ≫ i₃ ≫ g₁
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_1 : g₁ = (inv i₃ ≫ f₁) ≫ i₁
refine_1₁ : g₁ = inv i₃ ≫ f₁ ≫ i₁
refine_1₂ : g₁ = inv i₃ ≫ i₃ ≫ g₁
⊢ g₁ ≫ inv i₁ = inv i₃ ≫ f₁
have refine_1₃ : g₁ = g₁
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]