awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
j : J
⊢ Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }) :
          (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
            DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
          x) :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }) :
          (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
            DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
          y) :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
have a : Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
  ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
        (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
      x :
    DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
  ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
        (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
      y :
    DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
Tactic: rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, piComparison_comp_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
h : Nonempty (IsInitial.{v, u} X)
⊢ IsEmpty.{w + 1} (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X)
have rw : Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
Tactic: rw [← Types.initial_iff_empty]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
inst_4 : ReflectsColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
⊢ Nonempty (IsInitial.{v, u} X) ↔ IsEmpty.{w + 1} (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X)
have rw : Nonempty (IsInitial.{v, u} X) ↔ Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
Tactic: rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
inst_4 : ReflectsColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
rw : Nonempty (IsInitial.{v, u} X) ↔ Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
⊢ Nonempty (IsInitial.{v, u} X) ↔ IsEmpty.{w + 1} (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X)
have rw₁ : Nonempty.{w + 2} (IsInitial (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)) ↔
  Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
Tactic: rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂
⊢ (hom (FC := FC) (CC := CC) prod.fst : (a : CC (X₁ ⨯ X₂)) → CC X₁)
      ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂)) x :
        ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) =
    x.1
have obtain : ∀ (y : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)),
  Eq (α := CC X₁)
    ((hom (FC := FC) (CC := CC) prod.fst : (a : CC (X₁ ⨯ X₂)) → CC X₁)
        ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂))
            ((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y :
              ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂) :
          ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) :
      CC X₁)
    (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y).1 :
      ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁)
Tactic: obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂
⊢ (hom (FC := FC) (CC := CC) prod.snd : (a : CC (X₁ ⨯ X₂)) → CC X₂)
      ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂)) x :
        ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) =
    x.2
have obtain : ∀ (y : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)),
  Eq (α := CC X₂)
    ((hom (FC := FC) (CC := CC) prod.snd : (a : CC (X₁ ⨯ X₂)) → CC X₂)
        ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂))
            ((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y :
              ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂) :
          ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) :
      CC X₂)
    (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y).2 :
      ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂)
Tactic: obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst_3 : HasPullback f₁ f₂
inst_4 : PreservesLimit (cospan f₁ f₂) (forget C (FC := FC) (CC := CC))
x : ToType (FC := FC) (CC := CC) (pullback f₁ f₂)
⊢ ∃ (x₁ : ToType (FC := FC) (CC := CC) X₁) (x₂ : ToType (FC := FC) (CC := CC) X₂) (h :
    Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁ : CC S)
      ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂ : CC S)),
    x = pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁ x₂ h
have obtain : ∀ (x₁ : ToType (FC := FC) (CC := CC) X₁) (x₂ : ToType (FC := FC) (CC := CC) X₂)
  (h :
    Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) (x₁, x₂).1 : CC S)
      ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) (x₁, x₂).2 : CC S)),
  ∃ (x₁_1 : ToType (FC := FC) (CC := CC) X₁) (x₂_1 : ToType (FC := FC) (CC := CC) X₂) (h_1 :
    Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁_1 : CC S)
      ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂_1 : CC S)),
    Eq (α := ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
      ((Equiv.symm (pullbackEquiv (FC := FC) (CC := CC) f₁ f₂) :
            (a :
                { p : ToType X₁ × ToType X₂ //
                  (hom f₁ : (a : CC X₁) → CC S) p.1 = (hom f₂ : (a : CC X₂) → CC S) p.2 }) →
              ToType (pullback f₁ f₂))
          (Subtype.mk (p := fun (p : ToType (FC := FC) (CC := CC) X₁ × ToType (FC := FC) (CC := CC) X₂) ↦
            Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) p.1 : CC S)
              ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) p.2 : CC S))
            (x₁, x₂) h) :
        ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
      (pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁_1 x₂_1 h_1 : ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
Tactic: obtain ⟨⟨⟨x₁, x₂⟩, h⟩, rfl⟩ := (pullbackEquiv f₁ f₂).symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst_3 : HasWidePullback B X f
inst_4 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h₀ :
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
⊢ x = y
have a : ∀ (j : WidePullbackShape ι),
  Eq (α := CC ((wideCospan B X f).obj j))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) j) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj j))
        x :
      CC ((wideCospan B X f).obj j))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) j) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj j))
        y :
      CC ((wideCospan B X f).obj j))
Tactic: apply Concrete.limit_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
inst_3 : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst_4 : HasWidePullback B X f
inst_5 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
⊢ x = y
have apply : Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
  ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
Tactic: apply Concrete.widePullback_ext _ _ _ _ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
inst_3 : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst_4 : HasWidePullback B X f
inst_5 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
⊢ Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
have inhabit : ∀ (inhabited_h : Inhabited ι),
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_3 : HasMultiequalizer I
inst_4 : PreservesLimit I.multicospan (forget C (FC := FC) (CC := CC))
x y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
h :
  ∀ (t : J.L),
    Eq (α := CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) x :
        CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) y :
        CC (I.left t))
⊢ x = y
have a : ∀ (j : WalkingMulticospan J),
  Eq (α := CC (I.multicospan.obj j))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan j) : (a : CC (limit I.multicospan)) → CC (I.multicospan.obj j))
        x :
      CC (I.multicospan.obj j))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan j) : (a : CC (limit I.multicospan)) → CC (I.multicospan.obj j))
        y :
      CC (I.multicospan.obj j))
Tactic: apply Concrete.limit_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_3 : HasMultiequalizer I
inst_4 : PreservesLimit I.multicospan (forget C (FC := FC) (CC := CC))
x y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
h :
  ∀ (t : J.L),
    Eq (α := CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) x :
        CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) y :
        CC (I.left t))
b : J.R
⊢ Eq (α := CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.right b)) :
          (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.right b)))
        x :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.right b)) :
          (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.right b)))
        y :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))
have a : Eq (α := CC (I.multicospan.obj (WalkingMulticospan.right b)))
  ((hom (FC := FC) (CC := CC) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
        (a : CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
          CC (I.multicospan.obj (WalkingMulticospan.right b)))
      ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left (J.fst b))) :
            (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b))))
          x :
        CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) :
    CC (I.multicospan.obj (WalkingMulticospan.right b)))
  ((hom (FC := FC) (CC := CC) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
        (a : CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
          CC (I.multicospan.obj (WalkingMulticospan.right b)))
      ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left (J.fst b))) :
            (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b))))
          y :
        CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) :
    CC (I.multicospan.obj (WalkingMulticospan.right b)))
Tactic: rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), ConcreteCategory.comp_apply,
      ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))
i : J.R
⊢ Eq.{s + 1} (α := CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.fst i)) :
      CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.snd i)) :
      CC (I.right i))
have a : (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
      (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
        (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
    ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) =
  (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
Tactic: have a := x.2 (WalkingMulticospan.Hom.fst i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))
i : J.R
a :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
⊢ Eq.{s + 1} (α := CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.fst i)) :
      CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.snd i)) :
      CC (I.right i))
have b : (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
      (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
        (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
    ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) =
  (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
Tactic: have b := x.2 (WalkingMulticospan.Hom.snd i)