awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ConeMorphism.hom (Iso.hom (liftedLimitMapsToOriginal t)) ≫ c.π.app j = F.map ((liftLimit t).π.app j)
have rw : ConeMorphism.hom (Iso.hom (liftedLimitMapsToOriginal t)) ≫
    ConeMorphism.hom (Iso.inv (liftedLimitMapsToOriginal t)) ≫ F.map ((liftLimit t).π.app j) =
  F.map ((liftLimit t).π.app j)
Tactic: rw [← liftedLimitMapsToOriginal_inv_map_π (t := t)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
⊢ IsLimit d
have this : (Cone.functoriality K F).map f = i.inv
Tactic: have : (Cone.functoriality K F).map f = i.inv :=
          (hd.ofIsoLimit i.symm).uniq_cone_morphism
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso ((Cone.functoriality K F).map f)
have rw : IsIso i.inv
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsLimit d
have this₁ : IsIso ((Cone.functoriality K F).map f)
Tactic: haveI : IsIso ((Cone.functoriality K F).map f) := by
          rw [this]
          infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this_1 : (Cone.functoriality K F).map f = i.inv
this : IsIso ((Cone.functoriality K F).map f)
⊢ IsLimit d
have this₁ : IsIso f
Tactic: haveI : IsIso f := isIso_of_reflects_iso f (Cone.functoriality K F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
⊢ IsColimit d
have this : (Cocone.functoriality K F).map f = i.hom
Tactic: have : (Cocone.functoriality K F).map f = i.hom :=
          (hd.ofIsoColimit i.symm).uniq_cocone_morphism
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)
have rw : IsIso i.hom
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsColimit d
have this₁ : IsIso ((Cocone.functoriality K F).map f)
Tactic: haveI : IsIso ((Cocone.functoriality K F).map f) := by
          rw [this]
          infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this_1 : (Cocone.functoriality K F).map f = i.hom
this : IsIso ((Cocone.functoriality K F).map f)
⊢ IsColimit d
have this₁ : IsIso f
Tactic: haveI := isIso_of_reflects_iso f (Cocone.functoriality K F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm :
      (a : IsLimit c) → IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c))
    t
j : J
⊢ ((Cone.postcompose (isoWhiskerRight h F).hom).obj ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).π.app j =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose (isoWhiskerRight h F).hom).obj ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).pt) ≫
      c.π.app j
have dsimp : (c.π.app j ≫ F.map (h.inv.app j)) ≫ F.map (h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm :
      (a : IsLimit c) → IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c))
    t
j : J
⊢ (c.π.app j ≫ F.map (h.inv.app j)) ≫ F.map (h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
have rw : c.π.app j ≫ F.map (h.inv.app j ≫ h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
Tactic: rw [Category.assoc, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ G.mapCone
      (liftLimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
        (((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsLimit c) → IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c))
          t)) ≅
    c
have refine : IsLimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
  (F.mapCone
    (liftLimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
      (((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm :
          (a : IsLimit c) → IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c))
        t)))
Tactic: refine (IsLimit.mapConeEquiv h ?_).uniqueUpToIso t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
    (F.mapCone
      (liftLimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
        (((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsLimit c) → IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c))
          t)))
have apply : IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
Tactic: apply IsLimit.ofIsoLimit _ (liftedLimitMapsToOriginal _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cone (K ⋙ F)
hc : IsLimit c
⊢ LiftableCone K F c
have refine : F.mapCone (obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftLimit (hc.whiskerEquivalence e))) ≅ c
Tactic: refine ⟨(Cone.whiskeringEquivalence e).inverse.obj
          (liftLimit (hc.whiskerEquivalence e)), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cone (K ⋙ F)
hc : IsLimit c
inner : obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (F.mapCone (liftLimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (Cone.whisker e.functor c) :=
  mapIso (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftedLimitMapsToOriginal (hc.whiskerEquivalence e))
⊢ F.mapCone (obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftLimit (hc.whiskerEquivalence e))) ≅ c
have refine : F.mapCone (obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftLimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (F.mapCone (liftLimit (hc.whiskerEquivalence e)))
Tactic: refine ?_ ≪≫ inner ≪≫ ((Cone.whiskeringEquivalence e).unitIso.app c).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm :
      (a : IsColimit c) → IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c))
    t
j : J
⊢ ((Cocone.precompose (isoWhiskerRight h F).inv).obj ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).ι.app j ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (isoWhiskerRight h F).inv).obj
              ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).pt) =
    c.ι.app j
have dsimp : (F.map (h.inv.app j) ≫ F.map (h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm :
      (a : IsColimit c) → IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c))
    t
j : J
⊢ (F.map (h.inv.app j) ≫ F.map (h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
have rw : (F.map (h.inv.app j ≫ h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
Tactic: rw [← F.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ G.mapCocone
      (liftColimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)
        (((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsColimit c) → IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c))
          t)) ≅
    c
have refine : IsColimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
  (F.mapCocone
    (liftColimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)
      (((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm :
          (a : IsColimit c) → IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c))
        t)))
Tactic: refine (IsColimit.mapCoconeEquiv h ?_).uniqueUpToIso t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
    (F.mapCocone
      (liftColimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)
        (((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsColimit c) → IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c))
          t)))
have apply : IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)
Tactic: apply IsColimit.ofIsoColimit _ (liftedColimitMapsToOriginal _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cocone (K ⋙ F)
hc : IsColimit c
inner : obj (Equivalence.inverse (Cocone.whiskeringEquivalence e))
    (F.mapCocone (liftColimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (Cocone.whisker e.functor c) :=
  mapIso (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftedColimitMapsToOriginal (hc.whiskerEquivalence e))
⊢ F.mapCocone (obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftColimit (hc.whiskerEquivalence e))) ≅ c
have refine : F.mapCocone (obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftColimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (F.mapCocone (liftColimit (hc.whiskerEquivalence e)))
Tactic: refine ?_ ≪≫ inner ≪≫ ((Cocone.whiskeringEquivalence e).unitIso.app c).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
⊢ Eq (α := A.obj (limit (F ⋙ π A)))
    ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
          (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
        (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
      A.obj (limit (F ⋙ π A)))
    (liftedConeElement F : A.obj (limit (F ⋙ π A)))
have a : Eq (α := limit ((F ⋙ π A) ⋙ A))
  (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
        (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
      ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
            (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
          (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
        A.obj (limit (F ⋙ π A))) :
    limit ((F ⋙ π A) ⋙ A))
  (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
        (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
      (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
    limit ((F ⋙ π A) ⋙ A))
Tactic: apply (preservesLimitIso A (F ⋙ π A)).toEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
⊢ Eq (α := limit ((F ⋙ π A) ⋙ A))
    (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
          (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
        ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          A.obj (limit (F ⋙ π A))) :
      limit ((F ⋙ π A) ⋙ A))
    (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
          (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
        (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
      limit ((F ⋙ π A) ⋙ A))
have a : ∀ (i : I),
  Eq (α := (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
          (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
        (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
              (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
            ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
                  (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
                (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
              A.obj (limit (F ⋙ π A))) :
          limit ((F ⋙ π A) ⋙ A)) :
      (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
          (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
        (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
              (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
            (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
          limit ((F ⋙ π A) ⋙ A)) :
      (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Elements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
i : I
⊢ Eq (α := (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
          (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
        (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
              (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
            ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
                  (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
                (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
              A.obj (limit (F ⋙ π A))) :
          limit ((F ⋙ π A) ⋙ A)) :
      (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
          (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
        (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
              (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
            (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
          limit ((F ⋙ π A) ⋙ A)) :
      (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
have h₁ : Eq (α := ((F ⋙ π A) ⋙ A).obj i)
  ((hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := limit ((F ⋙ π A) ⋙ A))
            (Iso.hom (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ⟶ limit ((F ⋙ π A) ⋙ A))
            (limit.π ((F ⋙ π A) ⋙ A) i : limit ((F ⋙ π A) ⋙ A) ⟶ ((F ⋙ π A) ⋙ A).obj i)) :
        (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
      ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
            (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
              (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
          (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
        (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
    ((F ⋙ π A) ⋙ A).obj i)
  ((hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) : (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
      ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
            (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
              (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
          (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
        (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
    ((F ⋙ π A) ⋙ A).obj i)
Tactic: have h₁ := congr_hom (preservesLimitIso_hom_π A (F ⋙ π A) i)
    (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)