awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
x₁ x₂ : ∐ X₁
hx :
  Eq (α := ∐ X₂) ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₁ : ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₂ : ∐ X₂)
⊢ x₁ = x₂
have obtain : ∀ (i₁ : T) (x₁ : X₁ i₁)
  (hx :
    Eq (α := ∐ X₂)
      ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
          ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
                (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
              x₁ :
            (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
        ∐ X₂)
      ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₂ : ∐ X₂)),
  (hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
        (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
      x₁ =
    x₂
Tactic: obtain ⟨i₁, x₁, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₁
Cleared hypotheses: x₁, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
x₂ : ∐ X₁
i₁ : T
x₁ : X₁ i₁
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
              (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
            x₁ :
          (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₂ : ∐ X₂)
⊢ (hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
        (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
      x₁ =
    x₂
have obtain : ∀ (i₂ : T) (x₂ : X₁ i₂)
  (hx :
    Eq (α := ∐ X₂)
      ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
          ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
                (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
              x₁ :
            (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
        ∐ X₂)
      ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
          ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
                (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
              x₂ :
            (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
        ∐ X₂)),
  Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₁ :
      (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₂ :
      (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
Tactic: obtain ⟨i₂, x₂, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₂
Cleared hypotheses: x₂, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
              (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
            x₁ :
          (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
              (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
            x₂ :
          (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₁ :
      (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₂ :
      (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
have simp : Eq (α := ∐ X₁)
  ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
    (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
  ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
    (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
Tactic: simp only [cofan_mk_inj] at hx ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
⊢ Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
have h₁ : Eq (α := ∐ X₂)
  ((hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
        (a : X₁ i₁) → ∐ X₂)
      x₁ :
    ∐ X₂)
  ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
Tactic: have h₁ := congr_hom (Sigma.ι_map f i₁) x₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
⊢ Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
have h₂ : Eq (α := ∐ X₂)
  ((hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
        (a : X₁ i₂) → ∐ X₂)
      x₂ :
    ∐ X₂)
  ((hom (FC := TypeCat.Fun) (f i₂ ≫ Sigma.ι X₂ i₂) : (a : X₁ i₂) → ∐ X₂) x₂ : ∐ X₂)
Tactic: have h₂ := congr_hom (Sigma.ι_map f i₂) x₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
h₂ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₂) → ∐ X₂)
        x₂ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₂ ≫ Sigma.ι X₂ i₂) : (a : X₁ i₂) → ∐ X₂) x₂ : ∐ X₂)
⊢ Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
have h₃ : Eq (α := ∐ X₂)
  ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → ∐ X₁) x₁ : ∐ X₁) :
    ∐ X₂)
  ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : X₂ i₁) → ∐ X₂)
      ((hom (FC := TypeCat.Fun) (f i₁) : (a : X₁ i₁) → X₂ i₁) x₁ : X₂ i₁) :
    ∐ X₂)
Tactic: simp only [comp_apply] at h₁ h₂ hx
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
h₂ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₂) → ∐ X₂)
        x₂ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₂ ≫ Sigma.ι X₂ i₂) : (a : X₁ i₂) → ∐ X₂) x₂ : ∐ X₂)
h₃ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → ∐ X₁) x₁ : ∐ X₁) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : X₂ i₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : X₁ i₁) → X₂ i₁) x₁ : X₂ i₁) :
      ∐ X₂)
⊢ Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
have h₄ : Eq (α := ∐ X₂)
  ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → ∐ X₁) x₂ : ∐ X₁) :
    ∐ X₂)
  ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : X₂ i₂) → ∐ X₂)
      ((hom (FC := TypeCat.Fun) (f i₂) : (a : X₁ i₂) → X₂ i₂) x₂ : X₂ i₂) :
    ∐ X₂)
Tactic: simp only [comp_apply] at h₁ h₂ hx
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
have hx₁ : Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
  ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
      ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
        (fun (X : Type u) ↦ X) (X₂ i₁)) :
    (fun (X : Type u) ↦ X) (∐ X₂))
  ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
      ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
        (fun (X : Type u) ↦ X) (X₂ i₂)) :
    (fun (X : Type u) ↦ X) (∐ X₂))
Tactic: replace hx : Sigma.ι X₂ i₁ (f i₁ x₁) = Sigma.ι X₂ i₂ (f i₂ x₂) := by
      have h₁ := congr_hom (Sigma.ι_map f i₁) x₁
      have h₂ := congr_hom (Sigma.ι_map f i₂) x₂
      simp only [comp_apply] at h₁ h₂ hx
      simpa [← h₁, ← h₂]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
have obtain : ∀ (x₂ : X₁ i₁)
  (hx :
    Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
          ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
            (fun (X : Type u) ↦ X) (X₂ i₁)) :
        (fun (X : Type u) ↦ X) (∐ X₂))
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
          ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₂ :
            (fun (X : Type u) ↦ X) (X₂ i₁)) :
        (fun (X : Type u) ↦ X) (∐ X₂))),
  Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
Tactic: obtain rfl := Cofan.eq_of_inj_apply_eq_of_isColimit (coproductIsCoproduct X₂) _ _ hx
Cleared hypotheses: i₂, x₂, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ x₂ : X₁ i₁
hx :
  Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
have obtain : ∀
  (hx :
    Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
          ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
            (fun (X : Type u) ↦ X) (X₂ i₁)) :
        (fun (X : Type u) ↦ X) (∐ X₂))
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
          ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
            (fun (X : Type u) ↦ X) (X₂ i₁)) :
        (fun (X : Type u) ↦ X) (∐ X₂))),
  Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
Tactic: obtain rfl := h _ (Cofan.inj_injective_of_isColimit (coproductIsCoproduct X₂) i₁ hx)
Cleared hypotheses: x₂, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.UnivLE (goal)
Goal:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
⊢ Small.{v, max u v} α
have obtain : ∀ (a' : Type v) (m : Nonempty (uliftFunctor.{u, v}.obj a' ≅ α)), Small.{v, max u v} α
Tactic: obtain ⟨a', m⟩ := w.mem_essImage α
-- Lean 4 proof step from Mathlib.CategoryTheory.UnivLE (goal)
Goal:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m : Nonempty (uliftFunctor.{u, v}.obj a' ≅ α)
⊢ Small.{v, max u v} α
have obtain : ∀ (m' : uliftFunctor.{u, v}.obj a' ≅ α), Small.{v, max u v} α
Tactic: obtain ⟨m'⟩ := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f
have rw : G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f
Tactic: rw [Functor.comp_map, Functor.comp_map, α.naturality]