awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
h : Zigzag.{v₁, u₁} j j'
h₁ : F j = F j
⊢ F j = F j'
have h₂ : ∀ {b c : J}, Relation.ReflTransGen Zag.{v₁, u₁} j b → ∀ (hj : Zag.{v₁, u₁} b c) (ih : F j = F b), F j = F c
Tactic: induction h with
  | refl => rfl
  | tail _ hj ih =>
    rw [ih]
    rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
    exacts [hF hj, (hF hj).symm]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsPreconnected.{v₁, u₁} J
have h₁ : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
Tactic: apply zigzag_isPreconnected
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
⊢ Zigzag.{v₁, u₁} j₁ j₂
have h₁ : ∀ (l : List J) (hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)) (hl₂ : (j₁ :: l).getLast sorry = j₂), Zigzag.{v₁, u₁} j₁ j₂
Tactic: rcases h j₁ j₂ with ⟨l, hl₁, hl₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type w₂
inst_2 : Category.{w₁, w₂} C
inst_3 : IsConnected.{v₁, u₁} J
X Y : C
f : Quiver.Hom (V := Functor.{v₁, w₁, u₁, w₂} J C) (obj (const J) X) (obj (const J) Y)
⊢ map (const J) (f.app (Classical.arbitrary J)) = f
have w : ∀ (j : J), NatTrans.app (map (const J) (f.app (Classical.arbitrary J))) j = f.app j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
G : Type u_1
inst : Groupoid.{u_2, u_1} G
inst_1 : IsPreconnected.{u_2, u_1} G
⊢ ∀ (x y : G), Nonempty.{u_2 + 1} (x ⟶ y)
have refine : _root_.Equivalence fun (x y : G) ↦ Nonempty.{u_2 + 1} (x ⟶ y)
Tactic: refine equiv_relation _ ?_ fun {j₁ j₂} => Nonempty.intro
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
have w : ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ refl X ≪≫ α = α
have w : (refl X ≪≫ α).hom = α.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α ≪≫ refl Y = α
have w : (α ≪≫ refl Y).hom = α.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ α.symm ≪≫ α ≪≫ β = β
have rw : (α.symm ≪≫ α) ≪≫ β = β
Tactic: rw [← trans_assoc, symm_self_id, refl_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
rw : (α.symm ≪≫ α) ≪≫ β = β
⊢ α.symm ≪≫ α ≪≫ β = β
have rw₁ : refl Y ≪≫ β = β
Tactic: rw [← trans_assoc, symm_self_id, refl_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
rw : (α.symm ≪≫ α) ≪≫ β = β
rw₁ : refl Y ≪≫ β = β
⊢ α.symm ≪≫ α ≪≫ β = β
have rw₂ : β = β
Tactic: rw [← trans_assoc, symm_self_id, refl_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ α ≪≫ α.symm ≪≫ β = β
have rw : (α ≪≫ α.symm) ≪≫ β = β
Tactic: rw [← trans_assoc, self_symm_id, refl_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
rw : (α ≪≫ α.symm) ≪≫ β = β
⊢ α ≪≫ α.symm ≪≫ β = β
have rw₁ : refl X ≪≫ β = β
Tactic: rw [← trans_assoc, self_symm_id, refl_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
rw : (α ≪≫ α.symm) ≪≫ β = β
rw₁ : refl X ≪≫ β = β
⊢ α ≪≫ α.symm ≪≫ β = β
have rw₂ : β = β
Tactic: rw [← trans_assoc, self_symm_id, refl_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 : X ≅ Y
X_1 Y_1 : C
f g : X_1 ≅ Y_1
h : f.hom = g.hom
⊢ f.inv = g.inv
have rw : g.inv = g.inv
Tactic: rw [ext h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv
have rw : f = α.inv ≫ 𝟙 X ↔ f = α.inv
Tactic: rw [← eq_inv_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
rw : f = α.inv ≫ 𝟙 X ↔ f = α.inv
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv
have rw₁ : f = α.inv ↔ f = α.inv
Tactic: rw [← eq_inv_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ f ≫ α.hom = 𝟙 Y ↔ f = α.inv
have rw : f = 𝟙 Y ≫ α.inv ↔ f = α.inv
Tactic: rw [← eq_comp_inv, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
rw : f = 𝟙 Y ≫ α.inv ↔ f = α.inv
⊢ f ≫ α.hom = 𝟙 Y ↔ f = α.inv
have rw₁ : f = α.inv ↔ f = α.inv
Tactic: rw [← eq_comp_inv, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.hom = β.inv ↔ β.hom = α.inv
have rw : β.hom = α.symm.hom ↔ β.hom = α.inv
Tactic: rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : IsIso f
Z_1 : C
g h : Y ⟶ Z_1
w : f ≫ g = f ≫ h
⊢ g = h
have rw : inv f ≫ f ≫ g = h
Tactic: rw [← IsIso.inv_hom_id_assoc f g, w, IsIso.inv_hom_id_assoc f h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : IsIso f
Z_1 : C
g h : Y ⟶ Z_1
w : f ≫ g = f ≫ h
rw : inv f ≫ f ≫ g = h
⊢ g = h
have rw₁ : inv f ≫ f ≫ h = h
Tactic: rw [← IsIso.inv_hom_id_assoc f g, w, IsIso.inv_hom_id_assoc f h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : IsIso f
Z_1 : C
g h : Y ⟶ Z_1
w : f ≫ g = f ≫ h
rw : inv f ≫ f ≫ g = h
rw₁ : inv f ≫ f ≫ h = h
⊢ g = h
have rw₂ : h = h
Tactic: rw [← IsIso.inv_hom_id_assoc f g, w, IsIso.inv_hom_id_assoc f h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ inv f = g
have this : Eq.{v + 1} (α := Y ⟶ X) ((fun (x : X ⟶ X) ↦ inv f ≫ x) (f ≫ g)) ((fun (x : X ⟶ X) ↦ inv f ≫ x) (𝟙 X))
Tactic: have := congrArg (inv f ≫ ·) hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ X) (inv (𝟙 X)) (𝟙 X)
have hom_inv_id : Eq.{v + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X)
Tactic: apply inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso h
⊢ inv (f ≫ h) = inv h ≫ inv f
have hom_inv_id : (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X
Tactic: apply inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ inv (inv f) = f
have hom_inv_id : inv f ≫ f = 𝟙 Y
Tactic: apply inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ inv f.inv = f.hom
have hom_inv_id : f.inv ≫ f.hom = 𝟙 Y
Tactic: apply inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsIso (f ≫ g)
⊢ IsIso g
have rw : IsIso (inv f ≫ f ≫ g)
Tactic: rw [← id_comp g, ← inv_hom_id f, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : IsIso f
hh : IsIso h
w : f ≫ g = h
⊢ IsIso g
have hh₁ : IsIso (f ≫ g)
Tactic: rw [← w] at hh
Cleared hypotheses: hh, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
p : inv f = inv g
⊢ f = g
have apply : inv f ≫ f = inv f ≫ g
Tactic: apply (cancel_epi (inv f)).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
p : inv f = inv g
⊢ inv f ≫ f = inv f ≫ g
have rw : 𝟙 Y = inv f ≫ g
Tactic: rw [inv_hom_id, p, inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
p : inv f = inv g
rw : 𝟙 Y = inv f ≫ g
⊢ inv f ≫ f = inv f ≫ g
have rw₁ : 𝟙 Y = inv g ≫ g
Tactic: rw [inv_hom_id, p, inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : IsIso f
inst_2 : IsIso g
p : inv f = inv g
rw : 𝟙 Y = inv f ≫ g
rw₁ : 𝟙 Y = inv g ≫ g
⊢ inv f ≫ f = inv f ≫ g
have rw₂ : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) (𝟙 Y)
Tactic: rw [inv_hom_id, p, inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso f
have rw : IsIso (inv g)
Tactic: rw [(hom_comp_eq_id _).mp h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j
have w : (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ F.map (inv f) = inv (F.map f)
have hom_inv_id : F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
Tactic: apply eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.IsomorphismClasses (goal)
Goal:
C : Cat
⊢ ↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
        (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj ⋯ =
    𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
have h : ∀ (x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj
            sorry))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.IsomorphismClasses (goal)
Goal:
C : Cat
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj
            ⋯))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
      x
have h : ∀ (a b : (↑C : Type u)) (p : (isIsomorphicSetoid (↑C : Type u) : (↑C : Type u) → (↑C : Type u) → Prop) a b), sorry = sorry
Tactic: apply @Quot.recOn _ _ _ x
-- Lean 4 proof step from Mathlib.CategoryTheory.IsomorphismClasses (goal)
Goal:
C : Cat
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
h : ∀ (a b : (↑C : Type u)) (p : (isIsomorphicSetoid (↑C : Type u) : (↑C : Type u) → (↑C : Type u) → Prop) a b), ⋯ = ⋯
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj
            ⋯))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
      x
have h₁ : ∀ (a : (↑C : Type u)),
  TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj
            sorry))
      (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
      (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a)
Tactic: apply @Quot.recOn _ _ _ x
-- Lean 4 proof step from Mathlib.CategoryTheory.IsomorphismClasses (goal)
Goal:
C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ Eq (α :=
    Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)) ⟶
      Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
    (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
        (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯)
    (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
      (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
          (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
      (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
          (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯))
have h : ∀ (x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))),
  Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj sorry))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj sorry)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj sorry)))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.IsomorphismClasses (goal)
Goal:
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
⊢ Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯)))
      x)
have h : ∀ (a b : (↑C : Type u)) (p : (isIsomorphicSetoid (↑C : Type u) : (↑C : Type u) → (↑C : Type u) → Prop) a b),
  Eq (α :=
    Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
      (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj sorry))
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) b))
      (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj sorry)
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj sorry)))
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) b)))
    sorry sorry
Tactic: apply @Quot.recOn _ _ _ x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x.Hom y
⊢ comp x.id f = f
have left : ∀ (a : C) (f : Hom (left a) y), comp (id (left a)) f = f
Tactic: cases x
Cleared hypotheses: x, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x.Hom y
left : ∀ (a : C) (f : Hom (Join.left a) y), comp (id (Join.left a)) f = f
⊢ comp x.id f = f
have right : ∀ (a : D) (f : Hom (right a) y), comp (id (right a)) f = f
Tactic: cases x
Cleared hypotheses: x, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : C
f : Hom (left a) y
⊢ comp (id (left a)) f = f
have left : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)), comp (id (left a)) f = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : C
f : Hom (Join.left a) y
left : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)), comp (id (Join.left a)) f = f
⊢ comp (id (Join.left a)) f = f
have left₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)), comp (id (Join.left a)) f = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : D
f : Hom (right a) y
⊢ comp (id (right a)) f = f
have right : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)), comp (id (right a)) f = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : D
f : Hom (Join.right a) y
right : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)), comp (id (Join.right a)) f = f
⊢ comp (id (Join.right a)) f = f
have right₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)), comp (id (Join.right a)) f = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
⊢ comp (id (left a)) f = f
have left : { down := f.down : ULift.{v₂, v₁} (a ⟶ a_1) } = f
Tactic: simp only [Hom, id, comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
⊢ comp (id (right a)) f = f
have right : (match (motive :=
    (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
        | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
        | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
        | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
        | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
          match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
    right a, right a, left a_1, { down := 𝟙 a }, f with
  | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
  | left _x, left _y, right _z, x, x_1 => PUnit.unit
  | left _x, right _y, right _z, x, x_1 => PUnit.unit
  | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
  f
Tactic: simp only [Hom, id, comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
⊢ comp (id (right a)) f = f
have right : { down := f.down : ULift.{v₁, v₂} (a ⟶ a_1) } = f
Tactic: simp only [Hom, id, comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x.Hom y
⊢ comp f y.id = f
have left : ∀ (a : C) (f : Hom (left a) y), comp f y.id = f
Tactic: cases x
Cleared hypotheses: x, f