awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
have pos : ∀ (h : j' ≤ j),
  ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) sorry
Tactic: by_cases! h : j' ≤ j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
pos :
  ∀ (h : j' ≤ j),
    ∃ (j₁ : (↑(Set.Iio m) : Type w)),
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
        Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
have neg : ∀ (h : j < j'),
  ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) sorry
Tactic: by_cases! h : j' ≤ j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
have pos : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j sorry ∈ Set.Iio m
Tactic: refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
⊢ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯ ∈ Set.Iio m
have pos : ∀ (h' : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j sorry ∉ Set.Iio m), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
h' : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯ ∉ Set.Iio m
⊢ False
have h'₁ : m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j sorry
Tactic: simp only [Set.mem_Iio, not_lt] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
h' : m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯
⊢ False
have pos : IsMin m
Tactic: apply hm.1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
⊢ IsColimit.{w, v, w, u} (J := (↑(Set.Iio m) : Type w)) (C := C) (F :=
    comp (D := { x : J // x ∈ Set.Ici j })
      (Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s :=
              fun (x1 x2 : { x : J // x ∈ Set.Ici j }) ↦ x1 < x2) (Set.principalSegIio m)) :
          (a : (↑(Set.Iio m) : Type w)) → { x : J // x ∈ Set.Ici j }))
        ⋯)
      (Monotone.functor ⋯ ⋙ F))
    (PrincipalSeg.cocone (Set.principalSegIio m) (Monotone.functor ⋯ ⋙ F))
have this : hf.functor.Final
Tactic: have : hf.functor.Final := by
      rw [Monotone.final_functor_iff]
      rintro ⟨j', hj'⟩
      push _ ∈ _ at hj'
      dsimp only [f]
      by_cases! h : j' ≤ j
      · refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
        by_contra h'
        simp only [Set.mem_Iio, not_lt] at h'
        apply hm.1
        rintro ⟨k, hk⟩ hkm
        exact h'.trans hk
      · exact ⟨⟨⟨j', h.le⟩, hj'⟩, by rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
inst_1 : HasCoproduct.{w₂, v, u} f
e : β ≃ α
iso : (j : β) → g j ≅ f ((e : (a : β) → α) j)
⊢ HasCoproduct.{w, v, u} g
have have : ∀
  (α :
    Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
      ((Discrete.equivalence e).functor ⋙ Discrete.functor f)),
  HasCoproduct.{w, v, u} g
Tactic: have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
inst_1 : HasProduct.{w₂, v, u} f
e : β ≃ α
iso : (j : β) → g j ≅ f ((e : (a : β) → α) j)
⊢ HasProduct.{w, v, u} g
have have : ∀
  (α :
    Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
      ((Discrete.equivalence e).functor ⋙ Discrete.functor f)),
  HasProduct.{w, v, u} g
Tactic: have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
f : J → C
inst_1 : HasCoproduct.{u_1, v, u} f
j j' : J
w : j = j'
⊢ Eq.{v + 1} (α := f j ⟶ sigmaObj.{u_1, v, u} f) (eqToHom ⋯ ≫ ι f j') (ι f j)
have refl : Eq.{v + 1} (α := f j ⟶ sigmaObj.{u_1, v, u} f) (eqToHom sorry ≫ ι f j) (ι f j)
Tactic: cases w
Cleared hypotheses: j', w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
⊢ IsIso.{v, u} (C := C) (X := sigmaObj.{w, v, u} f) (Y := sigmaObj.{w, v, u} f) (Sigma.desc fun (a : β) ↦ Sigma.ι f a)
have h : (Sigma.desc fun (a : β) ↦ Sigma.ι f a) = 𝟙 (sigmaObj.{w, v, u} f)
Tactic: convert! IsIso.id _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
⊢ (Sigma.desc fun (a : β) ↦ Sigma.ι f a) = 𝟙 (sigmaObj.{w, v, u} f)
have h : ∀ (b : β),
  CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (Sigma.ι f b) (Sigma.desc fun (a : β) ↦ Sigma.ι f a) =
    Sigma.ι f b ≫ 𝟙 (sigmaObj.{w, v, u} f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ IsColimit (J := Discrete ((a : α) × β a)) (F :=
    Discrete.functor fun (x : (a : α) × β a) ↦
      match (motive := (a : α) × β a → C) x with
      | ⟨a, b⟩ => Y a b)
    (mk c.pt fun (x : (a : α) × β a) ↦
      match (motive :=
        (x : (a : α) × β a) →
          (fun (x : (a : α) × β a) ↦
                (match (motive := (a : α) × β a → C) x with
                  | ⟨a, b⟩ => Y a b :
                  C))
              x ⟶
            c.pt)
        x with
      | ⟨a, b⟩ => π a b ≫ c.inj a)
have refine_1 : (t :
    Cofan (C := C) fun (x : (a : α) × β a) ↦
      match (motive := (a : α) × β a → C) x with
      | ⟨a, b⟩ => Y a b) →
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
Tactic: refine Cofan.IsColimit.mk _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
refine_1 :
  (t :
      Cofan (C := C) fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b) →
    Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
        Discrete.functor fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
        (mk c.pt fun (x : (a : α) × β a) ↦
          match (motive :=
            (x : (a : α) × β a) →
              (fun (x : (a : α) × β a) ↦
                    (match (motive := (a : α) × β a → C) x with
                      | ⟨a, b⟩ => Y a b :
                      C))
                  x ⟶
                c.pt)
            x with
          | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
      t.pt
⊢ IsColimit (J := Discrete ((a : α) × β a)) (F :=
    Discrete.functor fun (x : (a : α) × β a) ↦
      match (motive := (a : α) × β a → C) x with
      | ⟨a, b⟩ => Y a b)
    (mk c.pt fun (x : (a : α) × β a) ↦
      match (motive :=
        (x : (a : α) × β a) →
          (fun (x : (a : α) × β a) ↦
                (match (motive := (a : α) × β a → C) x with
                  | ⟨a, b⟩ => Y a b :
                  C))
              x ⟶
            c.pt)
        x with
      | ⟨a, b⟩ => π a b ≫ c.inj a)
have refine_2 : ∀
  (t :
    Cofan (C := C) fun (x : (a : α) × β a) ↦
      match (motive := (a : α) × β a → C) x with
      | ⟨a, b⟩ => Y a b)
  (j : (a : α) × β a),
  CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
        Discrete.functor fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
        (mk c.pt fun (x : (a : α) × β a) ↦
          match (motive :=
            (x : (a : α) × β a) →
              (fun (x : (a : α) × β a) ↦
                    (match (motive := (a : α) × β a → C) x with
                      | ⟨a, b⟩ => Y a b :
                      C))
                  x ⟶
                c.pt)
            x with
          | ⟨a, b⟩ => π a b ≫ c.inj a))
      (inj (f := fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
        (mk c.pt fun (x : (a : α) × β a) ↦
          match (motive :=
            (x : (a : α) × β a) →
              (fun (x : (a : α) × β a) ↦
                    (match (motive := (a : α) × β a → C) x with
                      | ⟨a, b⟩ => Y a b :
                      C))
                  x ⟶
                c.pt)
            x with
          | ⟨a, b⟩ => π a b ≫ c.inj a)
        j)
      (hc.desc
        (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))) =
    t.inj j
Tactic: refine Cofan.IsColimit.mk _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ Eq.{v + 1} (α :=
    (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
      | ⟨a, b⟩ => Y a b) ⟶
      t.pt)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
          Discrete.functor fun (x : (a : α) × β a) ↦
            match (motive := (a : α) × β a → C) x with
            | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a))
        (inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          (Sigma.mk (β := fun (a : α) ↦ β a) a b))
        (hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))) :
      (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
        | ⟨a, b⟩ => Y a b) ⟶
        t.pt)
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
      (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
        | ⟨a, b⟩ => Y a b) ⟶
        t.pt)
have refine_2 : Eq (α := Y a b ⟶ t.pt)
  (π a b ≫
      c.inj a ≫
        hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))) :
    Y a b ⟶ t.pt)
  (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
    Y ((Sigma.mk (β := fun (a : α) ↦ β a) a b).fst (β := fun (a : α) ↦ β a))
        ((Sigma.mk (β := fun (a : α) ↦ β a) a b).snd (β := fun (a : α) ↦ β a)) ⟶
      t.pt)
Tactic: simp only [mk_pt, cofan_mk_inj, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ Eq (α := Y a b ⟶ t.pt)
    (π a b ≫
        c.inj a ≫
          hc.desc
            (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))) :
      Y a b ⟶ t.pt)
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
      Y ((Sigma.mk (β := fun (a : α) ↦ β a) a b).fst (β := fun (a : α) ↦ β a))
          ((Sigma.mk (β := fun (a : α) ↦ β a) a b).snd (β := fun (a : α) ↦ β a)) ⟶
        t.pt)
have refine_2 : Eq.{v + 1} (α := Y a b ⟶ t.pt)
  (NatTrans.app
      (Cocone.ι (mk t.pt fun (b : β { as := a }.as) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a }.as b)))
      { as := b } :
    Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶
      Functor.obj.{u_1, v, u_1, u}
        (Functor.obj (Functor.const (Discrete (β a)))
          (Cocone.pt.{u_1, v, u_1, u} (J := Discrete (β a)) (F := Discrete.functor (Y a))
            (mk t.pt fun (b : β { as := a : Discrete α }.as) ↦
              t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a : Discrete α }.as b))))
        { as := b : Discrete (β a) })
  (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))
Tactic: erw [hc.fac, (hs a).fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
m :
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j ≫
        m =
      t.inj j
⊢ m = hc.desc (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))
have refine_3 : ∀ (x : Discrete α) (a : α) (x : Discrete (β a)) (b : β a),
  Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫
      c.ι.app { as := a : Discrete α } ≫
        hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))))
Tactic: refine hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
m :
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j ≫
        m =
      t.inj j
x : Discrete α
a : α
x_1 : Discrete (β a)
b : β a
⊢ Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫
      c.ι.app { as := a : Discrete α } ≫
        hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))))
have refine_3 : Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
  ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
  (NatTrans.app
    (Cocone.ι (mk t.pt fun (b : β { as := a }.as) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a }.as b)))
    { as := b })
Tactic: erw [hc.fac, (hs a).fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasProduct.{w₂, v, u} f
⊢ (map fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (piObj.{w₂, v, u} f)
have h : ∀ (b : α),
  CategoryStruct.comp (Y := piObj.{w₂, v, u} f) (map fun (a : α) ↦ 𝟙 (f a)) (π f b) = 𝟙 (piObj.{w₂, v, u} f) ≫ π f b
Tactic: ext