awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
  (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
  (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E))
    (π ((E ⋙ F) ⋙ G) j))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w₁ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
  (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
  (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E))
    (π ((E ⋙ F) ⋙ G) j))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₁ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w₂ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
  (G.map (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) j)))
  (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E))
    (π ((E ⋙ F) ⋙ G) j))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₁ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₂ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (G.map (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w₃ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
  (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E))
    (π ((E ⋙ F) ⋙ G) j))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₁ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₂ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (G.map (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₃ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w₄ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
  (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (pre (F ⋙ G) E) (π ((E ⋙ F) ⋙ G) j)))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₁ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₂ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (G.map (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₃ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₄ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G)
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (pre (F ⋙ G) E) (π ((E ⋙ F) ⋙ G) j)))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w₅ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
  (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (π (F ⋙ G) (E.obj j)))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₁ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₂ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (G.map (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₃ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₄ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G)
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (pre (F ⋙ G) E) (π ((E ⋙ F) ⋙ G) j)))
w₅ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (π (F ⋙ G) (E.obj j)))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
have w₆ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j))) (G.map (π F (E.obj j)))
Tactic: erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₂, v₁, u₂, u₁} K J
inst_3 : HasLimit (e.functor ⋙ F)
⊢ HasLimit F
have this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
Tactic: haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₁, v, u₁, u} J C
⊢ limMap (𝟙 F) = 𝟙 (limit F)
have w : ∀ (j : J), CategoryStruct.comp (Y := limit F) (limMap (𝟙 F)) (limit.π F j) = 𝟙 (limit F) ≫ limit.π F j
Tactic: apply Limits.limit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
X Y Z : Functor.{v₁, v, u₁, u} J C
α : X ⟶ Y
β : Y ⟶ Z
⊢ Eq (α := limit X ⟶ limit Z) (limMap (α ≫ β)) (CategoryStruct.comp (Y := limit Y) (limMap α) (limMap β))
have w : ∀ (j : J),
  Eq (α := limit X ⟶ Z.obj j) (CategoryStruct.comp (Y := limit Z) (limMap (α ≫ β)) (limit.π Z j))
    (CategoryStruct.comp (Y := limit Z) (CategoryStruct.comp (Y := limit Y) (limMap α) (limMap β)) (limit.π Z j))
Tactic: apply Limits.limit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasLimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
⊢ Eq (α := obj lim F ⟶ limit (E ⋙ G)) (map lim α ≫ pre G E)
    (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (map lim (E.whiskerLeft α)))
have w : ∀ (j : K),
  Eq (α := obj lim F ⟶ (E ⋙ G).obj j) (CategoryStruct.comp (Y := limit (E ⋙ G)) (map lim α ≫ pre G E) (π (E ⋙ G) j))
    (CategoryStruct.comp (Y := limit (E ⋙ G))
      (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (map lim (E.whiskerLeft α))) (π (E ⋙ G) j))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasLimitsOfShape.{v₂, u₂, v, u} K C
F : Functor.{v₁, v, u₁, u} J C
E₁ E₂ : Functor.{v₂, v₁, u₂, u₁} K J
α : E₁ ⟶ E₂
⊢ Eq (α := limit F ⟶ limit (E₂ ⋙ F)) (pre F E₂)
    (CategoryStruct.comp (Y := limit (E₁ ⋙ F)) (pre F E₁) (map lim (whiskerRight α F)))
have w : ∀ (j : K),
  Eq (α := limit F ⟶ (E₂ ⋙ F).obj j) (CategoryStruct.comp (Y := limit (E₂ ⋙ F)) (pre F E₂) (π (E₂ ⋙ F) j))
    (CategoryStruct.comp (Y := limit (E₂ ⋙ F))
      (CategoryStruct.comp (Y := limit (E₁ ⋙ F)) (pre F E₁) (map lim (whiskerRight α F))) (π (E₂ ⋙ F) j))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : HasLimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
⊢ Eq (α := H.obj (limit F) ⟶ limit (G ⋙ H)) (CategoryStruct.comp (Y := H.obj (limit G)) (H.map (limMap α)) (post G H))
    (CategoryStruct.comp (Y := limit (F ⋙ H)) (post F H) (limMap (whiskerRight α H)))
have w : ∀ (j : J),
  Eq (α := H.obj (limit F) ⟶ (G ⋙ H).obj j)
    (CategoryStruct.comp (Y := limit (G ⋙ H)) (CategoryStruct.comp (Y := H.obj (limit G)) (H.map (limMap α)) (post G H))
      (π (G ⋙ H) j))
    (CategoryStruct.comp (Y := limit (G ⋙ H))
      (CategoryStruct.comp (Y := limit (F ⋙ H)) (post F H) (limMap (whiskerRight α H))) (π (G ⋙ H) j))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j
have eq : (map (L ⋙ const J) s.π ≫ adj.counit.app F).app j =
  (adj.counit.app (obj (const J) s.pt) ≫ map (𝟭 (Functor.{v₁, v, u₁, u} J C)) s.π).app j
Tactic: have eq := NatTrans.congr_app (adj.counit.naturality s.π) j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq :
  (map (L ⋙ const J) s.π ≫ adj.counit.app F).app j =
    (adj.counit.app (obj (const J) s.pt) ≫ map (𝟭 (Functor.{v₁, v, u₁, u} J C)) s.π).app j
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j
have eq' : Eq (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ obj.{v₁, v, u₁, u} (obj (const J) s.pt) j)
  (NatTrans.app (map (const J) (adj.unit.app s.pt) ≫ adj.counit.app (obj (const J) s.pt)) j)
  (NatTrans.app (𝟙 (obj (const J) s.pt)) j)
Tactic: have eq' := NatTrans.congr_app (adj.left_triangle_components s.pt) j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq :
  (map (L ⋙ const J) s.π ≫ adj.counit.app F).app j =
    (adj.counit.app (obj (const J) s.pt) ≫ map (𝟭 (Functor.{v₁, v, u₁, u} J C)) s.π).app j
eq' :
  Eq (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ obj.{v₁, v, u₁, u} (obj (const J) s.pt) j)
    (NatTrans.app (map (const J) (adj.unit.app s.pt) ≫ adj.counit.app (obj (const J) s.pt)) j)
    (NatTrans.app (𝟙 (obj (const J) s.pt)) j)
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j
have dsimp : (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j
Tactic: dsimp at eq eq' ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j = 𝟙 s.pt
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j
have rw : (adj.unit.app s.pt ≫ L.map s.π) ≫ (adj.counit.app F).app j = s.π.app j
Tactic: rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j = 𝟙 s.pt
rw : (adj.unit.app s.pt ≫ L.map s.π) ≫ (adj.counit.app F).app j = s.π.app j
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j
have rw₁ : adj.unit.app s.pt ≫ L.map s.π ≫ (adj.counit.app F).app j = s.π.app j
Tactic: rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j = 𝟙 s.pt
rw : (adj.unit.app s.pt ≫ L.map s.π) ≫ (adj.counit.app F).app j = s.π.app j
rw₁ : adj.unit.app s.pt ≫ L.map s.π ≫ (adj.counit.app F).app j = s.π.app j
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j
have rw₂ : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j = s.π.app j
Tactic: rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']