awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          (x i) :
        P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          (x j) :
        P.obj (Opposite.op (F.obj (pullback (f i) (f j))))) ↔
    Eq (α := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          (x i) :
        P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          (x j) :
        P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
have this₁ : Function.Bijective (α := (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) (β :=
  (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
    (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) →
      (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
Tactic: have : Function.Bijective (P.map (pullbackComparison F (f i) (f j)).op) := by
    rw [← isIso_iff_bijective]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : GrothendieckTopology.{u_2, u_3} C
S : C
R : Sieve.{u_2, u_3} S
⊢ R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
have rw : Sieve.generate R.arrows ∈ (J : (a : C) → Set (Sieve a)) S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
Tactic: rw [mem_toPrecoverage_iff, Sieve.generate_sieve]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : GrothendieckTopology.{u_2, u_3} C
S : C
R : Sieve.{u_2, u_3} S
rw : Sieve.generate R.arrows ∈ (J : (a : C) → Set (Sieve a)) S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
have rw₁ : R ∈ (J : (a : C) → Set (Sieve a)) S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
Tactic: rw [mem_toPrecoverage_iff, Sieve.generate_sieve]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{u_2, u_3} C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{u_2, u_3} (X i))) (J.toPrecoverage.coverings (X i))
      (Presieve.ofArrows (Y i) (g i))
⊢ (Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (x : (i : ι) × σ i) ↦
      g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i))) ∈
    J.toPrecoverage.coverings S
have rw : Sieve.generate (Presieve.bindOfArrows X f fun (i : ι) ↦ Presieve.ofArrows (Y i) (g i)) ∈ (J : (a : C) → Set (Sieve a)) S
Tactic: rw [mem_toPrecoverage_iff, ← Presieve.bindOfArrows_ofArrows]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{u_2, u_3} C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ J.toPrecoverage.coverings Y
have rw : Sieve.pullback g (Sieve.ofArrows X f) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: rw [mem_toPrecoverage_iff, ← Sieve.ofArrows, Sieve.ofArrows_eq_pullback_of_isPullback _ h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
K : Precoverage.{u_3, u_2} C
J : GrothendieckTopology.{u_3, u_2} C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage
have refine_1 : ∀ (h : K.toGrothendieck ≤ J) (X : C) (R : Presieve.{u_3, u_2} X) (hR : R ∈ K.coverings X),
  R ∈ J.toPrecoverage.coverings X
Tactic: refine ⟨fun h X R hR ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
K : Precoverage.{u_3, u_2} C
J : GrothendieckTopology.{u_3, u_2} C
refine_1 :
  ∀ (h : K.toGrothendieck ≤ J) (X : C) (R : Presieve.{u_3, u_2} X) (hR : R ∈ K.coverings X),
    R ∈ J.toPrecoverage.coverings X
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage
have refine_2 : ∀ (h : K ≤ J.toPrecoverage), K.toGrothendieck ≤ J
Tactic: refine ⟨fun h X R hR ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
K : Precoverage.{u_3, u_2} C
J : GrothendieckTopology.{u_3, u_2} C
h : K ≤ J.toPrecoverage
X : C
R : Sieve.{u_3, u_2} X
hR : R ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X
have refine_2 : ∀ (X : C) (S : Presieve.{u_3, u_2} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hR with
    | of X S hS => exact h _ hS
    | top X => grind
    | pullback X S _ Y f _ => grind
    | transitive X S R _ _ _ _ => grind
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
K : Precoverage.{u_3, u_2} C
J : GrothendieckTopology.{u_3, u_2} C
h : K ≤ J.toPrecoverage
X : C
R : Sieve.{u_3, u_2} X
hR : R ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (X : C) (S : Presieve.{u_3, u_2} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X
have refine_2₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hR with
    | of X S hS => exact h _ hS
    | top X => grind
    | pullback X S _ Y f _ => grind
    | transitive X S R _ _ _ _ => grind
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
K : Precoverage.{u_3, u_2} C
J : GrothendieckTopology.{u_3, u_2} C
h : K ≤ J.toPrecoverage
X : C
R : Sieve.{u_3, u_2} X
hR : R ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (X : C) (S : Presieve.{u_3, u_2} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
refine_2₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X
have refine_2₂ : ∀ (X : C) (S : Sieve.{u_3, u_2} X),
  K.Saturate X S →
    ∀ (Y : C) (f : Y ⟶ X), S ∈ (J : (a : C) → Set (Sieve a)) X → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: induction hR with
    | of X S hS => exact h _ hS
    | top X => grind
    | pullback X S _ Y f _ => grind
    | transitive X S R _ _ _ _ => grind
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
K : Precoverage.{u_3, u_2} C
J : GrothendieckTopology.{u_3, u_2} C
h : K ≤ J.toPrecoverage
X : C
R : Sieve.{u_3, u_2} X
hR : R ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (X : C) (S : Presieve.{u_3, u_2} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
refine_2₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
refine_2₂ :
  ∀ (X : C) (S : Sieve.{u_3, u_2} X),
    K.Saturate X S →
      ∀ (Y : C) (f : Y ⟶ X), S ∈ (J : (a : C) → Set (Sieve a)) X → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X
have refine_2₃ : ∀ (X : C) (S R : Sieve.{u_3, u_2} X),
  K.Saturate X S →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f R)) →
      S ∈ (J : (a : C) → Set (Sieve a)) X →
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (J : (a : C) → Set (Sieve a)) Y) →
          R ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hR with
    | of X S hS => exact h _ hS
    | top X => grind
    | pullback X S _ Y f _ => grind
    | transitive X S R _ _ _ _ => grind
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
⊢ IsTerminal (F.obj (op I))
have refine : (Y : Type w) → Unique (Y ⟶ F.obj (op I))
Tactic: refine @IsTerminal.ofUnique _ _ _ fun Y ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
Y : Type w
⊢ FamilyOfElements (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
have tauto : ⦃Y : C⦄ →
  (f : Y ⟶ I) →
    ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a) f →
      F.obj (op Y)
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
Y : Type w
⊢ FamilyOfElements.Compatible.{w, v, u} (P := F) (R :=
    ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
    fun ⦃Y : C⦄ (f : Y ⟶ I)
      (a : ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a) f) ↦
    False.elim ⋯
have tauto : ∀ ⦃Y₁ Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ I⦄ ⦃f₂ : Y₂ ⟶ I⦄
  (h₁ : ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a) f₁)
  (h₂ : ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a) f₂),
  g₁ ≫ f₁ = g₂ ≫ f₂ →
    Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
          ((fun ⦃Y : C⦄ (f : Y ⟶ I)
                (a :
                  ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
                    f) ↦
              (False.elim sorry : F.obj (op Y)))
            f₁ h₁) :
        (fun (X : Type w) ↦ X) (F.obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
          ((fun ⦃Y : C⦄ (f : Y ⟶ I)
                (a :
                  ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
                    f) ↦
              (False.elim sorry : F.obj (op Y)))
            f₂ h₂) :
        (fun (X : Type w) ↦ X) (F.obj (op Z)))
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
Y : Type w
⊢ Unique (Y ⟶ F.obj (op I))
have choose : (t : F.obj (op I)) →
  (h :
      (fun (t : F.obj (op I)) ↦
            FamilyOfElements.IsAmalgamation (R :=
              ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
              (fun ⦃Y : C⦄ (f : Y ⟶ I)
                  (a :
                    ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
                      f) ↦
                False.elim sorry)
              t)
          t ∧
        ∀ (y : F.obj (op I)),
          (fun (t : F.obj (op I)) ↦
                FamilyOfElements.IsAmalgamation (R :=
                  ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
                  (fun ⦃Y : C⦄ (f : Y ⟶ I)
                      (a :
                        ofArrows Empty.elim
                          (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a) f) ↦
                    False.elim sorry)
                  t)
              y →
            y = t) →
    Unique (Y ⟶ F.obj (op I))
Tactic: choose t h using hF (by tauto) (by tauto)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
Y : Type w
t : F.obj (op I)
h :
  (fun (t : F.obj (op I)) ↦
        FamilyOfElements.IsAmalgamation (R :=
          ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
          (fun ⦃Y : C⦄ (f : Y ⟶ I)
              (a :
                ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
                  f) ↦
            False.elim ⋯)
          t)
      t ∧
    ∀ (y : F.obj (op I)),
      (fun (t : F.obj (op I)) ↦
            FamilyOfElements.IsAmalgamation (R :=
              ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
              (fun ⦃Y : C⦄ (f : Y ⟶ I)
                  (a :
                    ofArrows Empty.elim (fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
                      f) ↦
                False.elim ⋯)
              t)
          y →
        y = t
a : Y ⟶ F.obj (op I)
⊢ a = default
have h₁ : ∀ (x : Y),
  (ConcreteCategory.hom (FC := TypeCat.Fun) a).toFun x =
    TypeCat.Fun.toFun (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ default) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
⊢ have this := ⋯;
  Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x) :
      F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj :
      F.obj
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (X x))
            (Fan.mk (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x)))) ⟶
        Equalizer.Presieve.Arrows.FirstObj F X)
have this : HasCoproduct.{u_1, v, u} X
Tactic: have : HasCoproduct X := ⟨⟨c, hc⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
this : HasCoproduct.{u_1, v, u} X
⊢ Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
      Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
have h : Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
  (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
  (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
    (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
Tactic: have h : Pi.lift (fun i ↦ F.map (c.inj i).op) =
      F.map (Pi.lift (fun i ↦ (c.inj i).op)) ≫ piComparison F _ := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
⊢ Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
      Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
have rw : Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
  (piComparison F fun (x : α) ↦ op (X x))
  (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
    (F.map
      (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
        Pi.lift fun (i : α) ↦ (c.inj i).op))
    (piComparison F fun (i : α) ↦ op (X i)))
Tactic: rw [h, ← Category.assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
⊢ Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map
        (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
          Pi.lift fun (i : α) ↦ (c.inj i).op))
      (piComparison F fun (i : α) ↦ op (X i)))
have hh : Eq (α := op c.pt ⟶ piObj.{u_1, v, u} fun (i : α) ↦ op (X i)) (Pi.lift fun (i : α) ↦ (c.inj i).op)
  (IsLimit.lift (productIsProduct fun (x : α) ↦ op (X x)) c.op)
Tactic: have hh : Pi.lift (fun i ↦ (c.inj i).op) = (productIsProduct (op <| X ·)).lift c.op := by
    simp [Pi.lift, productIsProduct]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
hh :
  Eq (α := op c.pt ⟶ piObj.{u_1, v, u} fun (i : α) ↦ op (X i)) (Pi.lift fun (i : α) ↦ (c.inj i).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (X x)) c.op)
⊢ Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map
        (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
          Pi.lift fun (i : α) ↦ (c.inj i).op))
      (piComparison F fun (i : α) ↦ op (X i)))
have rw : Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
  (piComparison F fun (x : α) ↦ op (X x))
  (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
    (F.map
      (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
        (hc.desc c).op ≫ Iso.hom (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))))
    (piComparison F fun (i : α) ↦ op (X i)))
Tactic: rw [hh, ← desc_op_comp_opCoproductIsoProduct'_hom hc]