awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso (hypothesis)
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
i' :
  IsIso (X :=
    Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
      (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
    (Functor.map (forget D (FC := FD) (CC := CD))
      (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))
⊢ IsIso f
have this : IsIso (X := Functor.obj.{v_1, u, u + 1, u + 1} (forget C (FC := FC) (CC := CC)) X)
  (Functor.map (forget C (FC := FC) (CC := CC)) f)
Tactic: haveI : IsIso ((forget C).map f) := by
        rwa [← @HasForget₂.forget_comp C _ _ _ _ _ D _ _ _ _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
⊢ (conj (refl X) : (a : End X) → End X) f = f
have rw : inv (refl X) ≫ f ≫ hom (refl X) = f
Tactic: rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
rw : inv (refl X) ≫ f ≫ hom (refl X) = f
⊢ (conj (refl X) : (a : End X) → End X) f = f
have rw₁ : 𝟙 X ≫ f ≫ hom (refl X) = f
Tactic: rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
rw : inv (refl X) ≫ f ≫ hom (refl X) = f
rw₁ : 𝟙 X ≫ f ≫ hom (refl X) = f
⊢ (conj (refl X) : (a : End X) → End X) f = f
have rw₂ : 𝟙 X ≫ f ≫ 𝟙 X = f
Tactic: rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
rw : inv (refl X) ≫ f ≫ hom (refl X) = f
rw₁ : 𝟙 X ≫ f ≫ hom (refl X) = f
rw₂ : 𝟙 X ≫ f ≫ 𝟙 X = f
⊢ (conj (refl X) : (a : End X) → End X) f = f
have rw₃ : f ≫ 𝟙 X = f
Tactic: rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
rw : inv (refl X) ≫ f ≫ hom (refl X) = f
rw₁ : 𝟙 X ≫ f ≫ hom (refl X) = f
rw₂ : 𝟙 X ≫ f ≫ 𝟙 X = f
rw₃ : f ≫ 𝟙 X = f
⊢ (conj (refl X) : (a : End X) → End X) f = f
have rw₄ : f = f
Tactic: rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ (α.symm.conj : (a : End Y) → End X) ((α.conj : (a : End X) → End Y) f : End Y) = f
have rw : ((α ≪≫ α.symm).conj : (a : End X) → End X) f = f
Tactic: rw [← trans_conj, α.self_symm_id, refl_conj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
rw : ((α ≪≫ α.symm).conj : (a : End X) → End X) f = f
⊢ (α.symm.conj : (a : End Y) → End X) ((α.conj : (a : End X) → End Y) f : End Y) = f
have rw₁ : (conj (refl X) : (a : End X) → End X) f = f
Tactic: rw [← trans_conj, α.self_symm_id, refl_conj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
rw : ((α ≪≫ α.symm).conj : (a : End X) → End X) f = f
rw₁ : (conj (refl X) : (a : End X) → End X) f = f
⊢ (α.symm.conj : (a : End Y) → End X) ((α.conj : (a : End X) → End Y) f : End Y) = f
have rw₂ : f = f
Tactic: rw [← trans_conj, α.self_symm_id, refl_conj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Conj (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
α : X ≅ Y
f : Aut X
⊢ Eq (α := F.obj Y ≅ F.obj Y) (F.mapIso ((α.conjAut : (a : Aut X) → Aut Y) f))
    (((F.mapIso α).conjAut : (a : Aut (F.obj X)) → Aut (F.obj Y)) (F.mapIso f))
have w : Eq (α := F.obj Y ⟶ F.obj Y) (Iso.hom (F.mapIso ((α.conjAut : (a : Aut X) → Aut Y) f)))
  (Iso.hom (((F.mapIso α).conjAut : (a : Aut (F.obj X)) → Aut (F.obj Y)) (F.mapIso f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
X : Type u_1
f : ConnectedComponents.{v_1, u_2} J → X
x : ConnectedComponents.{v_1, u_2} J
⊢ liftFunctor J (functorToDiscrete X f) x = f x
have obtain : ∀ (x_1 : J) (h : ⟦x_1⟧ = x), liftFunctor J (functorToDiscrete X f) x = f x
Tactic: obtain ⟨x, h⟩ := Quotient.exists_rep x
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
X : Type u_1
f : ConnectedComponents.{v_1, u_2} J → X
x_1 : ConnectedComponents.{v_1, u_2} J
x : J
h : ⟦x⟧ = x_1
⊢ liftFunctor J (functorToDiscrete X f) x_1 = f x_1
have rw : liftFunctor J (functorToDiscrete X f) ⟦x⟧ = f ⟦x⟧
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : ConnectedComponents.{v₁, u₁} J
⊢ Nonempty.{u₁ + 1} j.Component
have h : ∀ (a : J), Nonempty.{u₁ + 1} (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' a))
Tactic: induction j using Quotient.inductionOn'
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : ConnectedComponents.{v₁, u₁} J
⊢ IsConnected.{v₁, u₁} j.Component
have h : ∀ (j₁ j₂ : j.Component), ∃ (l : List j.Component), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast sorry = j₂
Tactic: apply isConnected_of_zigzag
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
⊢ ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          ⋯ =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯
have h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
Tactic: have h₁₂ : Zigzag j₁ j₂ := Quotient.exact' hj₁
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
⊢ ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          ⋯ =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯
have h : ∀ (l : List J) (hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)) (hl₂ : (j₁ :: l).getLast sorry = j₂),
  ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          sorry =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ sorry
Tactic: rcases List.exists_isChain_cons_of_relationReflTransGen h₁₂ with ⟨l, hl₁, hl₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
i : J
hi : i ∈ l
⊢ Zigzag.{v₁, u₁} i j₂
have apply : ∀ ⦃x y : J⦄, Zag.{v₁, u₁} x y → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) y → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) x
Tactic: apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
i : J
hi : i ∈ l
apply : ∀ ⦃x y : J⦄, Zag.{v₁, u₁} x y → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) y → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) x
⊢ Zigzag.{v₁, u₁} i j₂
have apply₁ : Zigzag.{v₁, u₁} j₂ j₂
Tactic: apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
⊢ ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          ⋯ =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯
have hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
Tactic: have hf : ∀ a : J, a ∈ l → Zigzag a j₂ := by
    intro i hi
    apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
    · intro j k
      apply Relation.ReflTransGen.head
    · apply Relation.ReflTransGen.refl
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
⊢ ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          ⋯ =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯
have h : List.IsChain Zag.{v₁, u₁}
  (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
    List.pmap (P := fun (a : J) ↦ Zigzag.{v₁, u₁} a j₂) f l hf)
Tactic: refine ⟨l.pmap f hf, ?_, by grind⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
⊢ List.IsChain Zag.{v₁, u₁}
    (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
      List.pmap (P := fun (a : J) ↦ Zigzag.{v₁, u₁} a j₂) f l hf)
have h : ∀ (x y : J) (x_1 : Zigzag.{v₁, u₁} x j₂) (x_2 : Zigzag.{v₁, u₁} y j₂) (h : Zag.{v₁, u₁} x y),
  Zag.{v₁, u₁} (f x x_1) (f y x_2)
Tactic: refine @List.isChain_cons_pmap_of_isChain_cons _ _ Zag _ _ f
    (fun x y _ _ h => ?_) _ _ h₁₂ hl₁ _
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ j' = k'
have rw : (Zigzag.setoid J : J → J → Prop) X Y
Tactic: rw [← hX, ← hY, Quotient.eq'']
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ ∃ (a :
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) k'
        (ObjectProperty.FullSubcategory.mk (P := k'.objectProperty) Y hY))),
    Functor.map (decomposedTo J) a = f
have this : j' = k'
Tactic: have : j' = k' := by
      rw [← hX, ← hY, Quotient.eq'']
      exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.ConnectedComponents (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
this : j' = k'
⊢ ∃ (a :
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) k'
        (ObjectProperty.FullSubcategory.mk (P := k'.objectProperty) Y hY))),
    Functor.map (decomposedTo J) a = f
have subst : ∀ (hY : j'.objectProperty Y),
  ∃ (a :
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) Y hY))),
    Functor.map (decomposedTo J) a = f
Tactic: subst this
Cleared hypotheses: k', hY, this
-- Lean 4 proof step from Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c : WideSubcategory P
inst_4 : ComonObj (c.obj (_P := P))
inst_5 : IsCommComonObj.{v_1, u_1} (c.obj (_P := P))
inst_6 : P.IsStableUnderComonoid (c.obj (_P := P))
⊢ Eq (α := c ⟶ MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := WideSubcategory.category P) c c) (Δ ≫ Iso.hom (β_ c c))
    Δ
have h : Eq (α :=
  c.obj (_P := P) ⟶ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := WideSubcategory.category P) c c).obj (_P := P))
  (InducedWideCategory.Hom.hom (P := P) (Δ ≫ Iso.hom (β_ c c))) (InducedWideCategory.Hom.hom (P := P) Δ)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Core (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
⊢ f = g
have iso : f.iso = g.iso
Tactic: apply CoreHom.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Core (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
α : Core (Type u₁)
⊢ { iso := (EquivFunctor.mapEquiv m (CoreHom.iso (𝟙 α)).toEquiv).toIso :
      CoreHom { of := m α.of : Core (Type u₂) } { of := m α.of : Core (Type u₂) } } =
    𝟙 { of := m α.of }
have h : ∀ (x : { of := m α.of }.of),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          { iso := (EquivFunctor.mapEquiv m (CoreHom.iso (𝟙 α)).toEquiv).toIso :
                CoreHom { of := m α.of : Core (Type u₂) } { of := m α.of : Core (Type u₂) } }.iso.hom).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (CoreHom.iso (𝟙 { of := m α.of : Core (Type u₂) })).hom).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Core (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
X Y Z : Core (Type u₁)
f : X ⟶ Y
g : Y ⟶ Z
⊢ { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso :
      CoreHom { of := m X.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } } =
    { iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso :
        CoreHom { of := m X.of : Core (Type u₂) } { of := m Y.of : Core (Type u₂) } } ≫
      { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }
have h : ∀ (x : { of := m X.of }.of),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso :
                CoreHom { of := m X.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } }.iso.hom).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
          (CoreHom.iso
            ({ iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso :
                CoreHom { of := m X.of : Core (Type u₂) } { of := m Y.of : Core (Type u₂) } } ≫
              { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso :
                CoreHom { of := m Y.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } }))))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : Dial.{v, u} C
F : X.Hom Y
G : Y.Hom Z
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)
have refine_1 : LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
  (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
  (Functor.obj (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
    (Functor.obj (Subobject.pullback π(π₁, F.F)) X.rel))
Tactic: refine
    le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : Dial.{v, u} C
F : X.Hom Y
G : Y.Hom Z
refine_1 :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback π(π₁, F.F)) X.rel))
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)
have refine_2 : LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
  (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
    (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
    (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Y.tgt))) Y.rel))
  (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))) (Functor.obj (Subobject.pullback π(π₁, G.F)) Y.rel))
Tactic: refine
    le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : Dial.{v, u} C
F : X.Hom Y
G : Y.Hom Z
refine_1 :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback π(π₁, F.F)) X.rel))
refine_2 :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
      (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Y.tgt))) Y.rel))
    (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))) (Functor.obj (Subobject.pullback π(π₁, G.F)) Y.rel))
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)
have refine_3 : LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
  (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} Y.src Z.tgt)) (Subobject.pullback (prod.map F.f (𝟙 Z.tgt)))
    (Functor.obj (Subobject.pullback (prod.map G.f (𝟙 Z.tgt))) Z.rel))
  (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)
Tactic: refine
    le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_