awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsNoetherianObject.{v, u} Y
f : ℕ →o Subobject.{v, u} X
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
have obtain : ∀ (n : ℕ)
  (hn :
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} Y)
          (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := sorry : ℕ →o Subobject.{v, u} Y } :
                (a : ℕ) → Subobject Y)
              n :
            Subobject.{v, u} Y)
          (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := sorry : ℕ →o Subobject.{v, u} Y } :
                (a : ℕ) → Subobject Y)
              m :
            Subobject.{v, u} Y)),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
Tactic: obtain ⟨n, hn⟩ := monotone_chain_condition_of_isNoetherianObject
    ⟨_, (Subobject.map i).monotone.comp f.2⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
hY : isNoetherianObject.{v, u} Y_1
⊢ isNoetherianObject.{v, u} X_1
have rw : ∀ (hY : ObjectProperty.Is.{v, u} isNoetherianObject Y_1), ObjectProperty.Is.{v, u} isNoetherianObject X_1
Tactic: rw [← isNoetherianObject.is_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
x : Cᵒᵖ
⊢ ↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))) = 𝟙 (Subobject.{v, u} (Opposite.unop x))
have h : ∀ (x_1 : Subobject.{v, u} (Opposite.unop x)),
  TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))))) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Subobject.{v, u} (Opposite.unop x)))).toFun x_1
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
X Y Z : Cᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ ↾(pullback (x ≫ x_1).unop).obj = ↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj
have h : ∀ (x_2 : Subobject.{v, u} (Opposite.unop X)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback (x ≫ x_1).unop).obj)).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj)).toFun x_2
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A T : C
hT : IsTerminal.{v₁, u₁} T
inst_1 : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f = g
have rw : f ≫ hT.from A = g ≫ hT.from A
Tactic: rw [← cancel_mono (hT.from A)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
inst_2 : Mono.{v₁, u₁} (Y := terminal.{v₁, u₁} C) (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g
have rw : Eq (α := Z ⟶ terminal.{v₁, u₁} C) (f ≫ terminal.from A) (g ≫ terminal.from A)
Tactic: rw [← cancel_mono (terminal.from A)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
hA : IsSubterminal.{v₁, u₁} A
inst_1 : HasBinaryProduct.{v₁, u₁} A A
⊢ prod.fst ≫ diag A = 𝟙 (Limits.prod.{v₁, u₁} A A)
have rw : ∀ (hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g) [inst_2 : HasBinaryProduct.{v₁, u₁} A A],
  prod.fst ≫ diag A = 𝟙 (Limits.prod.{v₁, u₁} A A)
Tactic: rw [IsSubterminal.def] at hA
Cleared hypotheses: hA, inst_1
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
⊢ f = g
have this : Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd
Tactic: have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
this : Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd
⊢ f = g
have rw : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.fst = g
Tactic: rw [← prod.lift_fst f g, this, prod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
this : Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd
rw : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.fst = g
⊢ f = g
have rw₁ : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.snd = g
Tactic: rw [← prod.lift_fst f g, this, prod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
this : Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd
rw : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.fst = g
rw₁ : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.snd = g
⊢ f = g
have rw₂ : g = g
Tactic: rw [← prod.lift_fst f g, this, prod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subterminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)
Z : C
f g : Z ⟶ X.obj (P := Over.isMono (terminal.{v₁, u₁} C)).left
⊢ f = g
have rw : f ≫ X.arrow = g ≫ X.arrow
Tactic: rw [← cancel_mono X.arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} A C
G : Functor.{v₂, v₃, u₂, u₃} B C
x : A ⊕ B
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) x with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) x with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g) (𝟙 x) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) x with
        | inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
have inl : ∀ (val : A),
  Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) inl val with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) inl val with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := inl val) (𝟙 (inl val)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) inl val with
        | inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} A C
G : Functor.{v₂, v₃, u₂, u₃} B C
val : A
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) inl val with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) inl val with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := inl val) (𝟙 (inl val)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) inl val with
        | inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inl val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
have inl : Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) x with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) x_1 with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := inl val) (𝟙 (inl val)) =
  F.map (𝟙 val)
Tactic: simp only [← map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} A C
G : Functor.{v₂, v₃, u₂, u₃} B C
val : B
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) inr val with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) inr val with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := inr val) (𝟙 (inr val)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inr val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inr val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) inr val with
        | inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inr val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inr val with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
have inr : Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) x with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) x_1 with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := inr val) (𝟙 (inr val)) =
  G.map (𝟙 val)
Tactic: simp only [← map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : A ⊕ B
f : x ⟶ y
⊢ F.map f ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          y) =
    Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          x) ≫
      G.map f
have inl : ∀ (x y : A) (f : x ⟶ y),
  Eq (α := F.obj (obj (Sum.inl_ A B) x) ⟶ G.obj (obj (Sum.inl_ A B) y))
    (F.map (map (Sum.inl_ A B) f) ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inl_ A B) y)))
    (Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inl_ A B) x)) ≫
      G.map (map (Sum.inl_ A B) f))
Tactic: cases f
Cleared hypotheses: x, y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : A ⊕ B
f : x ⟶ y
inl :
  ∀ (x y : A) (f : x ⟶ y),
    Eq (α := F.obj (obj (Sum.inl_ A B) x) ⟶ G.obj (obj (Sum.inl_ A B) y))
      (F.map (map (Sum.inl_ A B) f) ≫
        Iso.hom
          ((fun (x : A ⊕ B) ↦
              (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
                | Sum.inl x => e₁.app x
                | inr x => e₂.app x :
                F.obj x ≅ G.obj x))
            (obj (Sum.inl_ A B) y)))
      (Iso.hom
          ((fun (x : A ⊕ B) ↦
              (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
                | Sum.inl x => e₁.app x
                | inr x => e₂.app x :
                F.obj x ≅ G.obj x))
            (obj (Sum.inl_ A B) x)) ≫
        G.map (map (Sum.inl_ A B) f))
⊢ F.map f ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | Sum.inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          y) =
    Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | Sum.inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          x) ≫
      G.map f
have inr : ∀ (x y : B) (f : x ⟶ y),
  Eq (α := F.obj (obj (Sum.inr_ A B) x) ⟶ G.obj (obj (Sum.inr_ A B) y))
    (F.map (map (Sum.inr_ A B) f) ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | Sum.inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inr_ A B) y)))
    (Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | Sum.inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inr_ A B) x)) ≫
      G.map (map (Sum.inr_ A B) f))
Tactic: cases f
Cleared hypotheses: x, y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ B
f : X ⟶ Y
⊢ Eq (α := (F.sum' H).obj X ⟶ (G.sum' I).obj Y)
    ((F.sum' H).map f ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) Y with
      | inl X => α.app X
      | inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) X with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map f)
have inl : ∀ (x y : A) (f : x ⟶ y),
  Eq (α := (F.sum' H).obj (obj (Sum.inl_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inl_ A B) y))
    ((F.sum' H).map (map (Sum.inl_ A B) f) ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) y with
      | inl X => α.app X
      | inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) x with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map (map (Sum.inl_ A B) f))
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ B
f : X ⟶ Y
inl :
  ∀ (x y : A) (f : x ⟶ y),
    Eq (α := (F.sum' H).obj (obj (Sum.inl_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inl_ A B) y))
      ((F.sum' H).map (map (Sum.inl_ A B) f) ≫
        match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) y with
        | Sum.inl X => α.app X
        | inr X => β.app X)
      ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) x with
        | Sum.inl X => α.app X
        | inr X => β.app X) ≫
        (G.sum' I).map (map (Sum.inl_ A B) f))
⊢ Eq (α := (F.sum' H).obj X ⟶ (G.sum' I).obj Y)
    ((F.sum' H).map f ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) Y with
      | Sum.inl X => α.app X
      | inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) X with
      | Sum.inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map f)
have inr : ∀ (x y : B) (f : x ⟶ y),
  Eq (α := (F.sum' H).obj (obj (Sum.inr_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inr_ A B) y))
    ((F.sum' H).map (map (Sum.inr_ A B) f) ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inr_ A B) y with
      | Sum.inl X => α.app X
      | inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inr_ A B) x with
      | Sum.inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map (map (Sum.inr_ A B) f))
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ C
f : X ⟶ Y
⊢ Eq (α := (F.sum H).obj X ⟶ (G.sum I).obj Y)
    ((F.sum H).map f ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) Y with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) X with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map f)
have inl : ∀ (x y : A) (f : x ⟶ y),
  Eq (α := (F.sum H).obj (obj (Sum.inl_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inl_ A C) y))
    ((F.sum H).map (map (Sum.inl_ A C) f) ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) y with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) x with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map (map (Sum.inl_ A C) f))
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ C
f : X ⟶ Y
inl :
  ∀ (x y : A) (f : x ⟶ y),
    Eq (α := (F.sum H).obj (obj (Sum.inl_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inl_ A C) y))
      ((F.sum H).map (map (Sum.inl_ A C) f) ≫
        match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) y with
        | Sum.inl X => map (Sum.inl_ B D) (α.app X)
        | inr X => map (Sum.inr_ B D) (β.app X))
      ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) x with
        | Sum.inl X => map (Sum.inl_ B D) (α.app X)
        | inr X => map (Sum.inr_ B D) (β.app X)) ≫
        (G.sum I).map (map (Sum.inl_ A C) f))
⊢ Eq (α := (F.sum H).obj X ⟶ (G.sum I).obj Y)
    ((F.sum H).map f ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) Y with
      | Sum.inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) X with
      | Sum.inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map f)
have inr : ∀ (x y : C) (f : x ⟶ y),
  Eq (α := (F.sum H).obj (obj (Sum.inr_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inr_ A C) y))
    ((F.sum H).map (map (Sum.inr_ A C) f) ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inr_ A C) y with
      | Sum.inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inr_ A C) x with
      | Sum.inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map (map (Sum.inr_ A C) f))
Tactic: cases f
Cleared hypotheses: X, Y, f